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

   1 (*#* #stop file *)
   2
   3 Require lift_defs.
   4
   5    Section lift_ini. (*******************************************************)
   6
   7       Tactic Definition IH :=
   8          Match Context With
   9             | [ H1: (lift ?1 ?2 t) = (lift ?1 ?2 ?3) |- ? ] ->
  10                LApply (H ?3 ?1 ?2); [ Clear H H1; Intros | XAuto ]
  11             | [ H1: (lift ?1 ?2 t0) = (lift ?1 ?2 ?3) |- ? ] ->
  12                LApply (H0 ?3 ?1 ?2); [ Clear H0 H1; Intros | XAuto ].
  13
  14 (*#* #caption "main properties of lift" #clauses lift_props *)
  15
  16 (*#* #caption "injectivity" *)
  17 (*#* #cap #alpha x in T1, t in T2, d in i *)
  18
  19       Theorem lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
  20       XElim x.
  21 (* case 1 : TSort *)
  22       Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
  23 (* case 2 : TLRef n *)
  24       Intros; Apply (lt_le_e n d); Intros.
  25 (* case 2.1 : n < d *)
  26       Rewrite lift_lref_lt in H; [ LiftGenBase; XAuto | XAuto ].
  27 (* case 2.2 : n >= d *)
  28       Rewrite lift_lref_ge in H; [ LiftGenBase; XAuto | XAuto ].
  29 (* case 3 : TTail k *)
  30       XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
  31       LiftGenBase; Rewrite H1; IH; IH; XAuto.
  32       Qed.
  33
  34    End lift_ini.
  35
  36    Section lift_gen_lift. (**************************************************)
  37
  38       Tactic Definition IH :=
  39          Match Context With
  40             | [ H_x: (lift ?0 ?1 t) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
  41                LApply (H ?4 ?0 ?2 ?1 ?3); [ Clear H; Intros H | XAuto ];
  42                LApply H; [ Clear H H_x; Intros H | XAuto ];
  43                XElim H; Intros
  44             | [ H_x: (lift ?0 ?1 t0) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
  45                LApply (H0 ?4 ?0 ?2 ?1 ?3); [ Clear H0; Intros H0 | XAuto ];
  46                LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
  47                XElim H0; Intros.
  48
  49 (*#* #caption "generation lemma for lift" *)
  50 (*#* #cap #cap t1 #alpha t2 in T, x in T2, d1 in i1, d2 in i2 *)
  51
  52       Theorem lift_gen_lift : (t1,x:?; h1,h2,d1,d2:?) (le d1 d2) ->
  53                               (lift h1 d1 t1) = (lift h2 (plus d2 h1) x) ->
  54                               (EX t2 | x = (lift h1 d1 t2) &
  55                                        t1 = (lift h2 d2 t2)
  56                               ).
  57       XElim t1; Intros.
  58 (* case 1 : TSort *)
  59       Rewrite lift_sort in H0.
  60       LiftGenBase; Rewrite H0; Clear H0 x.
  61       EApply ex2_intro; Rewrite lift_sort; XAuto.
  62 (* case 2 : TLRef n *)
  63       Apply (lt_le_e n d1); Intros.
  64 (* case 2.1 : n < d1 *)
  65       Rewrite lift_lref_lt in H0; [ Idtac | XAuto ].
  66       LiftGenBase; Rewrite H0; Clear H0 x.
  67       EApply ex2_intro; Rewrite lift_lref_lt; XEAuto.
  68 (* case 2.2 : n >= d1 *)
  69       Rewrite lift_lref_ge in H0; [ Idtac | XAuto ].
  70       Apply (lt_le_e n d2); Intros.
  71 (* case 2.2.1 : n < d2 *)
  72       LiftGenBase; Rewrite H0; Clear H0 x.
  73       EApply ex2_intro; [ Rewrite lift_lref_ge | Rewrite lift_lref_lt ]; XEAuto.
  74 (* case 2.2.2 : n >= d2 *)
  75       Apply (lt_le_e n (plus d2 h2)); Intros.
  76 (* case 2.2.2.1 : n < d2 + h2 *)
  77       EApply lift_gen_lref_false; [ Idtac | Idtac | Apply H0 ];
  78       [ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
  79 (* case 2.2.2.2 : n >= d2 + h2 *)
  80       Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XEAuto ].
  81       LiftGenBase; Rewrite H0; Clear H0 x.
  82       EApply ex2_intro;
  83       [ Rewrite le_minus_plus; [ Idtac | XEAuto ]
  84       | Rewrite (le_plus_minus_sym h2 n); [ Idtac | XEAuto ] ];
  85       Rewrite lift_lref_ge; XEAuto.
  86 (* case 3 : TTail k *)
  87       NewInduction k.
  88 (* case 3.1 : Bind *)
  89       Rewrite lift_bind in H2.
  90       LiftGenBase; Rewrite H2; Clear H2 x.
  91       IH; Rewrite H; Rewrite H2; Clear H H2 x0.
  92       Arith4In H4 d2 h1; IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
  93       EApply ex2_intro; Rewrite lift_bind; XAuto.
  94 (* case 3.2 : Flat *)
  95       Rewrite lift_flat in H2.
  96       LiftGenBase; Rewrite H2; Clear H2 x.
  97       IH; Rewrite H; Rewrite H2; Clear H H2 x0.
  98       IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
  99       EApply ex2_intro; Rewrite lift_flat; XAuto.
 100       Qed.
 101
 102    End lift_gen_lift.
 103
 104       Tactic Definition LiftGen :=
 105          Match Context With
 106             | [ H: (lift ?1 ?2 ?3) = (lift ?1 ?2 ?4) |- ? ] ->
 107                LApply (lift_inj ?3 ?4 ?1 ?2); [ Clear H; Intros | XAuto ]
 108             | [ H: (lift ?0 ?1 ?2) = (lift ?3 (plus ?4 ?0) ?5) |- ? ] ->
 109                LApply (lift_gen_lift ?2 ?5 ?0 ?3 ?1 ?4); [ Intros H_x | XAuto ];
 110                LApply H_x; [ Clear H H_x; Intros H | XAuto ];
 111                XElim H; Intros
 112             | [ H: (lift (1) (0) ?1) = (lift (1) (S ?2) ?3) |- ? ] ->
 113                LApply (lift_gen_lift ?1 ?3 (1) (1) (0) ?2); [ Intros H_x | XAuto ];
 114                LApply H_x; [ Clear H_x H; Intros H | Arith7' ?2; XAuto ];
 115                XElim H; Intros
 116             | _ -> LiftGenBase.