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/lveq.ma".
18 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
20 (* Properties with length for local environments ****************************)
22 lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[0, 0] L2.
24 [ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
26 elim (length_inv_succ_sn … H) -H #I2 #K2 #HK #H destruct
27 /3 width=1 by lveq_bind/
31 (* Forward lemmas with length for local environments ************************)
33 lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n1 ≤ |L1|.
34 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
38 lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n2 ≤ |L2|.
39 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
43 lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
44 ∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2.
45 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/
46 #K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/
49 lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L1| ≤ |L2| → 0 = n1.
50 #L1 #L2 #n1 #n2 #H #HL
51 elim (lveq_fwd_length … H) -H
55 lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| → 0 = n2.
56 #L1 #L2 #n1 #n2 #H #HL
57 elim (lveq_fwd_length … H) -H
61 lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
62 |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
63 #L1 #L2 #n1 #n2 #H #HL
64 elim (lveq_fwd_length … H) -H
65 >HL -HL /2 width=1 by conj/
68 lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
69 |L1| + n2 = |L2| + n1.
70 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
71 /2 width=2 by injective_plus_r/
74 lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0, 0] L2 → |L1| = |L2|.
75 /3 width=2 by lveq_fwd_length_plus, injective_plus_l/ qed-.
77 lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
78 |L1| - n1 = |L2| - n2.
79 /3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
81 lemma lveq_fwd_abst_bind_length_le: ∀I1,I2,L1,L2,V1,n1,n2.
82 L1.ⓑ{I1}V1 ≋ⓧ*[n1, n2] L2.ⓘ{I2} → |L1| ≤ |L2|.
83 #I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
84 lapply (lveq_fwd_pair_sn … HL) #H destruct
85 elim (lveq_fwd_length … HL) -HL >length_bind >length_bind //
88 lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
89 L1.ⓘ{I1} ≋ⓧ*[n1, n2] L2.ⓑ{I2}V2 → |L2| ≤ |L1|.
90 /3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
92 (* Inversion lemmas with length for local environments **********************)
94 lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2.ⓧ → |L1| ≤ |L2| →
95 ∃∃m2. L1 ≋ ⓧ*[n1, m2] L2 & 0 = n1 & ↑m2 = n2.
96 #L1 #L2 #n1 #n2 #H #HL12
97 lapply (lveq_fwd_length_plus … H) normalize >plus_n_Sm #H0
98 lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
99 elim (le_inv_S1 … H0) -H0 #m2 #_ #H0 destruct
100 elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
103 lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1, n2] L2 → |L2| ≤ |L1| →
104 ∃∃m1. L1 ≋ ⓧ*[m1, n2] L2 & ↑m1 = n1 & 0 = n2.
105 #L1 #L2 #n1 #n2 #H #HL
106 lapply (lveq_sym … H) -H #H
107 elim (lveq_inv_void_dx_length … H HL) -H -HL
108 /3 width=4 by lveq_sym, ex3_intro/