From 1c8e230b1d81491b38126900d76201fb84303ced Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 8 Jan 2018 22:44:01 +0100 Subject: [PATCH] work in progress with voids and lveq (was: the most recent voids) --- .../contribs/lambdadelta/basic_2/names.txt | 3 +- .../functions/voidstar_2.ma} | 12 +- .../{rvoidstar_4.ma => voidstareq_4.ma} | 4 +- .../lambdadelta/basic_2/syntax/lenv_length.ma | 2 + .../lambdadelta/basic_2/syntax/lveq.ma | 94 +++++++++++++ .../lambdadelta/basic_2/syntax/lveq_length.ma | 72 ++++++++++ .../lambdadelta/basic_2/syntax/lveq_lveq.ma | 127 ++++++++++++++++++ .../lambdadelta/basic_2/syntax/lveq_voids.ma | 98 ++++++++++++++ .../lambdadelta/basic_2/syntax/voids.ma | 98 +++++++++----- .../basic_2/syntax/voids_length.ma | 68 ++++------ 10 files changed, 491 insertions(+), 87 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{syntax/voids_voids.ma => notation/functions/voidstar_2.ma} (73%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{rvoidstar_4.ma => voidstareq_4.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_lveq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_voids.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index c6ba0e03d..eba318b7e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -24,8 +24,7 @@ f,g : local reference transforming map 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 : diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_voids.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma similarity index 73% rename from matita/matita/contribs/lambdadelta/basic_2/syntax/voids_voids.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma index 5ee9d47d7..4c95b4170 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids_voids.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma @@ -12,12 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/syntax/voids.ma". +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* 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. +notation "hvbox( ⓧ* [ term 46 n ] term 46 L )" + non associative with precedence 46 + for @{ 'VoidStar $n $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rvoidstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/voidstareq_4.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/rvoidstar_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/voidstareq_4.ma index f9b03f68c..77841c6bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rvoidstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/voidstareq_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⓧ* [ term 46 n1 ] term 46 L1 ≋ ⓧ* [ term 46 n2 ] term 46 L2 )" +notation "hvbox( L1 ≋ⓧ* [ break term 46 n1, break term 46 n2 ] break term 46 L2 )" non associative with precedence 45 - for @{ 'RVoidStar $n1 $L1 $n2 $L2 }. + for @{ 'VoidStarEq $L1 $n1 $n2 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma index d2690db96..8b7ccd582 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma @@ -23,6 +23,8 @@ rec definition length L ≝ match L with interpretation "length (local environment)" 'card L = (length L). +definition length2 (L1) (L2): nat ≝ |L1| + |L2|. + (* Basic properties *********************************************************) lemma length_atom: |⋆| = 0. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma new file mode 100644 index 000000000..8cd00ab86 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq.ma @@ -0,0 +1,94 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma new file mode 100644 index 000000000..006f68020 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_length.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_lveq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_lveq.ma new file mode 100644 index 000000000..12b6f0cb6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_lveq.ma @@ -0,0 +1,127 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_voids.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_voids.ma new file mode 100644 index 000000000..88b7f77aa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lveq_voids.ma @@ -0,0 +1,98 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma index ca5c4fc58..854737b4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma @@ -12,52 +12,80 @@ (* *) (**************************************************************************) -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 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 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 +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 length_bind