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 include "ground/xoa/ex_3_1.ma".
16 include "ground/xoa/ex_3_4.ma".
17 include "ground/xoa/ex_4_1.ma".
18 include "ground/arith/nat_succ.ma".
19 include "static_2/notation/relations/voidstareq_4.ma".
20 include "static_2/syntax/lenv.ma".
22 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
24 inductive lveq: bi_relation nat lenv โ
25 | lveq_atom : lveq ๐ (โ) ๐ (โ)
26 | lveq_bind : โI1,I2,K1,K2. lveq ๐ K1 ๐ K2 โ
27 lveq ๐ (K1.โ[I1]) ๐ (K2.โ[I2])
28 | lveq_void_sn: โK1,K2,n1. lveq n1 K1 ๐ K2 โ
29 lveq (โn1) (K1.โง) ๐ K2
30 | lveq_void_dx: โK1,K2,n2. lveq ๐ K1 n2 K2 โ
31 lveq ๐ K1 (โn2) (K2.โง)
34 interpretation "equivalence up to exclusion binders (local environment)"
35 'VoidStarEq L1 n1 n2 L2 = (lveq n1 L1 n2 L2).
37 (* Basic properties *********************************************************)
39 lemma lveq_refl: โL. L โโง*[๐,๐] L.
40 #L elim L -L /2 width=1 by lveq_atom, lveq_bind/
43 lemma lveq_sym: bi_symmetric โฆ lveq.
44 #n1 #n2 #L1 #L2 #H elim H -L1 -L2 -n1 -n2
45 /2 width=1 by lveq_atom, lveq_bind, lveq_void_sn, lveq_void_dx/
48 (* Basic inversion lemmas ***************************************************)
50 fact lveq_inv_zero_aux: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
51 (๐ = n1) โ ๐ = n2 โ
52 โจโจ โงโง โ = L1 & โ = L2
53 | โโI1,I2,K1,K2. K1 โโง*[๐,๐] K2 & K1.โ[I1] = L1 & K2.โ[I2] = L2.
54 #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
55 [1: /3 width=1 by or_introl, conj/
56 |2: /3 width=7 by ex3_4_intro, or_intror/
57 |*: #K1 #K2 #n #_ [ #H #_ | #_ #H ]
58 elim (eq_inv_zero_nsucc โฆ H)
62 lemma lveq_inv_zero: โL1,L2. L1 โโง*[๐,๐] L2 โ
63 โจโจ โงโง โ = L1 & โ = L2
64 | โโI1,I2,K1,K2. K1 โโง*[๐,๐] K2 & K1.โ[I1] = L1 & K2.โ[I2] = L2.
65 /2 width=5 by lveq_inv_zero_aux/ qed-.
67 fact lveq_inv_succ_sn_aux: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
69 โโK1. K1 โโง*[m1,๐] L2 & K1.โง = L1 & ๐ = n2.
70 #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
71 [1: #m #H elim (eq_inv_nsucc_zero โฆ H)
72 |2: #I1 #I2 #K1 #K2 #_ #m #H elim (eq_inv_nsucc_zero โฆ H)
73 |*: #K1 #K2 #n #HK #m #H
74 [ >(eq_inv_nsucc_bi โฆ H) -m /2 width=3 by ex3_intro/
75 | elim (eq_inv_nsucc_zero โฆ H)
80 lemma lveq_inv_succ_sn: โL1,K2,n1,n2. L1 โโง*[โn1,n2] K2 โ
81 โโK1. K1 โโง*[n1,๐] K2 & K1.โง = L1 & ๐ = n2.
82 /2 width=3 by lveq_inv_succ_sn_aux/ qed-.
84 lemma lveq_inv_succ_dx: โK1,L2,n1,n2. K1 โโง*[n1,โn2] L2 โ
85 โโK2. K1 โโง*[๐,n2] K2 & K2.โง = L2 & ๐ = n1.
87 lapply (lveq_sym โฆ H) -H #H
88 elim (lveq_inv_succ_sn โฆ H) -H /3 width=3 by lveq_sym, ex3_intro/
91 fact lveq_inv_succ_aux: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
92 โm1,m2. โm1 = n1 โ โm2 = n2 โ โฅ.
93 #L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
94 [1: #m1 #m2 #H #_ elim (eq_inv_nsucc_zero โฆ H)
95 |2: #I1 #I2 #K1 #K2 #_ #m1 #m2 #H #_ elim (eq_inv_nsucc_zero โฆ H)
96 |*: #K1 #K2 #n #_ #m1 #m2 [ #_ #H | #H #_ ]
97 elim (eq_inv_nsucc_zero โฆ H)
101 lemma lveq_inv_succ: โL1,L2,n1,n2. L1 โโง*[โn1,โn2] L2 โ โฅ.
102 /2 width=9 by lveq_inv_succ_aux/ qed-.
104 (* Advanced inversion lemmas ************************************************)
106 lemma lveq_inv_bind_O: โI1,I2,K1,K2. K1.โ[I1] โโง*[๐,๐] K2.โ[I2] โ K1 โโง*[๐,๐] K2.
108 elim (lveq_inv_zero โฆ H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct //
111 lemma lveq_inv_atom_atom: โn1,n2. โ โโง*[n1,n2] โ โ โงโง ๐ = n1 & ๐ = n2.
112 #n1 @(nat_ind_succ โฆ n1) -n1 [2: #n1 #_ ]
113 #n2 @(nat_ind_succ โฆ n2) -n2 [2,4: #n2 #_ ]
115 [ elim (lveq_inv_succ โฆ H)
116 | elim (lveq_inv_succ_dx โฆ H) -H #Y #_ #H1 #H2 destruct
117 | elim (lveq_inv_succ_sn โฆ H) -H #Y #_ #H1 #H2 destruct
118 | /2 width=1 by conj/
122 lemma lveq_inv_bind_atom: โI1,K1,n1,n2. K1.โ[I1] โโง*[n1,n2] โ โ
123 โโm1. K1 โโง*[m1,๐] โ & BUnit Void = I1 & โm1 = n1 & ๐ = n2.
125 #n1 @(nat_ind_succ โฆ n1) -n1 [2: #n1 #_ ]
126 #n2 @(nat_ind_succ โฆ n2) -n2 [2,4: #n2 #_ ]
128 [ elim (lveq_inv_succ โฆ H)
129 | elim (lveq_inv_succ_dx โฆ H) -H #Y #_ #H1 #H2 destruct
130 | elim (lveq_inv_succ_sn โฆ H) -H #Y #HY #H1 #H2 destruct /2 width=3 by ex4_intro/
131 | elim (lveq_inv_zero โฆ H) -H *
133 | #Z1 #Z2 #Y1 #Y2 #_ #H1 #H2 destruct
138 lemma lveq_inv_atom_bind: โI2,K2,n1,n2. โ โโง*[n1,n2] K2.โ[I2] โ
139 โโm2. โ โโง*[๐,m2] K2 & BUnit Void = I2 & ๐ = n1 & โm2 = n2.
141 lapply (lveq_sym โฆ H) -H #H
142 elim (lveq_inv_bind_atom โฆ H) -H
143 /3 width=3 by lveq_sym, ex4_intro/
146 lemma lveq_inv_pair_pair: โI1,I2,K1,K2,V1,V2,n1,n2. K1.โ[I1]V1 โโง*[n1,n2] K2.โ[I2]V2 โ
147 โงโง K1 โโง*[๐,๐] K2 & ๐ = n1 & ๐ = n2.
148 #I1 #I2 #K1 #K2 #V1 #V2
149 #n1 @(nat_ind_succ โฆ n1) -n1 [2: #n1 #_ ]
150 #n2 @(nat_ind_succ โฆ n2) -n2 [2,4: #n2 #_ ]
152 [ elim (lveq_inv_succ โฆ H)
153 | elim (lveq_inv_succ_dx โฆ H) -H #Y #_ #H1 #H2 destruct
154 | elim (lveq_inv_succ_sn โฆ H) -H #Y #_ #H1 #H2 destruct
155 | elim (lveq_inv_zero โฆ H) -H *
157 | #Z1 #Z2 #Y1 #Y2 #HY #H1 #H2 destruct /3 width=1 by and3_intro/
162 lemma lveq_inv_void_succ_sn: โL1,L2,n1,n2. L1.โง โโง*[โn1,n2] L2 โ
163 โงโง L1 โ โง*[n1,๐] L2 & ๐ = n2.
165 elim (lveq_inv_succ_sn โฆ H) -H #Y #HY #H1 #H2 destruct /2 width=1 by conj/
168 lemma lveq_inv_void_succ_dx: โL1,L2,n1,n2. L1 โโง*[n1,โn2] L2.โง โ
169 โงโง L1 โ โง*[๐,n2] L2 & ๐ = n1.
171 lapply (lveq_sym โฆ H) -H #H
172 elim (lveq_inv_void_succ_sn โฆ H) -H
173 /3 width=1 by lveq_sym, conj/
176 (* Advanced forward lemmas **************************************************)
178 lemma lveq_fwd_gen: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
179 โจโจ ๐ = n1 | ๐ = n2.
181 #n1 @(nat_ind_succ โฆ n1) -n1 [2: #n1 #_ ]
182 #n2 @(nat_ind_succ โฆ n2) -n2 [2,4: #n2 #_ ]
184 [ elim (lveq_inv_succ โฆ H) ]
185 /2 width=1 by or_introl, or_intror/
188 lemma lveq_fwd_pair_sn:
189 โI1,K1,L2,V1,n1,n2. K1.โ[I1]V1 โโง*[n1,n2] L2 โ ๐ = n1.
191 #n1 @(nat_ind_succ โฆ n1) -n1 [2: #n1 #_ ] //
192 #n2 @(nat_ind_succ โฆ n2) -n2 [2: #n2 #_ ] #H
193 [ elim (lveq_inv_succ โฆ H)
194 | elim (lveq_inv_succ_sn โฆ H) -H #Y #_ #H1 #H2 destruct
198 lemma lveq_fwd_pair_dx:
199 โI2,L1,K2,V2,n1,n2. L1 โโง*[n1,n2] K2.โ[I2]V2 โ ๐ = n2.
200 /3 width=6 by lveq_fwd_pair_sn, lveq_sym/ qed-.