h : sort hierarchy parameter
i,j : local reference depth (de Bruijn's)
k,l : global reference level
-m :
-n : type iterations
+m,n : iterations
o : sort degree parameter (origin)
p,q : binder polarity
r :
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⓧ* [ term 46 n ] term 46 L )"
+ non associative with precedence 46
+ for @{ 'VoidStar $n $L }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⓧ* [ term 46 n1 ] term 46 L1 ≋ ⓧ* [ term 46 n2 ] term 46 L2 )"
- non associative with precedence 45
- for @{ 'RVoidStar $n1 $L1 $n2 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≋ⓧ* [ break term 46 n1, break term 46 n2 ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'VoidStarEq $L1 $n1 $n2 $L2 }.
interpretation "length (local environment)" 'card L = (length L).
+definition length2 (L1) (L2): nat ≝ |L1| + |L2|.
+
(* Basic properties *********************************************************)
lemma length_atom: |⋆| = 0.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/notation/relations/voidstareq_4.ma".
+include "basic_2/syntax/lenv.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+
+inductive lveq: bi_relation nat lenv ≝
+| lveq_atom : lveq 0 (⋆) 0 (⋆)
+| lveq_pair_sn: ∀I1,I2,K1,K2,V1,n. lveq n K1 n K2 →
+ lveq 0 (K1.ⓑ{I1}V1) 0 (K2.ⓘ{I2})
+| lveq_pair_dx: ∀I1,I2,K1,K2,V2,n. lveq n K1 n K2 →
+ lveq 0 (K1.ⓘ{I1}) 0 (K2.ⓑ{I2}V2)
+| lveq_void_sn: ∀K1,K2,n1,n2. lveq n1 K1 n2 K2 →
+ lveq (⫯n1) (K1.ⓧ) n2 K2
+| lveq_void_dx: ∀K1,K2,n1,n2. lveq n1 K1 n2 K2 →
+ lveq n1 K1 (⫯n2) (K2.ⓧ)
+.
+
+interpretation "equivalence up to exclusion binders (local environment)"
+ 'VoidStarEq L1 n1 n2 L2 = (lveq n1 L1 n2 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lveq_refl: ∀L. ∃n. L ≋ⓧ*[n, n] L.
+#L elim L -L /2 width=2 by ex_intro, lveq_atom/
+#L #I * #n #IH cases I -I /3 width=2 by ex_intro, lveq_pair_dx/
+* /4 width=2 by ex_intro, lveq_void_sn, lveq_void_dx/
+qed-.
+
+lemma lveq_sym: bi_symmetric … lveq.
+#n1 #n2 #L1 #L2 #H elim H -L1 -L2 -n1 -n2
+/2 width=2 by lveq_atom, lveq_pair_sn, lveq_pair_dx, lveq_void_sn, lveq_void_dx/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lveq_inv_atom_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ⋆ = L1 → ⋆ = L2 → ∧∧ 0 = n1 & 0 = n2.
+#L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
+[ /2 width=1 by conj/
+|2,3: #I1 #I2 #K1 #K2 #V #n #_ #H1 #H2 destruct
+|4,5: #K1 #K2 #n1 #n2 #_ #H1 #H2 destruct
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lveq_inv_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1, n2] ⋆ → 0 = n1 ∧ 0 = n2.
+/2 width=5 by lveq_inv_atom_aux/ qed-.
+
+fact lveq_inv_void_succ_sn_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀K1,m1. L1 = K1.ⓧ → n1 = ⫯m1 → K1 ≋ ⓧ*[m1, n2] L2.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ #K2 #m2 #H destruct
+| #I1 #I2 #L1 #L2 #V #n #_ #_ #K1 #m1 #H1 #H2 destruct
+| #I1 #I2 #L1 #L2 #V #n #_ #_ #K1 #m1 #H1 #H2 destruct
+| #L1 #L2 #n1 #n2 #HL12 #_ #K1 #m1 #H1 #H2 destruct //
+| #L1 #L2 #n1 #n2 #_ #IH #K1 #m1 #H1 #H2 destruct
+ /3 width=1 by lveq_void_dx/
+]
+qed-.
+
+lemma lveq_inv_void_succ_sn: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[⫯n1, n2] L2 → L1 ≋ ⓧ*[n1, n2] L2.
+/2 width=5 by lveq_inv_void_succ_sn_aux/ qed-.
+
+lemma lveq_inv_void_succ_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, ⫯n2] L2.ⓧ → L1 ≋ ⓧ*[n1, n2] L2.
+/4 width=5 by lveq_inv_void_succ_sn_aux, lveq_sym/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+fact lveq_fwd_pair_sn_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀I,K1,V. K1.ⓑ{I}V = L1 → 0 = n1.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 //
+#K1 #K2 #n1 #n2 #_ #IH #J #L1 #V #H destruct /2 width=4 by/
+qed-.
+
+lemma lveq_fwd_pair_sn: ∀I,K1,L2,V,n1,n2. K1.ⓑ{I}V ≋ⓧ*[n1, n2] L2 → 0 = n1.
+/2 width=8 by lveq_fwd_pair_sn_aux/ qed-.
+
+lemma lveq_fwd_pair_dx: ∀I,L1,K2,V,n1,n2. L1 ≋ⓧ*[n1, n2] K2.ⓑ{I}V → 0 = n2.
+/3 width=6 by lveq_fwd_pair_sn, lveq_sym/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/syntax/lenv_length.ma".
+include "basic_2/syntax/lveq.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+
+lemma lveq_eq_ex: ∀L1,L2. |L1| = |L2| → ∃n. L1 ≋ⓧ*[n, n] L2.
+#L1 elim L1 -L1
+[ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
+| #K1 * [ * | #I1 #V1 ] #IH #Y2 #H
+ elim (length_inv_succ_sn … H) -H * [1,3: * |*: #I2 #V2 ] #K2 #HK #H destruct
+ elim (IH … HK) -IH -HK #n #HK
+ /4 width=3 by lveq_pair_sn, lveq_pair_dx, lveq_void_sn, lveq_void_dx, ex_intro/
+]
+qed-.
+
+(* Forward lemmas with length for local environments ************************)
+
+lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n1 ≤ |L1|.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+/2 width=1 by le_S_S/
+qed-.
+
+lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → n2 ≤ |L2|.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+/2 width=1 by le_S_S/
+qed-.
+
+lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ |L1| + n2 = |L2| + n1.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+/2 width=2 by injective_plus_r/
+qed-.
+
+lemma lveq_fwd_length_eq: ∀L1,L2,n. L1 ≋ⓧ*[n, n] L2 → |L1| = |L2|.
+/3 width=2 by lveq_fwd_length, injective_plus_l/ qed-.
+
+lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ |L1| - n1 = |L2| - n2.
+/3 width=3 by lveq_fwd_length, lveq_fwd_length_le_dx, lveq_fwd_length_le_sn, plus_to_minus_2/ qed-.
+
+lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ |L1| = |L2| → n1 = n2.
+#L1 #L2 #n1 #n2 #H #HL12
+lapply (lveq_fwd_length … H) -H #H
+/2 width=2 by injective_plus_l/
+qed-.
+(*
+(* Inversion lemmas with length for local environments **********************)
+
+lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2.ⓧ → |L1| ≤ |L2| →
+ ∃∃m2. L1 ≋ ⓧ*[n1, m2] L2 & n2 = ⫯m2 & n1 ≤ m2.
+#L1 #L2 #n1 #n2 #H #HL12
+lapply (lveq_fwd_length … H) normalize >plus_n_Sm #H0
+lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
+elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
+/3 width=4 by lveq_inv_void_dx, ex3_intro/
+qed-.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/syntax/lveq_length.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+
+(* Main inversion lemmas ****************************************************)
+
+theorem lveq_inv_pair_sn: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
+ ∀I1,I2,V,m1,m2. K1.ⓑ{I1}V ≋ⓧ*[m1, m2] K2.ⓘ{I2} →
+ ∧∧ 0 = m1 & 0 = m2.
+#K1 #K2 #n #HK #I1 #I2 #V #m1 #m2 #H
+lapply (lveq_fwd_length_eq … HK) -HK #HK
+lapply (lveq_fwd_pair_sn … H) #H0 destruct
+<(lveq_inj_length … H) -H normalize /3 width=1 by conj, eq_f/
+qed-.
+
+theorem lveq_inv_pair_dx: ∀K1,K2,n. K1 ≋ⓧ*[n, n] K2 →
+ ∀I1,I2,V,m1,m2. K1.ⓘ{I1} ≋ⓧ*[m1, m2] K2.ⓑ{I2}V →
+ ∧∧ 0 = m1 & 0 = m2.
+/4 width=8 by lveq_inv_pair_sn, lveq_sym, commutative_and/ qed-.
+(*
+theorem lveq_inv_void_sn: ∀K1,K2,n1,n2. K1 ≋ⓧ*[n1, n2] K2 →
+ ∀m1,m2. K1.ⓧ ≋ⓧ*[m1, m2] K2 →
+ 0 < m1.
+*)
+(*
+theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
+ ∧∧ n1 = m1 & n2 = m2.
+#L1 #L2 @(f2_ind ?? length2 ?? L1 L2) -L1 -L2
+#x #IH #L1 #L2 #Hx #n1 #n2 #H
+generalize in match Hx; -Hx
+cases H -L1 -L2 -n1 -n2
+/2 width=8 by lveq_inv_pair_dx, lveq_inv_pair_sn, lveq_inv_atom/
+#K1 #K2 #n1 #n2 #HK #Hx #m1 #m2 #H destruct
+
+
+
+[ #_ #m1 #m2 #HL -x /2 width=1 by lveq_inv_atom/
+| #I1 #I2 #K1 #K2 #V1 #n #HK #_ #m1 #m2 #H -x
+
+
+
+theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀m1,m2. L1 ≋ⓧ*[m1, m2] L2 →
+ ∧∧ n1 = m1 & n2 = m2.
+#L1 #L2 #n1 #n2 #H @(lveq_ind_voids … H) -H -L1 -L2 -n1 -n2
+[ #n1 #n2 #m1 #m2 #H elim (lveq_inv_voids … H) -H *
+ [ /3 width=1 by voids_inj, conj/ ]
+ #J1 #J2 #K1 #K2 #W #m #_ [ #H #_ | #_ #H ]
+ elim (voids_inv_pair_sn … H) -H #H #_
+ elim (voids_atom_inv … H) -H #H #_ destruct
+]
+#I1 #I2 #L1 #L2 #V #n1 #n2 #n #HL #IH #m1 #m2 #H
+elim (lveq_inv_voids … H) -H *
+[1,4: [ #H #_ | #_ #H ]
+ elim (voids_inv_atom_sn … H) -H #H #_
+ elim (voids_pair_inv … H) -H #H #_ destruct
+]
+#J1 #J2 #K1 #K2 #W #m #HK [1,3: #H1 #H2 |*: #H2 #H1 ]
+elim (voids_inv_pair_sn … H1) -H1 #H #Hnm
+[1,4: -IH -Hnm elim (voids_pair_inv … H) -H #H1 #H2 destruct
+|2,3: elim (voids_inv_pair_dx … H2) -H2 #H2 #_
+
+ elim (IH … HK)
+
+
+(*
+/3 width=3 by lveq_inv_atom, lveq_inv_voids/
+|
+ lapply (lveq_inv_voids … H) -H #H
+ elim (lveq_inv_pair_sn … H) -H * /2 width=1 by conj/
+ #Y2 #y2 #HY2 #H1 #H2 #H3 destruct
+*)
+
+(*
+fact lveq_inv_pair_bind_aux: ∀L1,L2,n1,n2. L1 ≋ ⓧ*[n1, n2] L2 →
+ ∀I1,I2,K1,K2,V1. K1.ⓑ{I1}V1 = L1 → K2.ⓘ{I2} = L2 →
+ ∨∨ ∃∃m. K1 ≋ ⓧ*[m, m] K2 & 0 = n1 & 0 = n2
+ | ∃∃m1,m2. K1 ≋ ⓧ*[m1, m2] K2 &
+ BUnit Void = I2 & ⫯m2 = n2.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
+|2,3: #I1 #I2 #K1 #K2 #V #n #HK #_ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
+|4,5: #K1 #K2 #n1 #n2 #HK #IH #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
+ /3 width=4 by _/
+]
+qed-.
+
+lemma voids_inv_pair_bind: ∀I1,I2,K1,K2,V1,n1,n2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[n2]K2.ⓘ{I2} →
+ ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
+ | ∃∃m2. ⓧ*[n1]K1.ⓑ{I1}V1 ≋ ⓧ*[m2]K2 &
+ BUnit Void = I2 & ⫯m2 = n2.
+/2 width=5 by voids_inv_pair_bind_aux/ qed-.
+
+fact voids_inv_bind_pair_aux: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
+ ∀I1,I2,K1,K2,V2. K1.ⓘ{I1} = L1 → K2.ⓑ{I2}V2 = L2 →
+ ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
+ | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
+ BUnit Void = I1 & ⫯m1 = n1.
+#L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
+[ #J1 #J2 #L1 #L2 #V1 #H1 #H2 destruct
+|2,3: #I1 #I2 #K1 #K2 #V #n #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=2 by or_introl, ex3_intro/
+|4,5: #K1 #K2 #n1 #n2 #HK #J1 #J2 #L1 #L2 #V2 #H1 #H2 destruct /3 width=3 by or_intror, ex3_intro/
+]
+qed-.
+
+lemma voids_inv_bind_pair: ∀I1,I2,K1,K2,V2,n1,n2. ⓧ*[n1]K1.ⓘ{I1} ≋ ⓧ*[n2]K2.ⓑ{I2}V2 →
+ ∨∨ ∃∃n. ⓧ*[n]K1 ≋ ⓧ*[n]K2 & 0 = n1 & 0 = n2
+ | ∃∃m1. ⓧ*[m1]K1 ≋ ⓧ*[n2]K2.ⓑ{I2}V2 &
+ BUnit Void = I1 & ⫯m1 = n1.
+/2 width=5 by voids_inv_bind_pair_aux/ qed-.
+*)
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/xoa/xoa2.ma".
+include "basic_2/syntax/voids_length.ma".
+include "basic_2/syntax/lveq.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+
+(* Inversion lemmas with extension with exclusion binders *******************)
+
+lemma lveq_inv_voids: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∨∨ ∧∧ ⓧ*[n1]⋆ = L1 & ⓧ*[n2]⋆ = L2
+ | ∃∃I1,I2,K1,K2,V1,n. K1 ≋ⓧ*[n, n] K2 & ⓧ*[n1](K1.ⓑ{I1}V1) = L1 & ⓧ*[n2](K2.ⓘ{I2}) = L2
+ | ∃∃I1,I2,K1,K2,V2,n. K1 ≋ⓧ*[n, n] K2 & ⓧ*[n1](K1.ⓘ{I1}) = L1 & ⓧ*[n2](K2.ⓑ{I2}V2) = L2.
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ /3 width=1 by conj, or3_intro0/
+|2,3: /3 width=9 by or3_intro1, or3_intro2, ex3_6_intro/
+|4,5: #K1 #K2 #n1 #n2 #HK12 * *
+ /3 width=9 by conj, or3_intro0, or3_intro1, or3_intro2, ex3_6_intro/
+]
+qed-.
+
+(* Eliminators with extension with exclusion binders ************************)
+
+lemma lveq_ind_voids: ∀R:bi_relation lenv nat. (
+ ∀n1,n2. R (ⓧ*[n1]⋆) n1 (ⓧ*[n2]⋆) n2
+ ) → (
+ ∀I1,I2,K1,K2,V1,n1,n2,n. K1 ≋ⓧ*[n, n] K2 → R K1 n K2 n →
+ R (ⓧ*[n1]K1.ⓑ{I1}V1) n1 (ⓧ*[n2]K2.ⓘ{I2}) n2
+ ) → (
+ ∀I1,I2,K1,K2,V2,n1,n2,n. K1 ≋ⓧ*[n, n] K2 → R K1 n K2 n →
+ R (ⓧ*[n1]K1.ⓘ{I1}) n1 (ⓧ*[n2]K2.ⓑ{I2}V2) n2
+ ) →
+ ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 → R L1 n1 L2 n2.
+#R #IH1 #IH2 #IH3 #L1 #L2 @(f2_ind ?? length2 ?? L1 L2) -L1 -L2
+#m #IH #L1 #L2 #Hm #n1 #n2 #H destruct
+elim (lveq_inv_voids … H) -H * //
+#I1 #I2 #K1 #K2 #V #n #HK #H1 #H2 destruct
+/4 width=3 by lt_plus/
+qed-.
+
+(*
+
+(* Properties with extension with exclusion binders *************************)
+
+lemma lveq_voids_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀m1. ⓧ*[m1]L1 ≋ⓧ*[m1+n1, n2] L2.
+#L1 #L2 #n1 #n2 #HL12 #m1 elim m1 -m1 /2 width=1 by lveq_void_sn/
+qed-.
+
+lemma lveq_voids_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀m2. L1 ≋ⓧ*[n1, m2+n2] ⓧ*[m2]L2.
+#L1 #L2 #n1 #n2 #HL12 #m2 elim m2 -m2 /2 width=1 by lveq_void_dx/
+qed-.
+
+lemma lveq_voids: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1, n2] L2 →
+ ∀m1,m2. ⓧ*[m1]L1 ≋ⓧ*[m1+n1, m2+n2] ⓧ*[m2]L2.
+/3 width=1 by lveq_voids_dx, lveq_voids_sn/ qed-.
+
+lemma lveq_voids_zero: ∀L1,L2. L1 ≋ⓧ*[0, 0] L2 →
+ ∀n1,n2. ⓧ*[n1]L1 ≋ⓧ*[n1, n2] ⓧ*[n2]L2.
+#L1 #L2 #HL12 #n1 #n2
+>(plus_n_O … n1) in ⊢ (?%???); >(plus_n_O … n2) in ⊢ (???%?);
+/2 width=1 by lveq_voids/ qed-.
+
+(* Inversion lemmas with extension with exclusion binders *******************)
+
+lemma lveq_inv_voids_sn: ∀L1,L2,n1,n2,m1. ⓧ*[m1]L1 ≋ⓧ*[m1+n1, n2] L2 →
+ L1 ≋ⓧ*[n1, n2] L2.
+#L1 #L2 #n1 #n2 #m1 elim m1 -m1 /3 width=1 by lveq_inv_void_sn/
+qed-.
+
+lemma lveq_inv_voids_dx: ∀L1,L2,n1,n2,m2. L1 ≋ⓧ*[n1, m2+n2] ⓧ*[m2]L2 →
+ L1 ≋ⓧ*[n1, n2] L2.
+#L1 #L2 #n1 #n2 #m2 elim m2 -m2 /3 width=1 by lveq_inv_void_dx/
+qed-.
+
+lemma lveq_inv_voids: ∀L1,L2,n1,n2,m1,m2. ⓧ*[m1]L1 ≋ⓧ*[m1+n1, m2+n2] ⓧ*[m2]L2 →
+ L1 ≋ⓧ*[n1, n2] L2.
+/3 width=3 by lveq_inv_voids_dx, lveq_inv_voids_sn/ qed-.
+
+lemma lveq_inv_voids_zero: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ⓧ*[n1, n2] ⓧ*[n2]L2 →
+ L1 ≋ⓧ*[0, 0] L2.
+/2 width=3 by lveq_inv_voids/ qed-.
+
+*)
\ No newline at end of file
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/rvoidstar_4.ma".
+include "basic_2/notation/functions/voidstar_2.ma".
include "basic_2/syntax/lenv.ma".
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
+(* EXTENSION OF A LOCAL ENVIRONMENT WITH EXCLUSION BINDERS ******************)
-inductive voids: bi_relation nat lenv ≝
-| voids_atom : voids 0 (⋆) 0 (⋆)
-| voids_pair_sn: ∀I1,I2,K1,K2,V1,n. voids n K1 n K2 →
- voids 0 (K1.ⓑ{I1}V1) 0 (K2.ⓘ{I2})
-| voids_pair_dx: ∀I1,I2,K1,K2,V2,n. voids n K1 n K2 →
- voids 0 (K1.ⓘ{I1}) 0 (K2.ⓑ{I2}V2)
-| voids_void_sn: ∀K1,K2,n1,n2. voids n1 K1 n2 K2 →
- voids (⫯n1) (K1.ⓧ) n2 K2
-| voids_void_dx: ∀K1,K2,n1,n2. voids n1 K1 n2 K2 →
- voids n1 K1 (⫯n2) (K2.ⓧ)
-.
+rec definition voids (L:lenv) (n:nat) on n: lenv ≝ match n with
+[ O ⇒ L | S m ⇒ (voids L m).ⓧ ].
-interpretation "equivalence up to exclusion binders (local environment)"
- 'RVoidStar n1 L1 n2 L2 = (voids n1 L1 n2 L2).
+interpretation "extension with exclusion binders (local environment)"
+ 'VoidStar n L = (voids L n).
(* Basic properties *********************************************************)
-lemma voids_refl: ∀L. ∃n. ⓧ*[n]L ≋ ⓧ*[n]L.
-#L elim L -L /2 width=2 by ex_intro, voids_atom/
-#L #I * #n #IH cases I -I /3 width=2 by ex_intro, voids_pair_dx/
-* /4 width=2 by ex_intro, voids_void_sn, voids_void_dx/
+lemma voids_zero: ∀L. L = ⓧ*[0]L.
+// qed.
+
+lemma voids_succ: ∀L,n. (ⓧ*[n]L).ⓧ = ⓧ*[⫯n]L.
+// qed.
+
+(* Advanced properties ******************************************************)
+
+lemma voids_next: ∀n,L. ⓧ*[n](L.ⓧ) = ⓧ*[⫯n]L.
+#n elim n -n //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma voids_atom_inv: ∀K,n. ⓧ*[n]K = ⋆ → ∧∧ ⋆ = K & 0 = n.
+#K * /2 width=1 by conj/
+#n <voids_succ #H destruct
qed-.
-lemma voids_sym: bi_symmetric … voids.
-#n1 #n2 #L1 #L2 #H elim H -L1 -L2 -n1 -n2
-/2 width=2 by voids_atom, voids_pair_sn, voids_pair_dx, voids_void_sn, voids_void_dx/
+lemma voids_pair_inv: ∀I,K1,K2,V,n. ⓧ*[n]K1 = K2.ⓑ{I}V →
+ ∧∧ K2.ⓑ{I}V = K1 & 0 = n.
+#I #K1 #K2 #V * /2 width=1 by conj/
+#n <voids_succ #H destruct
qed-.
-(* Advanced Inversion lemmas ************************************************)
-
-fact voids_inv_void_dx_aux: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
- ∀K2,m2. n2 = ⫯m2 → L2 = K2.ⓧ → ⓧ*[n1]L1 ≋ ⓧ*[m2]K2.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
-[ #K2 #m2 #H destruct
-| #I1 #I2 #L1 #L2 #V #n #_ #_ #K2 #m2 #H destruct
-| #I1 #I2 #L1 #L2 #V #n #_ #_ #K2 #m2 #H destruct
-| #L1 #L2 #n1 #n2 #_ #IH #K2 #m2 #H1 #H2 destruct
- /3 width=1 by voids_void_sn/
-| #L1 #L2 #n1 #n2 #HL12 #_ #K2 #m2 #H1 #H2 destruct //
+(* Advanced inversion lemmas ************************************************)
+
+lemma voids_inv_atom_sn: ∀n1,K2,n2. ⓧ*[n1]⋆ = ⓧ*[n2]K2 →
+ ∧∧ ⓧ*[n1-n2]⋆ = K2 & n2 ≤ n1.
+#n1 elim n1 -n1
+[ #K2 <voids_zero * /2 width=1 by conj/
+ #n1 <voids_succ #H destruct
+| #n1 #IH #K2 *
+ [ <voids_zero #H destruct /2 width=1 by conj/
+ | #n2 <voids_succ <voids_succ >minus_S_S #H
+ elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
+ elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
+ ]
]
qed-.
-lemma voids_inv_void_dx: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[⫯n2]L2.ⓧ → ⓧ*[n1]L1 ≋ ⓧ*[n2]L2.
-/2 width=5 by voids_inv_void_dx_aux/ qed-.
+lemma voids_inv_pair_sn: ∀I,V,n1,K1,K2,n2. ⓧ*[n1]K1.ⓑ{I}V = ⓧ*[n2]K2 →
+ ∧∧ ⓧ*[n1-n2]K1.ⓑ{I}V = K2 & n2 ≤ n1.
+#I #V #n1 elim n1 -n1
+[ #K1 #K2 <voids_zero * /2 width=1 by conj/
+ #n1 <voids_succ #H destruct
+| #n1 #IH #K1 #K2 *
+ [ <voids_zero #H destruct /2 width=1 by conj/
+ | #n2 <voids_succ <voids_succ >minus_S_S #H
+ elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
+ elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
+ ]
+]
+qed-.
+
+(* Main inversion properties ************************************************)
+
+theorem voids_inj: ∀n. injective … (λL. ⓧ*[n]L).
+#n elim n -n //
+#n #IH #L1 #L2
+<voids_succ <voids_succ #H
+elim (destruct_lbind_lbind_aux … H) -H (**) (* destruct lemma needed *)
+/2 width=1 by/
+qed-.
include "basic_2/syntax/lenv_length.ma".
include "basic_2/syntax/voids.ma".
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
-
-(* Forward lemmas with length for local environments ************************)
-
-lemma voids_fwd_length_le_sn: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n1 ≤ |L1|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=1 by le_S_S/
-qed-.
-
-lemma voids_fwd_length_le_dx: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 → n2 ≤ |L2|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=1 by le_S_S/
-qed-.
-
-lemma voids_fwd_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
- |L1| + n2 = |L2| + n1.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=2 by injective_plus_r/
-qed-.
-
-lemma voids_fwd_length_minus: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
- |L1| - n1 = |L2| - n2.
-/3 width=3 by voids_fwd_length, voids_fwd_length_le_dx, voids_fwd_length_le_sn, plus_to_minus_2/ qed-.
-
-lemma voids_inj_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
- |L1| = |L2| → n1 = n2.
-#L1 #L2 #n1 #n2 #H #HL12
-lapply (voids_fwd_length … H) -H #H
-/2 width=2 by injective_plus_l/
-qed-.
-
-(* Inversion lemmas with length for local environments **********************)
-
-lemma voids_inv_void_dx_length: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2.ⓧ → |L1| ≤ |L2| →
- ∃∃m2. ⓧ*[n1]L1 ≋ ⓧ*[m2]L2 & n2 = ⫯m2 & n1 ≤ m2.
-#L1 #L2 #n1 #n2 #H #HL12
-lapply (voids_fwd_length … H) normalize >plus_n_Sm #H0
-lapply (plus2_inv_le_sn … H0 HL12) -H0 -HL12 #H0
-elim (le_inv_S1 … H0) -H0 #m2 #Hm2 #H0 destruct
-/3 width=4 by voids_inv_void_dx, ex3_intro/
+(* EXTENSION OF A LOCAL ENVIRONMENT WITH EXCLUSION BINDERS ******************)
+
+(* Properties with length for local environments ****************************)
+
+lemma length_void: ∀L,n. n+|L| = |ⓧ*[n]L|.
+#L #n elim n -n //
+#n #IH <voids_succ >length_bind <IH -IH //
+qed.
+
+lemma length_void_le: ∀L,n. |L| ≤ |ⓧ*[n]L|.
+// qed.
+
+(* Main forward properties with length for local environments ***************)
+
+theorem voids_inj_length: ∀n1,n2,L1,L2. ⓧ*[n1]L1 = ⓧ*[n2]L2 →
+ |L1| = |L2| → n1 = n2 ∧ L1 = L2.
+#n1 elim n1 -n1
+[ * /2 width=1 by conj/ #n2 #L1 #L2 | #n1 #IH * [ | #n2 ] #L1 #L2 ]
+[ <voids_zero #H destruct
+ <length_void <commutative_plus #H
+ elim (plus_xSy_x_false … H)
+| <voids_zero #H destruct
+ <length_void <commutative_plus #H
+ elim (plus_xSy_x_false … (sym_eq … H))
+| <voids_succ <voids_succ #H #HL12
+ elim (destruct_lbind_lbind_aux … H) -H (**) (* destruct lemma needed *)
+ #H #_ elim (IH … H HL12) -IH -H -HL12 /2 width=1 by conj/
+]
qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/syntax/voids.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
-
-(* Main inversion lemmas ****************************************************)
-
-theorem voids_inj: ∀L1,L2,n1,n2. ⓧ*[n1]L1 ≋ ⓧ*[n2]L2 →
- ∀m1,m2. ⓧ*[m1]L1 ≋ ⓧ*[m2]L2 →
- ∧∧ n1 = m1 & n2 = m2.
projects / helm.git / commitdiff