helm/coq-contribs/LAMBDA-TYPES/ty0_lift.v

   1 Require lift_props.
   2 Require drop_props.
   3 Require pc3_props.
   4 Require ty0_defs.
   5
   6 (*#* #caption "main properties of typing" #clauses ty0_props *)
   7
   8    Section ty0_lift. (*******************************************************)
   9
  10 (*#* #caption "lift preserves types" *)
  11 (*#* #cap #cap t1, t2 #alpha c in C1, e in C2, d in i *)
  12
  13       Theorem ty0_lift : (g:?; e:?; t1,t2:?) (ty0 g e t1 t2) ->
  14                          (c:?) (wf0 g c) -> (d,h:?) (drop h d c e) ->
  15                          (ty0 g c (lift h d t1) (lift h d t2)).
  16
  17 (*#* #stop file *)
  18
  19       Intros until 1; XElim H; Intros.
  20 (* case 1 : ty0_conv *)
  21       XEAuto.
  22 (* case 2 : ty0_sort *)
  23       Repeat Rewrite lift_sort; XAuto.
  24 (* case 3 : ty0_abbr *)
  25       Apply (lt_le_e n d0); Intros; DropDis.
  26 (* case 3.1 : n < d0 *)
  27       Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
  28       DropGenBase; Rewrite H4 in H0; Clear H4 x.
  29       Rewrite lift_lref_lt; [ Idtac | XAuto ].
  30       Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
  31       EApply ty0_abbr; XEAuto.
  32 (* case 3.2 : n >= d0 *)
  33       Rewrite lift_lref_ge; [ Idtac | XAuto ].
  34       Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
  35       Rewrite (plus_sym h (S n)); Simpl; XEAuto.
  36 (* case 4: ty0_abst *)
  37       Apply (lt_le_e n d0); Intros; DropDis.
  38 (* case 4.1 : n < d0 *)
  39       Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
  40       DropGenBase; Rewrite H4 in H0; Clear H4 x.
  41       Rewrite lift_lref_lt; [ Idtac | XAuto ].
  42       Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
  43       EApply ty0_abst; XEAuto.
  44 (* case 4.2 : n >= d0 *)
  45       Rewrite lift_lref_ge; [ Idtac | XAuto ].
  46       Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
  47       Rewrite (plus_sym h (S n)); Simpl; XEAuto.
  48 (* case 5: ty0_bind *)
  49       LiftTailRw; Simpl; EApply ty0_bind; XEAuto.
  50 (* case 6: ty0_appl *)
  51       LiftTailRw; Simpl; EApply ty0_appl; [ Idtac | Rewrite <- lift_bind ]; XEAuto.
  52 (* case 7: ty0_cast *)
  53       LiftTailRw; XEAuto.
  54       Qed.
  55
  56    End ty0_lift.
  57
  58       Hints Resolve ty0_lift : ltlc.
  59
  60       Tactic Definition Ty0Lift b u :=
  61          Match Context With
  62             [ H: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
  63                LApply (ty0_lift ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
  64                LApply (H_x (CTail ?2 (Bind b) u)); [ Clear H_x; Intros H_x | XEAuto ];
  65                LApply (H_x (0) (1)); [ Clear H_x; Intros | XAuto ].