]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/lveq_lveq.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / lveq_lveq.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "static_2/syntax/lveq_length.ma".
16
17 (* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
18
19 (* Main inversion lemmas ****************************************************)
20
21 theorem lveq_inv_bind: โˆ€K1,K2. K1 โ‰‹โ“ง*[๐ŸŽ,๐ŸŽ] K2 โ†’
22                        โˆ€I1,I2,m1,m2. K1.โ“˜[I1] โ‰‹โ“ง*[m1,m2] K2.โ“˜[I2] โ†’
23                        โˆงโˆง ๐ŸŽ = m1 & ๐ŸŽ = m2.
24 #K1 #K2 #HK #I1 #I2 #m1 #m2 #H
25 lapply (lveq_fwd_length_eq โ€ฆ HK) -HK #HK
26 elim (lveq_inj_length โ€ฆ H) -H /3 width=1 by conj/
27 qed-.
28
29 theorem lveq_inj: โˆ€L1,L2,n1,n2. L1 โ‰‹โ“ง*[n1,n2] L2 โ†’
30                   โˆ€m1,m2. L1 โ‰‹โ“ง*[m1,m2] L2 โ†’
31                   โˆงโˆง n1 = m1 & n2 = m2.
32 #L1 #L2 #n1 #n2 #Hn #m1 #m2 #Hm
33 elim (lveq_fwd_length โ€ฆ Hn) -Hn #H1 #H2 destruct
34 elim (lveq_fwd_length โ€ฆ Hm) -Hm #H1 #H2 destruct
35 /2 width=1 by conj/
36 qed-.
37
38 theorem lveq_inj_void_sn_ge: โˆ€K1,K2. |K2| โ‰ค |K1| โ†’
39                              โˆ€n1,n2. K1 โ‰‹โ“ง*[n1,n2] K2 โ†’
40                              โˆ€m1,m2. K1.โ“ง โ‰‹โ“ง*[m1,m2] K2 โ†’
41                              โˆงโˆง โ†‘n1 = m1 & ๐ŸŽ = m2 & ๐ŸŽ = n2.
42 #L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
43 elim (lveq_fwd_length โ€ฆ Hn) -Hn #H1 #H2 destruct
44 elim (lveq_fwd_length โ€ฆ Hm) -Hm #H1 #H2 destruct
45 >length_bind <nminus_succ_dx
46 <(nminus_succ_sn โ€ฆ HL) <(nle_inv_eq_zero_minus โ€ฆ HL)
47 /2 width=1 by and3_intro/
48 qed-.
49
50 theorem lveq_inj_void_dx_le: โˆ€K1,K2. |K1| โ‰ค |K2| โ†’
51                              โˆ€n1,n2. K1 โ‰‹โ“ง*[n1,n2] K2 โ†’
52                              โˆ€m1,m2. K1 โ‰‹โ“ง*[m1,m2] K2.โ“ง โ†’
53                              โˆงโˆง โ†‘n2 = m2 & ๐ŸŽ = m1 & ๐ŸŽ = n1.
54 /3 width=5 by lveq_inj_void_sn_ge, lveq_sym/ qed-. (* auto: 2x lveq_sym *)