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/arith/nat_le_minus_plus.ma".
16 include "static_2/syntax/lenv_length.ma".
17 include "static_2/syntax/lveq.ma".
19 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
21 (* Properties with length for local environments ****************************)
23 lemma lveq_length_eq: โL1,L2. |L1| = |L2| โ L1 โโง*[๐,๐] L2.
25 [ #Y2 #H >(length_inv_zero_sn โฆ H) -Y2 /2 width=3 by lveq_atom, ex_intro/
27 elim (length_inv_succ_sn โฆ H) -H #I2 #K2 #HK #H destruct
28 /3 width=1 by lveq_bind/
32 (* Forward lemmas with length for local environments ************************)
34 lemma lveq_fwd_length_le_sn: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ n1 โค |L1|.
35 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
36 /2 width=1 by nle_succ_bi/
39 lemma lveq_fwd_length_le_dx: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ n2 โค |L2|.
40 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
41 /2 width=1 by nle_succ_bi/
44 lemma lveq_fwd_length: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
45 โงโง |L1|-|L2| = n1 & |L2|-|L1| = n2.
46 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
48 | #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind //
50 #K1 #K2 #n #_ * #H1 #H2 destruct
51 >length_bind <nminus_succ_dx <nminus_succ_sn
52 /2 width=1 by nle_eq_zero_minus, conj/
55 lemma lveq_length_fwd_sn: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ |L1| โค |L2| โ ๐ = n1.
56 #L1 #L2 #n1 #n2 #H #HL
57 elim (lveq_fwd_length โฆ H) -H
58 >(nle_inv_eq_zero_minus โฆ HL) //
61 lemma lveq_length_fwd_dx: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ |L2| โค |L1| โ ๐ = n2.
62 #L1 #L2 #n1 #n2 #H #HL
63 elim (lveq_fwd_length โฆ H) -H
64 >(nle_inv_eq_zero_minus โฆ HL) //
67 lemma lveq_inj_length: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
68 |L1| = |L2| โ โงโง ๐ = n1 & ๐ = n2.
69 #L1 #L2 #n1 #n2 #H #HL
70 elim (lveq_fwd_length โฆ H) -H
71 >HL -HL /2 width=1 by conj/
74 lemma lveq_fwd_length_plus: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
75 |L1| + n2 = |L2| + n1.
76 #L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 //
77 #k1 #K2 #n #_ #IH <nplus_succ_dx //
80 lemma lveq_fwd_length_eq: โL1,L2. L1 โโง*[๐,๐] L2 โ |L1| = |L2|.
81 /3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-.
83 lemma lveq_fwd_length_minus: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2 โ
84 |L1| - n1 = |L2| - n2.
85 /3 width=3 by lveq_fwd_length_plus, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, nminus_plus_swap/ qed-.
87 lemma lveq_fwd_abst_bind_length_le: โI1,I2,L1,L2,V1,n1,n2.
88 L1.โ[I1]V1 โโง*[n1,n2] L2.โ[I2] โ |L1| โค |L2|.
89 #I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
90 lapply (lveq_fwd_pair_sn โฆ HL) #H destruct
91 elim (lveq_fwd_length โฆ HL) -HL >length_bind >length_bind
92 <nminus_succ_bi <nminus_succ_bi //
95 lemma lveq_fwd_bind_abst_length_le: โI1,I2,L1,L2,V2,n1,n2.
96 L1.โ[I1] โโง*[n1,n2] L2.โ[I2]V2 โ |L2| โค |L1|.
97 /3 width=6 by lveq_fwd_abst_bind_length_le, lveq_sym/ qed-.
99 (* Inversion lemmas with length for local environments **********************)
101 (**) (* state with m2 โ โn2 *)
102 lemma lveq_inv_void_dx_length: โL1,L2,n1,n2. L1 โโง*[n1,n2] L2.โง โ |L1| โค |L2| โ
103 โโm2. L1 โ โง*[n1,m2] L2 & ๐ = n1 & โm2 = n2.
104 #L1 #L2 #n1 #n2 #H #HL12
105 lapply (lveq_fwd_length_plus โฆ H) >length_bind >nplus_succ_shift #H0
106 lapply (nplus_2_des_le_sn_sn โฆ H0 HL12) -H0 -HL12 #H0
107 elim (nle_inv_succ_sn โฆ H0) -H0 #_ #H0 >H0 in H; -H0 #H
108 elim (lveq_inv_void_succ_dx โฆ H) -H /2 width=3 by ex3_intro/
111 (**) (* state with m1 โ โn1 *)
112 lemma lveq_inv_void_sn_length: โL1,L2,n1,n2. L1.โง โโง*[n1,n2] L2 โ |L2| โค |L1| โ
113 โโm1. L1 โ โง*[m1,n2] L2 & โm1 = n1 & ๐ = n2.
114 #L1 #L2 #n1 #n2 #H #HL
115 lapply (lveq_sym โฆ H) -H #H
116 elim (lveq_inv_void_dx_length โฆ H HL) -H -HL
117 /3 width=4 by lveq_sym, ex3_intro/