From: Ferruccio Guidi Date: Wed, 10 Feb 2016 19:02:11 +0000 (+0000) Subject: first commit for lreq ... X-Git-Tag: make_still_working~644 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=bb6e68b2cf746bb3108543807207a1ca628ab442 first commit for lreq ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc new file mode 100644 index 000000000..5099ffa1a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc @@ -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/substitution/drop.ma". +include "basic_2/substitution/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* alternative definition of lpx_sn *) +definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝ + λR,L1,L2. |L1| = |L2| ∧ + (∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2 + ). + +(* Basic forward lemmas ******************************************************) + +lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H // +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆. +#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H +normalize /2 width=1 by length_inv_zero_sn/ +qed-. + +lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. +#R #I1 #L2 #K1 #V1 #H elim H -H +#H #IH elim (length_inv_pos_sn … H) -H +#I2 #K2 #V2 #HK12 #H destruct +elim (IH I1 I2 K1 K2 V1 V2 0) // +#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12 +@conj // -HK12 +#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH +/2 width=1 by drop_drop, conj/ +qed-. + +lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆. +#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H +normalize /2 width=1 by length_inv_zero_dx/ +qed-. + +lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. +#R #I2 #L1 #K2 #V2 #H elim H -H +#H #IH elim (length_inv_pos_dx … H) -H +#I1 #K1 #V1 #HK12 #H destruct +elim (IH I1 I2 K1 K2 V1 V2 0) // +#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12 +@conj // -HK12 +#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH +/2 width=1 by drop_drop, conj/ +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆). +#R @conj // +#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1 +#H destruct +qed. + +lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2. + lpx_sn_alt R L1 L2 → R L1 V1 V2 → + lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2). +#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H +#HL12 #IH @conj // +#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i +[ #HLK1 #HLK2 + lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct + lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct + /2 width=1 by conj/ +| -HL12 -HV12 /3 width=6 by drop_inv_drop1/ +| #H lapply (drop_fwd_Y2 … H) -H + #H elim (ylt_yle_false … H) -H // +] +qed. + +(* Main properties **********************************************************) + +theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2. +#R #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/ +qed. + +(* Main inversion lemmas ****************************************************) + +theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2. +#R #L1 elim L1 -L1 +[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H // +| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/ +] +qed-. + +(* alternative definition of lpx_sn *****************************************) + +lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| → + (∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2 + ) → lpx_sn R L1 L2. +/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed. + +lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 → + |L1| = |L2| ∧ + ∀I1,I2,K1,K2,V1,V2,i. + ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R K1 V1 V2. +#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H +#H elim H -H /3 width=4 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma deleted file mode 100644 index 5099ffa1a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma +++ /dev/null @@ -1,127 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/substitution/drop.ma". -include "basic_2/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* alternative definition of lpx_sn *) -definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝ - λR,L1,L2. |L1| = |L2| ∧ - (∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2 - ). - -(* Basic forward lemmas ******************************************************) - -lemma lpx_sn_alt_fwd_length: ∀R,L1,L2. lpx_sn_alt R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H // -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lpx_sn_alt_inv_atom1: ∀R,L2. lpx_sn_alt R (⋆) L2 → L2 = ⋆. -#R #L2 #H lapply (lpx_sn_alt_fwd_length … H) -H -normalize /2 width=1 by length_inv_zero_sn/ -qed-. - -lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. -#R #I1 #L2 #K1 #V1 #H elim H -H -#H #IH elim (length_inv_pos_sn … H) -H -#I2 #K2 #V2 #HK12 #H destruct -elim (IH I1 I2 K1 K2 V1 V2 0) // -#H #HV12 destruct @(ex3_2_intro … K2 V2) // -HV12 -@conj // -HK12 -#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH -/2 width=1 by drop_drop, conj/ -qed-. - -lemma lpx_sn_alt_inv_atom2: ∀R,L1. lpx_sn_alt R L1 (⋆) → L1 = ⋆. -#R #L1 #H lapply (lpx_sn_alt_fwd_length … H) -H -normalize /2 width=1 by length_inv_zero_dx/ -qed-. - -lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. -#R #I2 #L1 #K2 #V2 #H elim H -H -#H #IH elim (length_inv_pos_dx … H) -H -#I1 #K1 #V1 #HK12 #H destruct -elim (IH I1 I2 K1 K2 V1 V2 0) // -#H #HV12 destruct @(ex3_2_intro … K1 V1) // -HV12 -@conj // -HK12 -#J1 #J2 #L1 #L2 #W1 #W2 #i #HKL1 #HKL2 elim (IH J1 J2 L1 L2 W1 W2 (⫯i)) -IH -/2 width=1 by drop_drop, conj/ -qed-. - -(* Basic properties *********************************************************) - -lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆). -#R @conj // -#I1 #I2 #K1 #K2 #V1 #V2 #i #HLK1 elim (drop_inv_atom1 … HLK1) -HLK1 -#H destruct -qed. - -lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2. - lpx_sn_alt R L1 L2 → R L1 V1 V2 → - lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2). -#R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H -#HL12 #IH @conj // -#I1 #I2 #K1 #K2 #W1 #W2 #i @(ynat_ind … i) -i -[ #HLK1 #HLK2 - lapply (drop_inv_O2 … HLK1) -HLK1 #H destruct - lapply (drop_inv_O2 … HLK2) -HLK2 #H destruct - /2 width=1 by conj/ -| -HL12 -HV12 /3 width=6 by drop_inv_drop1/ -| #H lapply (drop_fwd_Y2 … H) -H - #H elim (ylt_yle_false … H) -H // -] -qed. - -(* Main properties **********************************************************) - -theorem lpx_sn_lpx_sn_alt: ∀R,L1,L2. lpx_sn R L1 L2 → lpx_sn_alt R L1 L2. -#R #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by lpx_sn_alt_atom, lpx_sn_alt_pair/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem lpx_sn_alt_inv_lpx_sn: ∀R,L1,L2. lpx_sn_alt R L1 L2 → lpx_sn R L1 L2. -#R #L1 elim L1 -L1 -[ #L2 #H lapply (lpx_sn_alt_inv_atom1 … H) -H // -| #L1 #I #V1 #IH #X #H elim (lpx_sn_alt_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct /3 width=1 by lpx_sn_pair/ -] -qed-. - -(* alternative definition of lpx_sn *****************************************) - -lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| → - (∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2 - ) → lpx_sn R L1 L2. -/4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed. - -lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 → - |L1| = |L2| ∧ - ∀I1,I2,K1,K2,V1,V2,i. - ⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R K1 V1 V2. -#R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H -#H elim H -H /3 width=4 by conj/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc new file mode 100644 index 000000000..f69814078 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc @@ -0,0 +1,58 @@ +definition dropable_dx: predicate (relation lenv) ≝ + λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → + ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2. + +lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). +#R #HR #L1 #L2 #H elim H -L2 +[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2 + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2 + #K #HLK #HK2 elim (IHL1 … HLK) -L + /3 width=5 by step, ex2_intro/ +] +qed-. + + +fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k +[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). +/2 width=5 by lpx_sn_dropable_aux/ qed-. + +lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. + +lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma deleted file mode 100644 index f69814078..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma +++ /dev/null @@ -1,58 +0,0 @@ -definition dropable_dx: predicate (relation lenv) ≝ - λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → - ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2. - -lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). -#R #HR #L1 #L2 #H elim H -L2 -[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2 - /3 width=3 by inj, ex2_intro/ -| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2 - #K #HLK #HK2 elim (IHL1 … HLK) -L - /3 width=5 by step, ex2_intro/ -] -qed-. - - -fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k -[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). -/2 width=5 by lpx_sn_dropable_aux/ qed-. - -lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc new file mode 100644 index 000000000..031c12c96 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +definition lpx_sn_confluent: relation (relation3 lenv term term) ≝ λR1,R2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. + +definition lpx_sn_transitive: relation (relation3 lenv term term) ≝ λR1,R2. + ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → + ∀T2. R2 L2 T T2 → R1 L1 T1 T2. + +(* Main properties **********************************************************) + +theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). +#R #HR #L1 #L #H elim H -L1 -L // +#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H +elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5 by lpx_sn_pair/ +qed-. + +theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → + confluent2 … (lpx_sn R1) (lpx_sn R2). +#R1 #R2 #HR12 #L0 @(ynat_f_ind … length … L0) -L0 #x #IH * +[ #_ #X1 #H1 #X2 #H2 -x + >(lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/ +| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct + elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH /2 width=2 by ylt_succ2_refl/ #L #HL1 #HL2 + elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lpx_sn_pair, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc new file mode 100644 index 000000000..23eaab6ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). +#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 +[ /2 width=1 by lpx_sn_refl/ +| /3 width=1 by TC_reflexive, lpx_sn_refl/ +| /3 width=5 by lpx_sn_pair, step/ +] +qed-. + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. lpx_sn (LTC … R) L1 L2 → + TC … (lpx_sn R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → + ∀S:relation lenv. + S (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → + S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. +#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 +[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // +| #L2 #I #V2 #IHL2 #X #H + elim (TC_lpx_sn_inv_pair2 … H) // -H -HR + #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + lpx_sn (LTC … R) L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc deleted file mode 100644 index b9493ad4b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc +++ /dev/null @@ -1,195 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/ynat/ynat_lt.ma". -include "basic_2/notation/relations/midiso_4.ma". -include "basic_2/grammar/lenv_length.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -inductive lreq: relation4 ynat ynat lenv lenv ≝ -| lreq_atom: ∀l,m. lreq l m (⋆) (⋆) -| lreq_zero: ∀I1,I2,L1,L2,V1,V2. - lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 → - lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m. - lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -. - -interpretation - "equivalence (local environment)" - 'MidIso l m L1 L2 = (lreq l m L1 L2). - -(* Basic properties *********************************************************) - -lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m → - L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V. -#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/ -qed. - -lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l → - L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/ -qed. - -lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → - ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V. -#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 // -qed. - -lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L. -#L elim L -L // -#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ] -#Hl destruct /2 width=1 by lreq_succ/ -#m elim (ynat_cases … m) [| * #x ] -#Hm destruct /2 width=1 by lreq_zero, lreq_pair/ -qed. - -lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2. -#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] -* // [1,3: #L2 #I2 #V2 ] #l -[ #H elim (ysucc_inv_O_sn … H) -| >length_pair >length_pair #H - lapply (ysucc_inv_inj … H) -H #HL12 - elim (ynat_cases l) /3 width=1 by lreq_zero/ - * /3 width=1 by lreq_succ/ -| #H elim (ysucc_inv_O_dx … H) -] -qed. - -lemma lreq_sym: ∀l,m. symmetric … (lreq l m). -#l #m #L1 #L2 #H elim H -L1 -L2 -l -m -/2 width=1 by lreq_zero, lreq_pair, lreq_succ/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 #l #m * -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct -| #I #L1 #L2 #V #m #_ #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct -] -qed-. - -lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆. -/2 width=5 by lreq_inv_atom1_aux/ qed-. - -fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 → - ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct - /2 width=5 by ex2_3_intro/ -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H - elim (ysucc_inv_O_dx … H) -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 → - ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=9 by lreq_inv_zero1_aux/ qed-. - -fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J #K1 #W #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct - /2 width=3 by ex2_intro/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V. -/2 width=6 by lreq_inv_pair1_aux/ qed-. - -lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m → - ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2. -#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H // -#Y #HL12 #H destruct /2 width=1 by and3_intro/ -qed-. - -fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l → - ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct - /2 width=5 by ex2_3_intro/ -] -qed-. - -lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l → - ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=5 by lreq_inv_succ1_aux/ qed-. - -lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆. -/3 width=3 by lreq_inv_atom1, lreq_sym/ -qed-. - -lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l → - L1 ⩬[⫰l, m] L2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H // -#Z #Y #X #HL12 #H destruct // -qed-. - -lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 → - ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m → - ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V. -#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H -/3 width=3 by lreq_sym, ex2_intro/ -qed-. - -lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l → - ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -qed-. - -(* Advanced inversion lemmas ************************************************) - -fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct -| /4 width=1 by eq_f3, ysucc_inv_Y_dx/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2. -/2 width=5 by lreq_inv_O_Y_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma new file mode 100644 index 000000000..e2c7c0aff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 f ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEq $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma deleted file mode 100644 index 0cd902ba8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 T , break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'LazyEq $T $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma deleted file mode 100644 index 20297e517..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 f , break term 46 m ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'MidIso $f $k $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma deleted file mode 100644 index 6015011d4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 R , break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'RelationStar $R $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma new file mode 100644 index 000000000..698b130c3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'RelationStar $R1 $R2 $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 38fd8e785..0bed76cfd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -13,144 +13,147 @@ (**************************************************************************) include "ground_2/relocation/nstream_sle.ma". -include "basic_2/notation/relations/relationstar_4.ma". +include "basic_2/notation/relations/relationstar_5.ma". include "basic_2/grammar/lenv.ma". (* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) -inductive lexs (R:relation4 bool lenv term term): rtmap → relation lenv ≝ -| lexs_atom: ∀f. lexs R f (⋆) (⋆) +inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ +| lexs_atom: ∀f. lexs RN RP f (⋆) (⋆) | lexs_next: ∀I,L1,L2,V1,V2,f. - lexs R f L1 L2 → R (Ⓣ) L1 V1 V2 → - lexs R (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) + lexs RN RP f L1 L2 → RN L1 V1 V2 → + lexs RN RP (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) | lexs_push: ∀I,L1,L2,V1,V2,f. - lexs R f L1 L2 → R (Ⓕ) L1 V1 V2 → - lexs R (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) + lexs RN RP f L1 L2 → RP L1 V1 V2 → + lexs RN RP (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) . interpretation "general entrywise extension (local environment)" - 'RelationStar R f L1 L2 = (lexs R f L1 L2). + 'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2). (* Basic inversion lemmas ***************************************************) -fact lexs_inv_atom1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → X = ⋆ → Y = ⋆. -#R #X #Y #f * -X -Y -f // +fact lexs_inv_atom1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → X = ⋆ → Y = ⋆. +#RN #RP #X #Y #f * -X -Y -f // #I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom1 *) -lemma lexs_inv_atom1: ∀R,Y,f. ⋆ ⦻*[R, f] Y → Y = ⋆. +lemma lexs_inv_atom1: ∀RN,RP,Y,f. ⋆ ⦻*[RN, RP, f] Y → Y = ⋆. /2 width=6 by lexs_inv_atom1_aux/ qed-. -fact lexs_inv_next1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & Y = K2.ⓑ{J}W2. -#R #X #Y #f * -X -Y -f +fact lexs_inv_next1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K1 #W1 #g #H destruct -| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct /2 width=5 by ex3_2_intro/ | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_push_next … H) ] qed-. (* Basic_2A1: includes lpx_sn_inv_pair1 *) -lemma lexs_inv_next1: ∀R,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[R, ⫯g] Y → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & Y = K2.ⓑ{J}W2. +lemma lexs_inv_next1: ∀RN,RP,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RN, RP, ⫯g] Y → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2. /2 width=7 by lexs_inv_next1_aux/ qed-. -fact lexs_inv_push1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & Y = K2.ⓑ{J}W2. -#R #X #Y #f * -X -Y -f +fact lexs_inv_push1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K1 #W1 #g #H destruct | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_next_push … H) -| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lexs_inv_push1: ∀R,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[R, ↑g] Y → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & Y = K2.ⓑ{J}W2. +lemma lexs_inv_push1: ∀RN,RP,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RN, RP, ↑g] Y → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & Y = K2.ⓑ{J}W2. /2 width=7 by lexs_inv_push1_aux/ qed-. -fact lexs_inv_atom2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → Y = ⋆ → X = ⋆. -#R #X #Y #f * -X -Y -f // +fact lexs_inv_atom2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → Y = ⋆ → X = ⋆. +#RN #RP #X #Y #f * -X -Y -f // #I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom2 *) -lemma lexs_inv_atom2: ∀R,X,f. X ⦻*[R, f] ⋆ → X = ⋆. +lemma lexs_inv_atom2: ∀RN,RP,X,f. X ⦻*[RN, RP, f] ⋆ → X = ⋆. /2 width=6 by lexs_inv_atom2_aux/ qed-. -fact lexs_inv_next2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & X = K1.ⓑ{J}W1. -#R #X #Y #f * -X -Y -f +fact lexs_inv_next2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & X = K1.ⓑ{J}W1. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K2 #W2 #g #H destruct -| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct /2 width=5 by ex3_2_intro/ | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_push_next … H) ] qed-. (* Basic_2A1: includes lpx_sn_inv_pair2 *) -lemma lexs_inv_next2: ∀R,J,X,K2,W2,g. X ⦻*[R, ⫯g] K2.ⓑ{J}W2 → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & X = K1.ⓑ{J}W1. +lemma lexs_inv_next2: ∀RN,RP,J,X,K2,W2,g. X ⦻*[RN, RP, ⫯g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & X = K1.ⓑ{J}W1. /2 width=7 by lexs_inv_next2_aux/ qed-. -fact lexs_inv_push2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & X = K1.ⓑ{J}W1. -#R #X #Y #f * -X -Y -f +fact lexs_inv_push2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & X = K1.ⓑ{J}W1. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K2 #W2 #g #H destruct | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_next_push … H) -| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lexs_inv_push2: ∀R,J,X,K2,W2,g. X ⦻*[R, ↑g] K2.ⓑ{J}W2 → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & X = K1.ⓑ{J}W1. +lemma lexs_inv_push2: ∀RN,RP,J,X,K2,W2,g. X ⦻*[RN, RP, ↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & X = K1.ⓑ{J}W1. /2 width=7 by lexs_inv_push2_aux/ qed-. (* Basic_2A1: includes lpx_sn_inv_pair *) -lemma lexs_inv_next: ∀R,I1,I2,L1,L2,V1,V2,f. - L1.ⓑ{I1}V1 ⦻*[R, ⫯f] (L2.ⓑ{I2}V2) → - ∧∧ L1 ⦻*[R, f] L2 & R (Ⓣ) L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H +lemma lexs_inv_next: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RN, RP, ⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RN, RP, f] L2 & RN L1 V1 V2 & I1 = I2. +#RN #RP #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H #L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ qed-. -lemma lexs_inv_push: ∀R,I1,I2,L1,L2,V1,V2,f. - L1.ⓑ{I1}V1 ⦻*[R, ↑f] (L2.ⓑ{I2}V2) → - ∧∧ L1 ⦻*[R, f] L2 & R (Ⓕ) L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H +lemma lexs_inv_push: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RN, RP, ↑f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RN, RP, f] L2 & RP L1 V1 V2 & I1 = I2. +#RN #RP #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H #L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ qed-. (* Basic properties *********************************************************) -lemma lexs_eq_repl_back: ∀R,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[R, f] L2). -#R #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // -[ #I #L1 #L2 #V1 #v2 #f1 #_ #HS #IH #f2 #H elim (next_inv_sn … H) -H /3 width=1 by lexs_next/ -| #I #L1 #L2 #V1 #v2 #f1 #_ #HO #IH #f2 #H elim (push_inv_sn … H) -H /3 width=1 by lexs_push/ +lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RN, RP, f] L2). +#RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // +#I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H +[ elim (next_inv_sn … H) -H /3 width=1 by lexs_next/ +| elim (push_inv_sn … H) -H /3 width=1 by lexs_push/ ] qed-. -lemma lexs_eq_repl_fwd: ∀R,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[R, f] L2). -#R #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) +lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[RN, RP, f] L2). +#RN #RP #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) qed-. +(* Note: fexs_sym and fexs_trans hold, but lexs_sym and lexs_trans do not *) (* Basic_2A1: includes: lpx_sn_refl *) -lemma lexs_refl: ∀R,f. - (∀b,L. reflexive … (R b L)) → - reflexive … (lexs R f). -#R #f #HR #L generalize in match f; -f elim L -L // +lemma lexs_refl: ∀RN,RP,f. + (∀L. reflexive … (RN L)) → + (∀L. reflexive … (RP L)) → + reflexive … (lexs RN RP f). +#RN #RP #f #HRN #HRP #L generalize in match f; -f elim L -L // #L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/ qed. -lemma sle_lexs_trans: ∀R. (∀L,T1,T2. R (Ⓣ) L T1 T2 → R (Ⓕ) L T1 T2) → - ∀L1,L2,f2. L1 ⦻*[R, f2] L2 → - ∀f1. f1 ⊆ f2 → L1 ⦻*[R, f1] L2. -#R #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) → + ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2. +#RN #RP #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // #I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH [ * * [2: #n1 ] ] #f1 #H [ /4 width=5 by lexs_next, sle_inv_SS_aux/ @@ -160,10 +163,10 @@ lemma sle_lexs_trans: ∀R. (∀L,T1,T2. R (Ⓣ) L T1 T2 → R (Ⓕ) L T1 T2) ] qed-. -lemma sle_lexs_conf: ∀R. (∀L,T1,T2. R (Ⓕ) L T1 T2 → R (Ⓣ) L T1 T2) → - ∀L1,L2,f1. L1 ⦻*[R, f1] L2 → - ∀f2. f1 ⊆ f2 → L1 ⦻*[R, f2] L2. -#R #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) → + ∀L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. f1 ⊆ f2 → L1 ⦻*[RN, RP, f2] L2. +#RN #RP #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // #I #L1 #L2 #V1 #V2 #f1 #_ #HV12 #IH [2: * * [2: #n2 ] ] #f2 #H [ /4 width=5 by lexs_next, sle_inv_OS_aux/ @@ -173,10 +176,11 @@ lemma sle_lexs_conf: ∀R. (∀L,T1,T2. R (Ⓕ) L T1 T2 → R (Ⓣ) L T1 T2) → ] qed-. -lemma lexs_co: ∀R1,R2. - (∀b,L1,T1,T2. R1 b L1 T1 T2 → R2 b L1 T1 T2) → - ∀L1,L2,f. L1 ⦻*[R1, f] L2 → L1 ⦻*[R2, f] L2. -#R1 #R2 #HR #L1 #L2 #f #H elim H -L1 -L2 -f +lemma lexs_co: ∀RN1,RP1,RN2,RP2. + (∀L1,T1,T2. RN1 L1 T1 T2 → RN2 L1 T1 T2) → + (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) → + ∀L1,L2,f. L1 ⦻*[RN1, RP1, f] L2 → L1 ⦻*[RN2, RP2, f] L2. +#RN1 #RP1 #RN2 #RP2 #HRN #HRP #L1 #L2 #f #H elim H -L1 -L2 -f /3 width=1 by lexs_atom, lexs_next, lexs_push/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index c3626ee27..c8d3536de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -20,6 +20,6 @@ include "basic_2/relocation/lexs.ma". (* Forward lemmas on length for local environments **************************) (* Basic_2A1: includes: lpx_sn_fwd_length *) -lemma lexs_fwd_length: ∀R,L1,L2,f. L1 ⦻*[R, f] L2 → |L1| = |L2|. -#R #L1 #L2 #f #H elim H -L1 -L2 -f // +lemma lexs_fwd_length: ∀RN,RP,L1,L2,f. L1 ⦻*[RN, RP, f] L2 → |L1| = |L2|. +#RM #RP #L1 #L2 #f #H elim H -L1 -L2 -f // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma new file mode 100644 index 000000000..568dad1ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lazyeq_3.ma". +include "basic_2/grammar/ceq.ma". +include "basic_2/relocation/lexs.ma". + +(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) + +(* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *) +definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq cfull. + +interpretation + "ranged equivalence (local environment)" + 'LazyEq f L1 L2 = (lreq f L1 L2). + +(* Basic properties *********************************************************) + +lemma lreq_eq_repl_back: ∀L1,L2. eq_stream_repl_back … (λf. L1 ≡[f] L2). +/2 width=3 by lexs_eq_repl_back/ qed-. + +lemma lreq_eq_repl_fwd: ∀L1,L2. eq_stream_repl_fwd … (λf. L1 ≡[f] L2). +/2 width=3 by lexs_eq_repl_fwd/ qed-. + +lemma sle_lreq_trans: ∀L1,L2,f2. L1 ≡[f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ≡[f1] L2. +/2 width=3 by sle_lexs_trans/ qed-. + +(* Basic_2A1: includes: lreq_refl *) +lemma lreq_refl: ∀f. reflexive … (lreq f). +/2 width=1 by lexs_refl/ qed. + +(* Basic_2A1: includes: lreq_sym *) +lemma lreq_sym: ∀f. symmetric … (lreq f). +#f #L1 #L2 #H elim H -L1 -L2 -f +/2 width=1 by lexs_next, lexs_push/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: includes: lreq_inv_atom1 *) +lemma lreq_inv_atom1: ∀Y,f. ⋆ ≡[f] Y → Y = ⋆. +/2 width=4 by lexs_inv_atom1/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair1 *) +lemma lreq_inv_next1: ∀J,K1,Y,W1,g. K1.ⓑ{J}W1 ≡[⫯g] Y → + ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓑ{J}W1. +#J #K1 #Y #W1 #g #H elim (lexs_inv_next1 … H) -H /2 width=3 by ex2_intro/ +qed-. + +(* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *) +lemma lreq_inv_push1: ∀J,K1,Y,W1,g. K1.ⓑ{J}W1 ≡[↑g] Y → + ∃∃K2,W2. K1 ≡[g] K2 & Y = K2.ⓑ{J}W2. +#J #K1 #Y #W1 #g #H elim (lexs_inv_push1 … H) -H /2 width=4 by ex2_2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_atom2 *) +lemma lreq_inv_atom2: ∀X,f. X ≡[f] ⋆ → X = ⋆. +/2 width=4 by lexs_inv_atom2/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair2 *) +lemma lreq_inv_next2: ∀J,X,K2,W2,g. X ≡[⫯g] K2.ⓑ{J}W2 → + ∃∃K1. K1 ≡[g] K2 & X = K1.ⓑ{J}W2. +#J #X #K2 #W2 #g #H elim (lexs_inv_next2 … H) -H /2 width=3 by ex2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *) +lemma lreq_inv_push2: ∀J,X,K2,W2,g. X ≡[↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ≡[g] K2 & X = K1.ⓑ{J}W1. +#J #X #K2 #W2 #g #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair *) +lemma lreq_inv_next: ∀I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ≡[⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ≡[f] L2 & V1 = V2 & I1 = I2. +/2 width=1 by lexs_inv_next/ qed-. + +(* Basic_2A1: includes: lreq_inv_succ *) +lemma lreq_inv_push: ∀I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ≡[↑f] (L2.ⓑ{I2}V2) → + L1 ≡[f] L2 ∧ I1 = I2. +#I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push … H) -H /2 width=1 by conj/ +qed-. + +(* Basic_2A1: removed theorems 5: + lreq_pair_lt lreq_succ_lt lreq_pair_O_Y lreq_O2 lreq_inv_O_Y +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma new file mode 100644 index 000000000..1b932c460 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lexs_length.ma". +include "basic_2/relocation/lreq.ma". + +(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) + +(* Forward lemmas on length for local environments **************************) + +(* Basic_2A1: includes: lreq_fwd_length *) +lemma lreq_fwd_length: ∀L1,L2,f. L1 ≡[f] L2 → |L1| = |L2|. +/2 width=4 by lexs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma deleted file mode 100644 index 031c12c96..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma +++ /dev/null @@ -1,48 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -definition lpx_sn_confluent: relation (relation3 lenv term term) ≝ λR1,R2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. - -definition lpx_sn_transitive: relation (relation3 lenv term term) ≝ λR1,R2. - ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → - ∀T2. R2 L2 T T2 → R1 L1 T1 T2. - -(* Main properties **********************************************************) - -theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). -#R #HR #L1 #L #H elim H -L1 -L // -#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H -elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5 by lpx_sn_pair/ -qed-. - -theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → - confluent2 … (lpx_sn R1) (lpx_sn R2). -#R1 #R2 #HR12 #L0 @(ynat_f_ind … length … L0) -L0 #x #IH * -[ #_ #X1 #H1 #X2 #H2 -x - >(lpx_sn_inv_atom1 … H1) -X1 - >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/ -| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct - elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH /2 width=2 by ylt_succ2_refl/ #L #HL1 #HL2 - elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lpx_sn_pair, ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma deleted file mode 100644 index 23eaab6ab..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma +++ /dev/null @@ -1,119 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on transitive_closure *****************************************) - -lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). -#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 -[ /2 width=1 by lpx_sn_refl/ -| /3 width=1 by TC_reflexive, lpx_sn_refl/ -| /3 width=5 by lpx_sn_pair, step/ -] -qed-. - -lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → - ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → - ∀V1,V2. LTC … R L1 V1 V2 → - TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). -#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // -[ /2 width=1 by TC_lpx_sn_pair_refl/ -| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ -] -qed-. - -lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. lpx_sn (LTC … R) L1 L2 → - TC … (lpx_sn R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ -qed-. - -(* Inversion lemmas on transitive closure ***********************************) - -lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. -#R #L1 #H @(TC_ind_dx … L1 H) -L1 -[ /2 width=2 by lpx_sn_inv_atom2/ -| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ -] -qed-. - -lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 -[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct - lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀S:relation lenv. - S (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → - S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. -#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 -[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // -| #L2 #I #V2 #IHL2 #X #H - elim (TC_lpx_sn_inv_pair2 … H) // -H -HR - #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ -] -qed-. - -lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. -#R #L2 #H elim H -L2 -[ /2 width=2 by lpx_sn_inv_atom1/ -| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ -] -qed-. - -fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 -[ #J #K #W #H destruct -| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. - -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - lpx_sn (LTC … R) L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. - -(* Forward lemmas on transitive closure *************************************) - -lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L2 -[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // -| #L #L2 #_ #HL2 #IHL1 - >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // -] -qed-.