1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
17 include "Lift/fun.ma".
19 theorem lift_comp_ge_1: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
20 \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
21 \forall u2. Lift l2 i2 t2 u2 \to
22 i1 >= i2 \to \forall i. (l2 + i1 == i) \to
24 intros 5. elim H; clear H i1 t1 t2;
25 [ lapply lift_conf to H1, H2. clear H2. subst.
26 lapply linear lift_inv_sort_1 to H1.
28 | lapply lift_conf to H2, H3. clear H3. subst.
29 lapply linear lift_inv_lref_1 to H2.
30 decompose; subst; clear H2 H4 i2;
31 [ lapply linear nle_nplus to H5 as H0. clear l2. (**)
32 lapply linear nle_trans to H1, H0.
34 | lapply nle_nplus_comp_lt_2 to H3, H5; auto.
36 | lapply linear lift_inv_lref_1 to H3.
38 [ clear H2 H4 H6 n3 l2.
39 lapply linear nle_trans to H3, H5 as H0.
40 lapply linear nle_false to H1, H0. decompose
41 | lapply linear lift_inv_lref_1 to H4.
43 [ clear H1 H5 H6 H7 n1.
44 lapply linear nle_nplus to H2 as H0. (**)
45 lapply linear nle_trans to H3, H0 as H2.
46 lapply linear nle_false to H2, H4. decompose
48 lapply nle_nplus_comp to H6, H7; auto.
52 lapply linear lift_inv_bind_1 to H5.
53 lapply linear lift_inv_bind_1 to H6.
54 decompose. subst. auto width = 4
56 lapply linear lift_inv_flat_1 to H5.
57 lapply linear lift_inv_flat_1 to H6.
58 decompose. subst. auto width = 4
62 theorem lift_comp_ge_2: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
63 \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
64 \forall i,u2. Lift l2 i t2 u2 \to
65 i2 >= i1 \to (l1 + i2 == i) \to
67 intros 5. elim H; clear H i1 t1 t2;
68 [ lapply linear lift_inv_sort_1 to H1.
69 lapply linear lift_inv_sort_1 to H2.
71 | lapply linear lift_inv_lref_1 to H2.
72 lapply linear lift_inv_lref_1 to H3.
73 decompose; subst; (* clear H2 H4 i2; *)
74 [ clear H H3 H4 H5. auto
76 lapply linear nle_nplus to H5 as H0. (**)
77 lapply linear nle_trans to H3, H0 as H2.
78 lapply nle_false to H, H2. decompose
80 lapply linear nle_trans to H4, H3 as H.
81 lapply nle_false to H, H1. decompose
83 lapply linear nle_trans to H4, H3 as H.
84 lapply nle_false to H, H1. decompose
87 | lapply linear lift_inv_lref_1 to H3.
89 [ clear H2 H4 H6 n3 l2.
90 lapply linear nle_trans to H3, H5 as H0.
91 lapply linear nle_false to H1, H0. decompose
92 | lapply linear lift_inv_lref_1 to H4.
94 [ clear H1 H5 H6 H7 n1.
95 lapply linear nle_nplus to H2 as H0. (**)
96 lapply linear nle_trans to H3, H0 as H2.
97 lapply linear nle_false to H2, H4. decompose
99 lapply nle_nplus_comp to H6, H7; auto.
103 lapply linear lift_inv_bind_1 to H5.
104 lapply linear lift_inv_bind_1 to H6.
105 decompose. subst. auto width = 4
107 lapply linear lift_inv_flat_1 to H5.
108 lapply linear lift_inv_flat_1 to H6.
109 decompose. subst. auto width = 4
115 theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
116 \forall l2,i2,z. Lift l2 i2 t2 t3 \to
118 \forall i. \to i2 <= i \to (l1 + i1 == i) \to
119 \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
121 axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
122 \forall l2,i,t2. Lift l2 i t2 u2 \to
123 \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
124 \exists t1. | Lift l2 i2 t1 u1 \land