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 "basic_2/syntax/lenv_length.ma".
16 include "basic_2/syntax/voids.ma".
18 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
20 (* Forward lemmas with length for local environments ************************)
22 lemma voids_fwd_length_le_sn: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n1 ≤ |L1|.
23 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
27 lemma voids_fwd_length_le_dx: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n2 ≤ |L2|.
28 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
32 lemma voids_fwd_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
33 |L1| + n2 = |L2| + n1.
34 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
35 /2 width=2 by injective_plus_r/
38 lemma voids_fwd_length_minus: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
39 |L1| - n1 = |L2| - n2.
40 /3 width=3 by voids_fwd_length, voids_fwd_length_le_dx, voids_fwd_length_le_sn, plus_to_minus_2/ qed-.
42 lemma voids_inj_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
43 |L1| = |L2| → n1 = n2.
44 #L1 #L2 #n1 #n2 #H #HL12
45 lapply (voids_fwd_length … H) -H #H
46 /2 width=2 by injective_plus_l/
49 (* Inversion lemmas with length for local environments **********************)
51 lemma voids_inv_void_dx_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2.ⓧ → |L1| ≤ |L2| →
52 ∃∃m2. ⓧ*[n1]L1 ≋ ⓧ*[m2]L2 & n2 = ⫯m2 & n1 ≤ m2.
53 #L1 #L2 #n1 #n2 #H #HL12
54 lapply (voids_fwd_length … H) normalize >plus_n_Sm #H0
55 lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
56 elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
57 /3 width=4 by voids_inv_void_dx, ex3_intro/