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/inv".
17 include "Lift/defs.ma".
19 (* Inversion properties *****************************************************)
21 theorem lift_inv_sort_1: \forall l, i, h, x.
22 Lift l i (leaf (sort h)) x \to
24 intros. inversion H; clear H; intros;
33 theorem lift_inv_lref_1: \forall l, i, j1, x.
34 Lift l i (leaf (lref j1)) x \to
35 (i > j1 \land x = leaf (lref j1)) \lor
37 \exists j2. (l + j1 == j2) \land x = leaf (lref j2)
39 intros. inversion H; clear H; intros;
41 | destruct H2. clear H2. subst. auto
42 | destruct H3. clear H3. subst. auto depth = 5
48 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
49 Lift l i (intb r u1 t1) x \to
52 Lift l (succ i) t1 t2 \land
54 intros. inversion H; clear H; intros;
58 | destruct H5. clear H5 H1 H3. subst. auto depth = 5
63 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
64 Lift l i (intf r u1 t1) x \to
69 intros. inversion H; clear H; intros;
74 | destruct H5. clear H5 H1 H3. subst. auto depth = 5
78 theorem lift_inv_sort_2: \forall l, i, x, h.
79 Lift l i x (leaf (sort h)) \to
81 intros. inversion H; clear H; intros;
90 theorem lift_inv_lref_2: \forall l, i, x, j2.
91 Lift l i x (leaf (lref j2)) \to
92 (i > j2 \land x = leaf (lref j2)) \lor
94 \exists j1. (l + j1 == j2) \land x = leaf (lref j1)
96 intros. inversion H; clear H; intros;
98 | destruct H3. clear H3. subst. auto
99 | destruct H4. clear H4. subst. auto depth = 5
105 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
106 Lift l i x (intb r u2 t2) \to
109 Lift l (succ i) t1 t2 \land
111 intros. inversion H; clear H; intros;
115 | destruct H6. clear H5 H1 H3. subst. auto depth = 5
120 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
121 Lift l i x (intf r u2 t2) \to
126 intros. inversion H; clear H; intros;
131 | destruct H6. clear H6 H1 H3. subst. auto depth = 5
135 (* Corollaries of inversion properties ***************************************)
137 theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
138 Lift l i (leaf (lref j1)) x \to
139 i > j1 \to x = leaf (lref j1).
141 lapply linear lift_inv_lref_1 to H. decompose; subst;
143 | lapply linear nle_false to H2, H1. decompose
147 theorem lift_inv_lref_1_le: \forall l, i, j1, x.
148 Lift l i (leaf (lref j1)) x \to
149 i <= j1 \to \forall j2. (l + j1 == j2) \to
152 lapply linear lift_inv_lref_1 to H. decompose; subst;
153 [ lapply linear nle_false to H1, H3. decompose
154 | lapply linear nplus_mono to H2, H4. subst. auto
158 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
159 Lift l i x (leaf (lref j2)) \to
160 i > j2 \to x = leaf (lref j2).
162 lapply linear lift_inv_lref_2 to H. decompose; subst;
164 | lapply linear nle_false to H2, H1. decompose
168 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
169 Lift l i x (leaf (lref j2)) \to
170 i <= j2 \to \forall j1. (l + j1 == j2) \to
173 lapply linear lift_inv_lref_2 to H. decompose; subst;
174 [ lapply linear nle_false to H1, H3. decompose
175 | lapply linear nplus_inj_2 to H2, H4. subst. auto