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; subst. autobatch.
27 theorem lift_inv_lref_1: \forall l, i, j1, x.
28 Lift l i (lref j1) x \to
29 (i > j1 \land x = lref j1) \lor
31 \exists j2. (l + j1 == j2) \land x = lref j2
33 intros. inversion H; clear H; intros; subst; auto depth = 5.
36 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
37 Lift l i (intb r u1 t1) x \to
40 Lift l (succ i) t1 t2 \land
42 intros. inversion H; clear H; intros; subst. auto depth = 5.
45 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
46 Lift l i (intf r u1 t1) x \to
51 intros. inversion H; clear H; intros; subst. auto depth = 5.
54 theorem lift_inv_sort_2: \forall l, i, x, h.
55 Lift l i x (sort h) \to
57 intros. inversion H; clear H; intros; subst. autobatch.
60 theorem lift_inv_lref_2: \forall l, i, x, j2.
61 Lift l i x (lref j2) \to
62 (i > j2 \land x = lref j2) \lor
64 \exists j1. (l + j1 == j2) \land x = lref j1
66 intros. inversion H; clear H; intros; subst; auto depth = 5.
69 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
70 Lift l i x (intb r u2 t2) \to
73 Lift l (succ i) t1 t2 \land
75 intros. inversion H; clear H; intros; subst. auto depth = 5.
78 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
79 Lift l i x (intf r u2 t2) \to
84 intros. inversion H; clear H; intros; subst. auto depth = 5.
87 (* Corollaries of inversion properties ***************************************)
89 theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
90 Lift l i (lref j1) x \to
91 i > j1 \to x = lref j1.
93 lapply linear lift_inv_lref_1 to H. decompose; subst;
95 | lapply linear nle_false to H2, H1. decompose
99 theorem lift_inv_lref_1_le: \forall l, i, j1, x.
100 Lift l i (lref j1) x \to i <= j1 \to
101 \exists j2. (l + j1 == j2) \land x = lref j2.
103 lapply linear lift_inv_lref_1 to H. decompose; subst;
104 [ lapply linear nle_false to H1, H2. decompose
109 theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
110 Lift l i (lref j1) x \to
111 i <= j1 \to \forall j2. (l + j1 == j2) \to
114 lapply linear lift_inv_lref_1 to H. decompose; subst;
115 [ lapply linear nle_false to H1, H3. decompose
116 | lapply linear nplus_mono to H2, H4. subst. auto
120 theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
121 Lift l i x (lref j2) \to
122 i > j2 \to x = lref j2.
124 lapply linear lift_inv_lref_2 to H. decompose; subst;
126 | lapply linear nle_false to H2, H1. decompose
130 theorem lift_inv_lref_2_le: \forall l, i, x, j2.
131 Lift l i x (lref j2) \to i <= j2 \to
132 \exists j1. (l + j1 == j2) \land x = lref j1.
134 lapply linear lift_inv_lref_2 to H. decompose; subst;
135 [ lapply linear nle_false to H1, H2. decompose
140 theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
141 Lift l i x (lref j2) \to
142 i <= j2 \to \forall j1. (l + j1 == j2) \to
145 lapply linear lift_inv_lref_2 to H. decompose; subst;
146 [ lapply linear nle_false to H1, H3. decompose
147 | lapply linear nplus_inj_2 to H2, H4. subst. auto