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 (* NOTE: this holds because of nplus_comm_1 *)
20 theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
21 \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
22 \forall x. Lift l2 i2 t2 x \to
23 \forall i,y. Lift l1 i u1 y \to
24 i1 >= i2 \to (l2 + i1 == i) \to x = y.
25 intros 5. elim H; clear H i1 t1 t2;
26 [ lapply lift_mono to H1, H2. clear H2. subst.
27 lapply linear lift_inv_sort_1 to H1. subst.
28 lapply linear lift_inv_sort_1 to H3. subst. auto
29 | lapply lift_mono to H2, H3. clear H3. subst.
30 lapply linear lift_inv_lref_1 to H2.
31 decompose; subst; clear H2 H5;
32 lapply linear lift_inv_lref_1_gt to H4; subst; auto width = 4
33 | lapply lift_inv_lref_1_le to H3; [ 2: auto ]. clear H3.
34 lapply lift_inv_lref_1_le to H4; [ 2: auto ]. clear H4.
35 decompose. subst. clear H6 i2.
36 lapply lift_inv_lref_1_le to H5; [ 2: auto depth = 4 width = 4 ].
37 decompose. subst. clear H5 H1 H7 i. auto depth = 4
39 lapply linear lift_inv_bind_1 to H5.
40 lapply linear lift_inv_bind_1 to H6. decompose. subst.
41 lapply linear lift_inv_bind_1 to H7. decompose. subst.
44 lapply linear lift_inv_flat_1 to H5.
45 lapply linear lift_inv_flat_1 to H6. decompose. subst.
46 lapply linear lift_inv_flat_1 to H7. decompose. subst.
51 theorem lift_comp_rew_dx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
52 \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
53 \forall u2. Lift l2 i2 t2 u2 \to
54 i1 >= i2 \to \forall i. (l2 + i1 == i) \to
57 lapply (lift_total l1 u1 i). decompose.
58 lapply lift_comp to H, H1, H2, H5, H3, H4. subst. auto.
61 theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
62 \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
63 \forall i,u2. Lift l2 i t2 u2 \to
64 i2 >= i1 \to (l1 + i2 == i) \to
67 lapply (lift_total l1 u1 i1). decompose.
68 lapply lift_comp to H1, H, H5, H2, H3, H4. subst. auto.
71 theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
72 \forall l2,i2,z. Lift l2 i2 t2 t3 \to
74 \forall i. \to i2 <= i \to (l1 + i1 == i) \to
75 \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
77 axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
78 \forall l2,i,t2. Lift l2 i t2 u2 \to
79 \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
80 \exists t1. | Lift l2 i2 t1 u1 \land