5 Section lift_ini. (*******************************************************)
7 Tactic Definition IH :=
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 ].
16 (*#* #caption "main properties of lift" #clauses lift_props *)
18 (*#* #caption "injectivity" *)
19 (*#* #cap #alpha x in T1, t in T2, d in i *)
21 Theorem lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
27 Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
28 (* case 2 : TBRef n *)
29 Intros; Apply (lt_le_e n d); Intros.
30 (* case 2.1 : n < d *)
31 Rewrite lift_bref_lt in H; [ LiftGenBase; XAuto | XAuto ].
32 (* case 2.2 : n >= d *)
33 Rewrite lift_bref_ge in H; [ LiftGenBase; XAuto | XAuto ].
34 (* case 3 : TTail k *)
35 XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
36 LiftGenBase; Rewrite H1; IH; IH; XAuto.
41 Section lift_gen_lift. (**************************************************)
43 Tactic Definition IH :=
45 | [ H_x: (lift ?0 ?1 t) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
46 LApply (H ?4 ?0 ?2 ?1 ?3); [ Clear H; Intros H | XAuto ];
47 LApply H; [ Clear H H_x; Intros H | XAuto ];
49 | [ H_x: (lift ?0 ?1 t0) = (lift ?2 (plus ?3 ?0) ?4) |- ? ] ->
50 LApply (H0 ?4 ?0 ?2 ?1 ?3); [ Clear H0; Intros H0 | XAuto ];
51 LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
56 (*#* #caption "generation lemma for lift" *)
57 (*#* #cap #cap t1 #alpha t2 in T, x in T2, d1 in i1, d2 in i2 *)
59 Theorem lift_gen_lift : (t1,x:?; h1,h2,d1,d2:?) (le d1 d2) ->
60 (lift h1 d1 t1) = (lift h2 (plus d2 h1) x) ->
61 (EX t2 | x = (lift h1 d1 t2) &
69 Rewrite lift_sort in H0.
70 LiftGenBase; Rewrite H0; Clear H0 x.
71 EApply ex2_intro; Rewrite lift_sort; XAuto.
72 (* case 2 : TBRef n *)
73 Apply (lt_le_e n d1); Intros.
74 (* case 2.1 : n < d1 *)
75 Rewrite lift_bref_lt in H0; [ Idtac | XAuto ].
76 LiftGenBase; Rewrite H0; Clear H0 x.
77 EApply ex2_intro; Rewrite lift_bref_lt; XEAuto.
78 (* case 2.2 : n >= d1 *)
79 Rewrite lift_bref_ge in H0; [ Idtac | XAuto ].
80 Apply (lt_le_e n d2); Intros.
81 (* case 2.2.1 : n < d2 *)
82 LiftGenBase; Rewrite H0; Clear H0 x.
83 EApply ex2_intro; [ Rewrite lift_bref_ge | Rewrite lift_bref_lt ]; XEAuto.
84 (* case 2.2.2 : n >= d2 *)
85 Apply (lt_le_e n (plus d2 h2)); Intros.
86 (* case 2.2.2.1 : n < d2 + h2 *)
87 EApply lift_gen_bref_false; [ Idtac | Idtac | Apply H0 ];
88 [ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
89 (* case 2.2.2.2 : n >= d2 + h2 *)
90 Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XEAuto ].
91 LiftGenBase; Rewrite H0; Clear H0 x.
93 [ Rewrite le_minus_plus; [ Idtac | XEAuto ]
94 | Rewrite (le_plus_minus_sym h2 n); [ Idtac | XEAuto ] ];
95 Rewrite lift_bref_ge; XEAuto.
96 (* case 3 : TTail k *)
99 Rewrite lift_bind in H2.
100 LiftGenBase; Rewrite H2; Clear H2 x.
101 IH; Rewrite H; Rewrite H2; Clear H H2 x0.
102 Arith4In H4 d2 h1; IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
103 EApply ex2_intro; Rewrite lift_bind; XAuto.
104 (* case 3.2 : Flat *)
105 Rewrite lift_flat in H2.
106 LiftGenBase; Rewrite H2; Clear H2 x.
107 IH; Rewrite H; Rewrite H2; Clear H H2 x0.
108 IH; Rewrite H; Rewrite H0; Clear H H0 x1 t t0.
109 EApply ex2_intro; Rewrite lift_flat; XAuto.
114 Tactic Definition LiftGen :=
116 | [ H: (lift ?1 ?2 ?3) = (lift ?1 ?2 ?4) |- ? ] ->
117 LApply (lift_inj ?3 ?4 ?1 ?2); [ Clear H; Intros | XAuto ]
118 | [ H: (lift ?0 ?1 ?2) = (lift ?3 (plus ?4 ?0) ?5) |- ? ] ->
119 LApply (lift_gen_lift ?2 ?5 ?0 ?3 ?1 ?4); [ Intros H_x | XAuto ];
120 LApply H_x; [ Clear H H_x; Intros H | XAuto ];
122 | [ H: (lift (1) (0) ?1) = (lift (1) (S ?2) ?3) |- ? ] ->
123 LApply (lift_gen_lift ?1 ?3 (1) (1) (0) ?2); [ Intros H_x | XAuto ];
124 LApply H_x; [ Clear H_x H; Intros H | Arith7' ?2; XAuto ];