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 (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 (lref j1) x \to
35 (i > j1 \land x = lref j1) \lor
37 \exists j2. (l + j1 == j2) \land x = 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 (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 (lref j2) \to
92 (i > j2 \land x = lref j2) \lor
94 \exists j1. (l + j1 == j2) \land x = 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 (lref j1) x \to
139 i > j1 \to x = 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 (lref j1) x \to i <= j1 \to
149 \exists j2. (l + j1 == j2) \land x = lref j2.
151 lapply linear lift_inv_lref_1 to H. decompose; subst;
152 [ lapply linear nle_false to H1, H2. decompose
157 theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
158 Lift l i (lref j1) x \to
159 i <= j1 \to \forall j2. (l + j1 == j2) \to
162 lapply linear lift_inv_lref_1 to H. decompose; subst;
163 [ lapply linear nle_false to H1, H3. decompose
164 | lapply linear nplus_mono to H2, H4. subst. auto
168 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
169 Lift l i x (lref j2) \to
170 i > j2 \to x = lref j2.
172 lapply linear lift_inv_lref_2 to H. decompose; subst;
174 | lapply linear nle_false to H2, H1. decompose
178 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
179 Lift l i x (lref j2) \to i <= j2 \to
180 \exists j1. (l + j1 == j2) \land x = lref j1.
182 lapply linear lift_inv_lref_2 to H. decompose; subst;
183 [ lapply linear nle_false to H1, H2. decompose
188 theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
189 Lift l i x (lref j2) \to
190 i <= j2 \to \forall j1. (l + j1 == j2) \to
193 lapply linear lift_inv_lref_2 to H. decompose; subst;
194 [ lapply linear nle_false to H1, H3. decompose
195 | lapply linear nplus_inj_2 to H2, H4. subst. auto