From: Ferruccio Guidi Date: Sun, 5 May 2013 18:16:14 +0000 (+0000) Subject: - partial commit (just the components before computation) X-Git-Tag: make_still_working~1162 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0679e5d5a305a43a8b4b01a5ac4c7caffacc73b9;p=helm.git - partial commit (just the components before computation) - we park head normal forms for the moment - some refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lbotr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lbotr.etc new file mode 100644 index 000000000..df6b2c11e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lbotr.etc @@ -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/relocation/lsubr_lbotr.ma". +include "basic_2/relocation/ldrop_ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Inversion lemmas about local env. full refinement for substitution *******) + +(* Note: ldrop_ldrop not needed *) +lemma lbotr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ⊒[d, e] L → + d ≤ i → i < d + e → I = Abbr. +#I #L elim L -L +[ #K #V #i #H + lapply (ldrop_inv_atom1 … H) -H #H destruct +| #L #J #W #IHL #K #V #i #H + elim (ldrop_inv_O1 … H) -H * + [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct + lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct + lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H + elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct // + | #Hi #HLK #d @(nat_ind_plus … d) -d + [ #e #H #_ #Hide + elim (lbotr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct + @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/ + | #d #_ #e #H #Hdi #Hide + lapply (lbotr_inv_skip … H ?) -H // #HL + @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/ + ] + ] +] +qed-. + +(* Properties about local env. full refinement for substitution *************) + +(* Note: ldrop_ldrop not needed *) +lemma lbotr_ldrop: ∀L,d,e. + (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) → + ⊒[d, e] L. +#L elim L -L // +#L #I #V #IHL #d @(nat_ind_plus … d) -d +[ #e @(nat_ind_plus … e) -e // + #e #_ #H0 + >(H0 I L V 0 ? ? ?) // + /5 width=6 by lbotr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) +| #d #_ #e #H0 + /5 width=6 by lbotr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) +] +qed. + +lemma lbotr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 → + dd + ee ≤ d → ⊒[dd, ee] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee +@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 +lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid +elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H +elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct +@(lbotr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 // +qed. + +lemma lbotr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → + ∀dd,ee. ⊒[dd, ee] L1 → + dd ≤ d + e → d + e ≤ dd + ee → + ⊒[d, dd + ee - d - e] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee +@lbotr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2 +lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie +>commutative_plus in Hiddee; >minus_minus_comm commutative_plus // -Hddie /2 width=1/ +qed. + +lemma lbotr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 → + d + e ≤ dd → ⊒[dd - e, ee] L2. +#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee +@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 +elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd +>plus_minus in Hiddee; // #Hiddee +lapply (transitive_le … Hdde Hddi) -Hdde #Hid +lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2 +@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lpx.etc new file mode 100644 index 000000000..d23ed28e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ldrop_lpx.etc @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_px.ma". +include "basic_2/relocation/ldrop.ma". + +(* DROPPING *****************************************************************) + +(* Properties on pointwise extension ****************************************) + +lemma lpx_deliftable_dropable: ∀R. t_deliftable_sn R → dropable_sn (lpx R). +#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5/ +] +qed. + +lemma lpx_liftable_dedropable: ∀R. reflexive ? R → + t_liftable R → dedropable_sn (lpx R). +#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ +| #K1 #I #V1 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ +| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 + elim (IHLK1 … HK12) -K1 /3 width=5/ +| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 /3 width=5/ +] +qed. + +fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L2 → + d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx R K1 K2. +#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e +[ #d #e #X #H >(lpx_inv_atom2 … H) -H /2 width=3/ +| #K2 #I #V2 #X #H + elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ +| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ + elim (lpx_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ +| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ + >commutative_plus normalize #H destruct +] +qed-. + +lemma lpx_dropable: ∀R. dropable_dx (lpx R). +/2 width=5 by lpx_dropable_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_px.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_px.etc new file mode 100644 index 000000000..ea916e10a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lenv_px.etc @@ -0,0 +1,166 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_append.ma". + +(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************) + +inductive lpx (R:relation term): relation lenv ≝ +| lpx_stom: lpx R (⋆) (⋆) +| lpx_pair: ∀I,K1,K2,V1,V2. + lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_inv_atom1_aux/ qed-. + +fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_inv_pair1_aux/ qed-. + +fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_inv_atom2_aux/ qed-. + +fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L → + ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 normalize +[ #K1 #K2 #HK12 + @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + +lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) → + ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 normalize +[ #K2 #K1 #HK12 + @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct + @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) +] +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). +#R #HR #L elim L -L // /2 width=1/ +qed. + +lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R). +#R #HR #L1 #L2 #H elim H -H // /3 width=1/ +qed. + +lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R). +#R #HR #L1 #L #H elim H -L // +#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H +elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ +qed. + +lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R). +#R #HR #L0 #L1 #H elim H -L1 +[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/ +| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct + elim (IHK01 … HK02) -K0 #K #HK1 #HK2 + elim (HR … HV01 … HV02) -HR -V0 /3 width=5/ +] +qed. + +lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2. +#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ +qed. + +lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L → + ∀L2. lpx R L L2 → lpx (TC … R) L1 L2. +#R #L1 #L #H elim H -L /2 width=1/ +#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H +elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ +qed. + +lemma TC_lpx_pair_dx: ∀R. reflexive ? R → + ∀I,K,V1,V2. TC … R V1 V2 → + TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2). +#R #HR #I #K #V1 #V2 #H elim H -V2 +/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) +qed. + +lemma TC_lpx_pair_sn: ∀R. reflexive ? R → + ∀I,V,K1,K2. TC … (lpx R) K1 K2 → + TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V). +#R #HR #I #V #K1 #K2 #H elim H -K2 +/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) +qed. + +lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. +#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/ +qed. + +lemma lpx_inv_TC: ∀R. reflexive ? R → + ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 /3 width=1/ /3 width=3/ +qed. + +lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 → + lpx R (L1 @@ K1) (L2 @@ K2). +#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc new file mode 100644 index 000000000..99ae801d7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lfprs_ltprs.etc @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/ltprs.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Properties on context-free parallel computation for local environments ***) + +lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄. +/3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc new file mode 100644 index 000000000..f0d631ebb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lift.etc @@ -0,0 +1,25 @@ +definition t_liftable: relation term → Prop ≝ + λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 → + ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2. + +definition t_deliftable_sn: relation term → Prop ≝ + λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2. + +lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R). +#R #HR #T1 #T2 #H elim H -T2 +[ /3 width=7/ +| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2 + elim (lift_total T d e) /3 width=9/ +] +qed. + +lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R). +#R #HR #U1 #U2 #H elim H -U2 +[ #U2 #HU12 #T1 #d #e #HTU1 + elim (HR … HU12 … HTU1) -U1 /3 width=3/ +| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1 + elim (IHU1 … HTU1) -U1 #T #HTU #HT1 + elim (HR … HU2 … HTU) -U /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc new file mode 100644 index 000000000..8655a5e54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr.etc @@ -0,0 +1,198 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'SubEq $L1 $d $e $L2 }. + +include "basic_2/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) + +inductive lsubr: nat → nat → relation lenv ≝ +| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆) +| lsubr_OO: ∀L1,L2. lsubr 0 0 L1 L2 +| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 → + lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV) +| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 → + lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2) +| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2) +. + +interpretation + "local environment refinement (substitution)" + 'SubEq L1 d e L2 = (lsubr d e L1 L2). + +definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R. + ∀L2,s1,s2. R L2 s1 s2 → + ∀L1,d,e. L1 ⊑ [d, e] L2 → R L1 s1 s2. + +(* Basic properties *********************************************************) + +lemma lsubr_bind_eq: ∀L1,L2,e. L1 ⊑ [0, e] L2 → ∀I,V. + L1. ⓑ{I} V ⊑ [0, e + 1] L2.ⓑ{I} V. +#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ +qed. + +lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e → + L1. ⓓV ⊑ [0, e] L2.ⓓV. +#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ⊑ [0, e - 1] L2 → 0 < e → + L1. ⓑ{I}V1 ⊑ [0, e] L2. ⓛV2. +#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ +qed. + +lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ⊑ [d - 1, e] L2 → 0 < d → + ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ⊑ [d, e] L2. ⓑ{I2} V2. +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ +qed. + +lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e → + L1. ⓓV ⊑ [0, e] L2. ⓑ{I}V. +* /2 width=1/ qed. + +lemma lsubr_refl: ∀d,e,L. L ⊑ [d, e] L. +#d elim d -d +[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/ +| #d #IHd #e #L elim L -L // /2 width=1/ +] +qed. + +lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))). +#S #R #HR #L1 #s1 #s2 #H elim H -s2 +[ /3 width=5/ +| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 + lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L1 = ⋆ → + L2 = ⋆ ∨ (d = 0 ∧ e = 0). +#L1 #L2 #d #e * -L1 -L2 -d -e +[ /2 width=1/ +| /3 width=1/ +| #L1 #L2 #W #e #_ #H destruct +| #L1 #L2 #I #W1 #W2 #e #_ #H destruct +| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct +] +qed. + +lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ⊑ [d, e] L2 → + L2 = ⋆ ∨ (d = 0 ∧ e = 0). +/2 width=3/ qed-. + +fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → + ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d → + ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. +#L1 #L2 #d #e * -L1 -L2 -d -e +[ #d #e #I1 #K1 #V1 #H destruct +| #L1 #L2 #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/ +] +qed. + +lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑ [d, e] L2 → 0 < d → + ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. +/2 width=5/ qed-. + +fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L2 = ⋆ → + L1 = ⋆ ∨ (d = 0 ∧ e = 0). +#L1 #L2 #d #e * -L1 -L2 -d -e +[ /2 width=1/ +| /3 width=1/ +| #L1 #L2 #W #e #_ #H destruct +| #L1 #L2 #I #W1 #W2 #e #_ #H destruct +| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct +] +qed. + +lemma lsubr_inv_atom2: ∀L1,d,e. L1 ⊑ [d, e] ⋆ → + L1 = ⋆ ∨ (d = 0 ∧ e = 0). +/2 width=3/ qed-. + +fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → + ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e → + ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV. +#L1 #L2 #d #e * -L1 -L2 -d -e +[ #d #e #K1 #V #H destruct +| #L1 #L2 #K1 #V #_ #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/ +| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct +| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ⊑ [0, e] K2.ⓓV → 0 < e → + ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV. +/2 width=5/ qed-. + +fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → + ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d → + ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1. +#L1 #L2 #d #e * -L1 -L2 -d -e +[ #d #e #I1 #K1 #V1 #H destruct +| #L1 #L2 #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H + elim (lt_zero_false … H) +| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/ +] +qed. + +lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ⊑ [d, e] K2.ⓑ{I2}V2 → 0 < d → + ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1. +/2 width=5/ qed-. + +(* Basic forward lemmas *****************************************************) + +fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → + d = 0 → e = |L1| → |L1| ≤ |L2|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize +[ // +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ⊑ [0, |L1|] L2 → |L1| ≤ |L2|. +/2 width=5/ qed-. + +fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → + d = 0 → e = |L2| → |L2| ≤ |L1|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize +[ // +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ +| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct +] +qed. + +lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ⊑ [0, |L2|] L2 → |L2| ≤ |L1|. +/2 width=5/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc new file mode 100644 index 000000000..b95a19b66 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/lsubr_lbotr.etc @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'SubEqBottom $d $e $L2 }. + +include "basic_2/relocation/lsubr.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) + +(* bottom element of the refinement *) +definition lbotr: nat → nat → predicate lenv ≝ + λd,e. NF_sn … (lsubr d e) (lsubr d e …). + +interpretation + "local environment full refinement (substitution)" + 'SubEqBottom d e L = (lbotr d e L). + +(* Basic properties *********************************************************) + +lemma lbotr_atom: ∀d,e. ⊒[d, e] ⋆. +#d #e #L #H +elim (lsubr_inv_atom2 … H) -H +[ #H destruct // +| * #H1 #H2 destruct // +] +qed. + +lemma lbotr_OO: ∀L. ⊒[0, 0] L. +// qed. + +lemma lbotr_abbr: ∀L,V,e. ⊒[0, e] L → ⊒[0, e + 1] L.ⓓV. +#L #V #e #HL #K #H +elim (lsubr_inv_abbr2 … H ?) -H // (ltpr_inv_atom1 … HL2) -L2 // +qed-. + +lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 → + ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2. +#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/ +#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct +elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/ +qed-. + +lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆. +#L1 #H @(ltprs_ind_dx … H) -L1 // +#L1 #L #HL1 #_ #IHL2 destruct +>(ltpr_inv_atom2 … HL1) -L1 // +qed-. + +lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1. +#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/ +#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct +elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|. +#L1 #L2 #H @(ltprs_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 +>IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc new file mode 100644 index 000000000..1d2db2daf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_alt.etc @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( T1 ➡ ➡ * break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedStarAlt $T1 $T2 }. + +include "basic_2/computation/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +(* alternative definition of ltprs *) +definition ltprsa: relation lenv ≝ lpx tprs. + +interpretation + "context-free parallel computation (environment) alternative" + 'PRedStarAlt L1 L2 = (ltprsa L1 L2). + +(* Basic properties *********************************************************) + +lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2. +/2 width=1/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2. +/2 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc new file mode 100644 index 000000000..a7c320089 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ldrop.etc @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr_ldrop.ma". +include "basic_2/computation/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +lemma ltprs_ldrop_conf: dropable_sn ltprs. +/2 width=3/ qed. + +lemma ldrop_ltprs_trans: dedropable_sn ltprs. +/2 width=3/ qed. + +lemma ltprs_ldrop_trans_O1: dropable_dx ltprs. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc new file mode 100644 index 000000000..7ededf2af --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/ltprs_ltprs.etc @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr_ltpr.ma". +include "basic_2/computation/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +(* Advanced properties ******************************************************) + +lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 → + ∃∃L0. L1 ➡ L0 & L2 ➡* L0. +/3 width=3/ qed. + +(* Main properties **********************************************************) + +theorem ltprs_conf: confluent … ltprs. +/3 width=3/ qed. + +theorem ltprs_trans: Transitive … ltprs. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc new file mode 100644 index 000000000..492b39041 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs.etc @@ -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 *) +(* *) +(**************************************************************************) + +notation "hvbox( T1 ➡ * break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedStar $T1 $T2 }. + +include "basic_2/reducibility/tpr.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Basic_1: includes: pr1_pr0 *) +definition tprs: relation term ≝ TC … tpr. + +interpretation "context-free parallel computation (term)" + 'PRedStar T1 T2 = (tprs T1 T2). + +(* Basic eliminators ********************************************************) + +lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 → + (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) → + ∀T2. T1 ➡* T2 → R T2. +#T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 → + (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) → + ∀T1. T1 ➡* T2 → R T1. +#T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +lemma tprs_refl: reflexive … tprs. +/2 width=1/ qed. + +lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2. +/2 width=1/ qed. + +lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2. +/2 width=3/ qed. + +lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2. +/2 width=3/ qed. + +(* Basic_1: was only: pr1_head_1 *) +lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2 +[1,3: /3 width=1/ +|2,4: #V #V2 #_ #HV2 #IHV1 + @(tprs_strap1 … IHV1) -IHV1 /2 width=1/ +] +qed. + +(* Basic_1: was only: pr1_head_2 *) +lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2 +[1,3: /3 width=1/ +|2,4: #T #T2 #_ #HT2 #IHT1 + @(tprs_strap1 … IHT1) -IHT1 /2 width=1/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k. +#U2 #k #H @(tprs_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU1 destruct +>(tpr_inv_atom1 … HU2) -HU2 // +qed-. + +lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨ + ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2. +#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/ +#U #U2 #_ #HU2 * /3 width=3/ * +#W #T #HW1 #HT1 #H destruct +elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ * +#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc new file mode 100644 index 000000000..d0d173470 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_lift.etc @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_lift.ma". +include "basic_2/computation/tprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Advanced inversion lemmas ************************************************) + +lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 → + ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2. +#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/ +#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct +elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + +lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → + V1 ➡* V2 ∧ T1 ➡* T2. +#a #V1 #V2 #T1 #T2 #H +elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ +qed-. + +(* Relocation properties ****************************************************) + +(* Note: this was missing in basic_1 *) +lemma tprs_lift: t_liftable tprs. +/3 width=7/ qed. + +(* Note: this was missing in basic_1 *) +lemma tprs_inv_lift1: t_deliftable_sn tprs. +/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc new file mode 100644 index 000000000..87a4a71ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tprs_tprs.etc @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_tpr.ma". +include "basic_2/computation/tprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was: pr1_strip *) +lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 → + ∃∃T0. T1 ➡ T0 & T2 ➡* T0. +/3 width=3 by TC_strip1, tpr_conf/ qed. + +(* Main propertis ***********************************************************) + +(* Basic_1: was: pr1_confluence *) +theorem tprs_conf: confluent … tprs. +/3 width=3/ qed. + +(* Basic_1: was: pr1_t *) +theorem tprs_trans: Transitive … tprs. +/2 width=3/ qed. + +(* Basic_1: was: pr1_comp *) +lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 +@(tprs_trans … (②{I}V.T2)) /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc new file mode 100644 index 000000000..6b7892611 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/delift/cprs_delift.etc @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cpr_delift.ma". +include "basic_2/reducibility/cpr_cpr.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties on inverse basic term relocation ******************************) + +(* Note: this should be stated with tprs *) +lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2. +#L #V #T1 #T2 * #T #HT1 #HT2 +@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *) +qed. + +(* Basic_1: was only: pr3_gen_cabbr *) +lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 → + ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 → + ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2. +#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/ +#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 +elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT +elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc new file mode 100644 index 000000000..f42bdf7e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs.etc @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }. + +notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 , term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }. + +include "basic_2/reducibility/fpr.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) + +definition fprs: bi_relation lenv term ≝ bi_TC … fpr. + +interpretation "context-free parallel computation (closure)" + 'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +/2 width=1/ qed. + +lemma fprs_refl: bi_reflexive … fprs. +/2 width=1/ qed. + +lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → + ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → + ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc new file mode 100644 index 000000000..b76637ff7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_aaa.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/cfpr_aaa.ma". +include "basic_2/computation/fprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) + +(* Properties about atomic arity assignment on terms ************************) + +lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → + ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A. +#L1 #T1 #A #HT1 #L2 #T2 #HLT12 +@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc new file mode 100644 index 000000000..9d4d954b8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_cprs.etc @@ -0,0 +1,138 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/fpr_cpr.ma". +include "basic_2/computation/cprs_lfprs.ma". +include "basic_2/computation/lfprs_ltprs.ma". +include "basic_2/computation/lfprs_fprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) + +(* Advanced properties ******************************************************) + +lemma fprs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 → + ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ➡* ⦃L2, ⓕ{I}V2.T2⦄. +#L1 #L2 #T1 #T2 #HT12 @(fprs_ind … HT12) -L2 -T2 /3 width=1/ +#L #L2 #T #T2 #_ #HT2 #IHT2 #V1 #V2 #HV12 #I +lapply (IHT2 … HV12 I) -IHT2 -HV12 /3 width=6/ +qed. + +lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ → + ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ & + U2 = -ⓑ{I}V2.T2. +#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/ +#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct +elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/ +qed-. + +lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ → + ∀d,e,L1. ⇩[d, e] L1 ≡ K1 → + ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 → + ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2. +#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2 +[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 + >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/ +| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2 + elim (lift_total T d e) #U #HTU + elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL + elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → + ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/ +#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct +elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + +lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ → + ∃∃K1,V1. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ & + L1 = K1.ⓑ{I}V1. +#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/ +#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct +elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/ +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b. + ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ & + T = -ⓑ{I}V2.T2. +#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/ +#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct +elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/ +qed-. + +lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ → + ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ & + ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I #K1 #L2 #V1 #T1 #T2 #H #b +elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct +elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/ +qed-. + +lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W. + ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ & + U2 = ⓛ{a}V2.T2. +#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/ +#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct +elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/ +qed-. + +(* Properties on context-sensitive parallel computation for terms ***********) + +lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄. +#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/ +qed. + +(* Forward lemmas on context-sensitive parallel computation for terms *******) + +lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // +#L #L2 #T #T2 #H1 #H2 #IH1 +elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2 +lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/ +qed-. +(* +(* Advanced properties ******************************************************) + +lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → + ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄. +#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I +elim (fpr_inv_all … H) /3 width=4/ +qed. + +(* Advanced forward lemmas **************************************************) + +lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2. +* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H +elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/ + | #T #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T #HV1 #_ #H destruct /3 width=4/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc new file mode 100644 index 000000000..e0c1b3058 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/fprs_fprs.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/fpr_fpr.ma". +include "basic_2/computation/fprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) + +(* Advanced properties ******************************************************) + +lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄. +#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 +/2 width=4/ qed. + +(* Main propertis ***********************************************************) + +theorem fprs_conf: bi_confluent … fprs. +/2 width=4/ qed. + +theorem fprs_trans: bi_transitive … fprs. +/2 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lenv_px_bi.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lenv_px_bi.etc new file mode 100644 index 000000000..931d075ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lenv_px_bi.etc @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************) + +inductive lpx_bi (R:bi_relation lenv term): relation lenv ≝ +| lpx_bi_stom: lpx_bi R (⋆) (⋆) +| lpx_bi_pair: ∀I,K1,K2,V1,V2. + lpx_bi R K1 K2 → R K1 V1 K2 V2 → + lpx_bi R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_bi_inv_atom1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_bi_inv_atom1: ∀R,L2. lpx_bi R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_bi_inv_atom1_aux/ qed-. + +fact lpx_bi_inv_pair1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → + ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_bi R K1 K2 & + R K1 V1 K2 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_bi_inv_pair1: ∀R,I,K1,V1,L2. lpx_bi R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 & + L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_bi_inv_pair1_aux/ qed-. + +fact lpx_bi_inv_atom2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_bi_inv_atom2: ∀R,L1. lpx_bi R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_bi_inv_atom2_aux/ qed-. + +fact lpx_bi_inv_pair2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → + ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 & + L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_bi_inv_pair2: ∀R,I,L1,K2,V2. lpx_bi R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 & + L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_bi_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_bi_fwd_length: ∀R,L1,L2. lpx_bi R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_bi_refl: ∀R. bi_reflexive ? ? R → reflexive … (lpx_bi R). +#R #HR #L elim L -L // /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc new file mode 100644 index 000000000..a5c42ba65 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpr/lfprs_fprs.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/lfpr_fpr.ma". +include "basic_2/computation/fprs_fprs.ma". +include "basic_2/computation/lfprs.ma". + +(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************) + +(* Inversion lemmas on context-free parallel reduction for closures *********) + +lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄. +#L1 #L2 #H @(lfprs_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 #T +lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/ +qed-. + +(* Properties on context-free parallel computation for closures *************) + +lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/ +qed. + +lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +#L1 #L #L2 #T1 #T2 #HL1 #HL2 +lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 width=4/ +qed. +(* +lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc new file mode 100644 index 000000000..f6106d38d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/chnf.etc @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'HdNormal $L $T }. + +include "basic_2/reduction/cpr_tshf.ma". + +(* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************) + +definition chnf: lenv → predicate term ≝ λL. NF … (cpr L) tshf. + +interpretation + "context-sensitive head normality (term)" + 'HdNormal L T = (chnf L T). + +(* Basic inversion lemmas ***************************************************) + +lemma chnf_inv_tshf: ∀L,T. L ⊢ 𝐇𝐍⦃T⦄ → T ≈ T. +normalize /2 width=1/ +qed-. + +(* Basic properties *********************************************************) + +lemma tshf_thnf: ∀T. T ≈ T → ⋆ ⊢ 𝐇𝐍⦃T⦄. +#T #HT #T2 #H elim (cpr_fwd_tshf1 … H) -H // +#H elim H // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/cpr_tshf.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/cpr_tshf.etc new file mode 100644 index 000000000..0fc5e1d0c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/cpr_tshf.etc @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/tshf.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Forward lemmas on same head forms for terms ******************************) + +lemma cpr_fwd_tshf1: ∀L,T1,T2. L ⊢ T1 ➡ T2 → T1 ≈ T1 → + T2 ≈ T1 ∨ (L = ⋆ → ⊥). +#L #T1 #T2 #H elim H -L -T1 -T2 +[ /2 width=1/ +| #L #K #V1 #V2 #W2 #i #HLK #_ #_ #_ #_ + @or_intror #H destruct + lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct +| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #_ #H + elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct /2 width=1/ +| #I #L #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H + elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct + lapply (IHT12 HT1U2) -IHT12 -HT1U2 * #HUT2 /3 width=1/ + lapply (simple_tshf_repl_sn … HUT2 HT1) /3 width=1/ +| #L #V #T #T1 #T2 #_ #_ #_ #H + elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct +| #L #V #T1 #T2 #_ #_ #H + elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct +| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H + elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H + elim (simple_inv_bind … H) +| #a #L #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H + elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H + elim (simple_inv_bind … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc new file mode 100644 index 000000000..583c3f46f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tshf/tshf.etc @@ -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 *) +(* *) +(**************************************************************************) + +notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )" + non associative with precedence 45 + for @{ 'Hom $L $T1 $T2 }. + +notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'HdReducible $L $T }. + +notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'NotHdReducible $L $T }. + +include "basic_2/grammar/term_simple.ma". + +(* SAME HEAD TERM FORMS *****************************************************) + +inductive tshf: relation term ≝ + | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I}) + | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2) + | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2) + | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ → + tshf (ⓐV1. T1) (ⓐV2. T2) +. + +interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2). + +(* Basic properties *********************************************************) + +lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. +#T1 #T2 #H elim H -T1 -T2 /2 width=1/ +qed. + +lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. +#T1 #T2 #H elim H -T1 -T2 // /2 width=1/ +qed. + +lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. +/3 width=2/ qed. + +lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. +#T1 #T2 #H elim H -T1 -T2 // +[ #V1 #V2 #T1 #T2 #H + elim (simple_inv_bind … H) +| #a #V1 #V2 #T1 #T2 #H + elim (simple_inv_bind … H) +] +qed. (**) (* remove from index *) + +lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. +/3 width=3/ qed-. + +(* Basic inversion lemmas ***************************************************) + +fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀a,I,W1,U1. T1 = ⓑ{a,I}W1.U1 → + ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & + (Bind2 a I = Bind2 false Abbr ∨ I = Abst). +#T1 #T2 * -T1 -T2 +[ #J #a #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ +| #b #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ +| #V1 #V2 #T1 #T2 #_ #_ #_ #a #I #W1 #U1 #H destruct +] +qed. + +lemma tshf_inv_bind1: ∀a,I,W1,U1,T2. ⓑ{a,I}W1.U1 ≈ T2 → + ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & + (Bind2 a I = Bind2 false Abbr ∨ I = Abst). +/2 width=5/ qed-. + +fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → + ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & + I = Appl & T2 = ⓐW2. U2. +#T1 #T2 * -T1 -T2 +[ #J #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct +| #a #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct +| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/ +] +qed. + +lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → + ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & + I = Appl & T2 = ⓐW2. U2. +/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma deleted file mode 100644 index ea916e10a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma +++ /dev/null @@ -1,166 +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/grammar/lenv_append.ma". - -(* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************) - -inductive lpx (R:relation term): relation lenv ≝ -| lpx_stom: lpx R (⋆) (⋆) -| lpx_pair: ∀I,K1,K2,V1,V2. - lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_inv_atom1_aux/ qed-. - -fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_inv_pair1_aux/ qed-. - -fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_inv_atom2_aux/ qed-. - -fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_inv_pair2_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 normalize // -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L → - ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2. -#R #L1 elim L1 -L1 normalize -[ #K1 #K2 #HK12 - @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) -| #L1 #I #V1 #IH #K1 #X #H - elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct - elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct - @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) -] -qed-. - -lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) → - ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1. -#R #L2 elim L2 -L2 normalize -[ #K2 #K1 #HK12 - @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) -| #L2 #I #V2 #IH #K2 #X #H - elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct - elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct - @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) -] -qed-. - -(* Basic properties *********************************************************) - -lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). -#R #HR #L elim L -L // /2 width=1/ -qed. - -lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R). -#R #HR #L1 #L2 #H elim H -H // /3 width=1/ -qed. - -lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R). -#R #HR #L1 #L #H elim H -L // -#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H -elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ -qed. - -lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R). -#R #HR #L0 #L1 #H elim H -L1 -[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/ -| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H - elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct - elim (IHK01 … HK02) -K0 #K #HK1 #HK2 - elim (HR … HV01 … HV02) -HR -V0 /3 width=5/ -] -qed. - -lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2. -#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ -qed. - -lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L → - ∀L2. lpx R L L2 → lpx (TC … R) L1 L2. -#R #L1 #L #H elim H -L /2 width=1/ -#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H -elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ -qed. - -lemma TC_lpx_pair_dx: ∀R. reflexive ? R → - ∀I,K,V1,V2. TC … R V1 V2 → - TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2). -#R #HR #I #K #V1 #V2 #H elim H -V2 -/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) -qed. - -lemma TC_lpx_pair_sn: ∀R. reflexive ? R → - ∀I,V,K1,K2. TC … (lpx R) K1 K2 → - TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V). -#R #HR #I #V #K1 #K2 #H elim H -K2 -/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) -qed. - -lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. -#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/ -qed. - -lemma lpx_inv_TC: ∀R. reflexive ? R → - ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 /3 width=1/ /3 width=3/ -qed. - -lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 → - lpx R (L1 @@ K1) (L2 @@ K2). -#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma deleted file mode 100644 index 931d075ab..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_bi.ma +++ /dev/null @@ -1,88 +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/grammar/lenv_length.ma". - -(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************) - -inductive lpx_bi (R:bi_relation lenv term): relation lenv ≝ -| lpx_bi_stom: lpx_bi R (⋆) (⋆) -| lpx_bi_pair: ∀I,K1,K2,V1,V2. - lpx_bi R K1 K2 → R K1 V1 K2 V2 → - lpx_bi R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_bi_inv_atom1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_bi_inv_atom1: ∀R,L2. lpx_bi R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_bi_inv_atom1_aux/ qed-. - -fact lpx_bi_inv_pair1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → - ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx_bi R K1 K2 & - R K1 V1 K2 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_bi_inv_pair1: ∀R,I,K1,V1,L2. lpx_bi R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 & - L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_bi_inv_pair1_aux/ qed-. - -fact lpx_bi_inv_atom2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_bi_inv_atom2: ∀R,L1. lpx_bi R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_bi_inv_atom2_aux/ qed-. - -fact lpx_bi_inv_pair2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → - ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 & - L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_bi_inv_pair2: ∀R,I,L1,K2,V2. lpx_bi R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 & - L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_bi_inv_pair2_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_bi_fwd_length: ∀R,L1,L2. lpx_bi R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 normalize // -qed-. - -(* Basic properties *********************************************************) - -lemma lpx_bi_refl: ∀R. bi_reflexive ? ? R → reflexive … (lpx_bi R). -#R #HR #L elim L -L // /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma deleted file mode 100644 index d7cdcf595..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px_sn.ma +++ /dev/null @@ -1,145 +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/grammar/lenv_append.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -inductive lpx_sn (R:lenv→relation term): relation lenv ≝ -| lpx_sn_stom: lpx_sn R (⋆) (⋆) -| lpx_sn_pair: ∀I,K1,K2,V1,V2. - lpx_sn R K1 K2 → R K1 V1 V2 → - lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -definition lpx_sn_confluent: relation (lenv→relation 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 (lenv→relation 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. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ -] -qed-. - -lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 normalize // -qed-. - -(* Advanced forward lemmas **************************************************) - -lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L → - ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2. -#R #L1 elim L1 -L1 -[ #K1 #K2 #HK12 - @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *) -| #L1 #I #V1 #IH #K1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct - elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct - @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *) -] -qed-. - -lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) → - ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1. -#R #L2 elim L2 -L2 -[ #K2 #K1 #HK12 - @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *) -| #L2 #I #V2 #IH #K2 #X #H - elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct - elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct - @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *) -] -qed-. - -(* Basic properties *********************************************************) - -lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). -#R #HR #L elim L -L // /2 width=1/ -qed-. - -lemma lpx_sn_append: ∀R. l_appendable_sn R → - ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 → - lpx_sn R (L1 @@ K1) (L2 @@ K2). -#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ -qed-. - -(* Advanced properties ******************************************************) - -lemma 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/ -qed-. - -lemma lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → - confluent2 … (lpx_sn R1) (lpx_sn R2). -#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH * -[ #_ #X1 #H1 #X2 #H2 -n - >(lpx_sn_inv_atom1 … H1) -X1 - >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ -| #L0 #I #V0 #Hn #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 normalize // #L #HL1 #HL2 - elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma new file mode 100644 index 000000000..b229526dd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_append.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +inductive lpx_sn (R:lenv→relation term): relation lenv ≝ +| lpx_sn_stom: lpx_sn R (⋆) (⋆) +| lpx_sn_pair: ∀I,K1,K2,V1,V2. + lpx_sn R K1 K2 → R K1 V1 V2 → + lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L → + ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2. +#R #L1 elim L1 -L1 +[ #K1 #K2 #HK12 + @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *) +| #L1 #I #V1 #IH #K1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct + @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. + +lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) → + ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1. +#R #L2 elim L2 -L2 +[ #K2 #K1 #HK12 + @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *) +| #L2 #I #V2 #IH #K2 #X #H + elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct + elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct + @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *) +] +qed-. + +(* Basic properties *********************************************************) + +lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). +#R #HR #L elim L -L // /2 width=1/ +qed-. + +lemma lpx_sn_append: ∀R. l_appendable_sn R → + ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 → + lpx_sn R (L1 @@ K1) (L2 @@ K2). +#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma new file mode 100644 index 000000000..69c010a19 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma @@ -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/grammar/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +definition lpx_sn_confluent: relation (lenv→relation 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 (lenv→relation 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/ +qed-. + +theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → + confluent2 … (lpx_sn R1) (lpx_sn R2). +#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH * +[ #_ #X1 #H1 #X2 #H2 -n + >(lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/ +| #L0 #I #V0 #Hn #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 normalize // #L #HL1 #HL2 + elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma new file mode 100644 index 000000000..fa1234d1a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma @@ -0,0 +1,122 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/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/ +] +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/ +/2 width=1 by TC_lpx_sn_pair/ +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 +[ #L1 #H lapply (lpx_sn_inv_atom2 … H) -H // +| #L1 #L #HL1 #_ #IHL2 destruct + lapply (lpx_sn_inv_atom2 … HL1) -HL1 // +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … 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/ +| #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 #HV2 /3 width=5/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. s_rs_trans … 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/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ #L2 #H lapply (lpx_sn_inv_atom1 … H) -H // +| #L #L2 #_ #HL2 #IHL1 destruct + lapply (lpx_sn_inv_atom1 … HL2) -HL2 // +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … 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/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … 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. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + lpx_sn (LTC … R) L1 L2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 /2 width=1/ +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/grammar/tshf.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma deleted file mode 100644 index a8873c18b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tshf.ma +++ /dev/null @@ -1,86 +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/grammar/term_simple.ma". - -(* SAME HEAD TERM FORMS *****************************************************) - -inductive tshf: relation term ≝ - | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I}) - | tshf_abbr: ∀V1,V2,T1,T2. tshf (-ⓓV1. T1) (-ⓓV2. T2) - | tshf_abst: ∀a,V1,V2,T1,T2. tshf (ⓛ{a}V1. T1) (ⓛ{a}V2. T2) - | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄ → - tshf (ⓐV1. T1) (ⓐV2. T2) -. - -interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2). - -(* Basic properties *********************************************************) - -lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. -#T1 #T2 #H elim H -T1 -T2 /2 width=1/ -qed. - -lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. -#T1 #T2 #H elim H -T1 -T2 // /2 width=1/ -qed. - -lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. -/3 width=2/ qed. - -lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 #H elim H -T1 -T2 // -[ #V1 #V2 #T1 #T2 #H - elim (simple_inv_bind … H) -| #a #V1 #V2 #T1 #T2 #H - elim (simple_inv_bind … H) -] -qed. (**) (* remove from index *) - -lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -/3 width=3/ qed-. - -(* Basic inversion lemmas ***************************************************) - -fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀a,I,W1,U1. T1 = ⓑ{a,I}W1.U1 → - ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & - (Bind2 a I = Bind2 false Abbr ∨ I = Abst). -#T1 #T2 * -T1 -T2 -[ #J #a #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ -| #b #V1 #V2 #T1 #T2 #a #I #W1 #U1 #H destruct /3 width=3/ -| #V1 #V2 #T1 #T2 #_ #_ #_ #a #I #W1 #U1 #H destruct -] -qed. - -lemma tshf_inv_bind1: ∀a,I,W1,U1,T2. ⓑ{a,I}W1.U1 ≈ T2 → - ∃∃W2,U2. T2 = ⓑ{a,I}W2. U2 & - (Bind2 a I = Bind2 false Abbr ∨ I = Abst). -/2 width=5/ qed-. - -fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → - ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & - I = Appl & T2 = ⓐW2. U2. -#T1 #T2 * -T1 -T2 -[ #J #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -| #a #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/ -] -qed. - -lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → - ∃∃W2,U2. U1 ≈ U2 & 𝐒⦃U1⦄ & 𝐒⦃U2⦄ & - I = Appl & T2 = ⓐW2. U2. -/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 6a5b14e62..d53b103c8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -116,10 +116,6 @@ notation "hvbox( T1 . break ⓛ T2 )" left associative with precedence 49 for @{ 'DxAbst $T1 $T2 }. -notation "hvbox( T . break ④ { term 46 I } break { term 46 T1 , break term 46 T2 , break term 46 T3 } )" - non associative with precedence 50 - for @{ 'DxItem4 $T $I $T1 $T2 $T3 }. - notation "hvbox( ♯ { term 46 x } )" non associative with precedence 90 for @{ 'Weight $x }. @@ -132,10 +128,6 @@ notation "hvbox( 𝐒 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Simple $T }. -notation "hvbox( L ⊢ break term 46 T1 ≈ break term 46 T2 )" - non associative with precedence 45 - for @{ 'Hom $L $T1 $T2 }. - notation "hvbox( T1 ≃ break term 46 T2 )" non associative with precedence 45 for @{ 'Iso $T1 $T2 }. @@ -146,14 +138,6 @@ notation "hvbox( ⇧ [ term 46 d , break term 46 e ] break term 46 T1 ≡ break non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. -notation "hvbox( L1 break ⊑ [ term 46 d , break term 46 e ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'SubEq $L1 $d $e $L2 }. - -notation "hvbox( ⊒ [ term 46 d , break term 46 e ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'SubEqBottom $d $e $L2 }. - notation "hvbox( ⇩ [ term 46 e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $e $L1 $L2 }. @@ -196,6 +180,10 @@ notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃ * break ⦃ term 46 L2 non associative with precedence 45 for @{ 'SupTermStar $L1 $T1 $L2 $T2 }. +notation "hvbox( L1 ⊑ break term 46 L2 )" + non associative with precedence 45 + for @{ 'SubEq $L1 $L2 }. + notation "hvbox( L ⊢ break term 46 T1 ▶* break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $L $T1 $T2 }. @@ -258,36 +246,6 @@ notation "hvbox( L ⊢ break 𝐍 ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Normal $L $T }. -(* this might be removed *) -notation "hvbox( 𝐇𝐑 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'HdReducible $T }. - -(* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'HdReducible $L $T }. - -(* this might be removed *) -notation "hvbox( 𝐇𝐈 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'NotHdReducible $T }. - -(* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'NotHdReducible $L $T }. - -(* this might be removed *) -notation "hvbox( 𝐇𝐍 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'HdNormal $T }. - -(* this might be removed *) -notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'HdNormal $L $T }. - notation "hvbox( L ⊢ break term 46 T1 ➡ break term 46 T2 )" non associative with precedence 45 for @{ 'PRed $L $T1 $T2 }. @@ -306,6 +264,10 @@ notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'PRedSnStar $L1 $L2 }. +notation "hvbox( L1 ⊢ ➡➡* break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStarAlt $L1 $L2 }. + notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma deleted file mode 100644 index 839450da3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma +++ /dev/null @@ -1,36 +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/reduction/cpr_tshf.ma". - -(* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************) - -definition chnf: lenv → predicate term ≝ λL. NF … (cpr L) tshf. - -interpretation - "context-sensitive head normality (term)" - 'HdNormal L T = (chnf L T). - -(* Basic inversion lemmas ***************************************************) - -lemma chnf_inv_tshf: ∀L,T. L ⊢ 𝐇𝐍⦃T⦄ → T ≈ T. -normalize /2 width=1/ -qed-. - -(* Basic properties *********************************************************) - -lemma tshf_thnf: ∀T. T ≈ T → ⋆ ⊢ 𝐇𝐍⦃T⦄. -#T #HT #T2 #H elim (cpr_fwd_tshf1 … H) -H // -#H elim H // -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index e6ad7b2ba..421cc97de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -45,16 +45,11 @@ interpretation "context-sensitive parallel reduction (term)" (* Basic properties *********************************************************) -(* Note: it does not hold replacing |L1| with |L2| *) -lemma cpr_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → - ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. +lemma cpr_lsubr_trans: lsubr_trans … cpr. #L1 #T1 #T2 #H elim H -L1 -T1 -T2 [ // | #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi - lapply (ldrop_fwd_O1_length … HLK1) #H2i - elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi - minus_minus_comm >arith_b1 // /4 width=3/ - ] -| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie - elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 -Hie -Hi destruct - | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/ - ] -| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide - elim (le_inv_plus_l … Hdi) #Hdim #Hi - lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1 - elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/ +lemma l_liftable_LTC: ∀R. l_liftable R → l_liftable (LTC … R). +#R #HR #K #T1 #T2 #H elim H -T2 +[ /3 width=9/ +| #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #HTU1 #U2 #HTU2 + elim (lift_total T d e) /4 width=11 by step/ (**) (* auto too slow without trace *) +] +qed. + +lemma l_deliftable_sn_LTC: ∀R. l_deliftable_sn R → l_deliftable_sn (LTC … R). +#R #HR #L #U1 #U2 #H elim H -U2 +[ #U2 #HU12 #K #d #e #HLK #T1 #HTU1 + elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3/ +| #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 + elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 + elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma deleted file mode 100644 index df6b2c11e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lbotr.ma +++ /dev/null @@ -1,94 +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/relocation/lsubr_lbotr.ma". -include "basic_2/relocation/ldrop_ldrop.ma". - -(* DROPPING *****************************************************************) - -(* Inversion lemmas about local env. full refinement for substitution *******) - -(* Note: ldrop_ldrop not needed *) -lemma lbotr_inv_ldrop: ∀I,L,K,V,i. ⇩[0, i] L ≡ K. ⓑ{I}V → ∀d,e. ⊒[d, e] L → - d ≤ i → i < d + e → I = Abbr. -#I #L elim L -L -[ #K #V #i #H - lapply (ldrop_inv_atom1 … H) -H #H destruct -| #L #J #W #IHL #K #V #i #H - elim (ldrop_inv_O1 … H) -H * - [ -IHL #H1 #H2 #d #e #HL #Hdi #Hide destruct - lapply (le_n_O_to_eq … Hdi) -Hdi #H destruct - lapply (HL … (L.ⓓW) ?) -HL /2 width=1/ #H - elim (lsubr_inv_abbr2 … H ?) -H // -Hide #K #_ #H destruct // - | #Hi #HLK #d @(nat_ind_plus … d) -d - [ #e #H #_ #Hide - elim (lbotr_inv_bind … H ?) -H [2: /2 width=2/ ] #HL #H destruct - @(IHL … HLK … HL) -IHL -HLK -HL // /2 width=1/ - | #d #_ #e #H #Hdi #Hide - lapply (lbotr_inv_skip … H ?) -H // #HL - @(IHL … HLK … HL) -IHL -HLK -HL /2 width=1/ - ] - ] -] -qed-. - -(* Properties about local env. full refinement for substitution *************) - -(* Note: ldrop_ldrop not needed *) -lemma lbotr_ldrop: ∀L,d,e. - (∀I,K,V,i. d ≤ i → i < d + e → ⇩[0, i] L ≡ K. ⓑ{I}V → I = Abbr) → - ⊒[d, e] L. -#L elim L -L // -#L #I #V #IHL #d @(nat_ind_plus … d) -d -[ #e @(nat_ind_plus … e) -e // - #e #_ #H0 - >(H0 I L V 0 ? ? ?) // - /5 width=6 by lbotr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) -| #d #_ #e #H0 - /5 width=6 by lbotr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) -] -qed. - -lemma lbotr_ldrop_trans_le: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 → - dd + ee ≤ d → ⊒[dd, ee] L2. -#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee -@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 -lapply (lt_to_le_to_lt … Hiddee Hddee) -Hddee #Hid -elim (ldrop_trans_le … HL12 … HLK2 ?) -L2 /2 width=2/ #X #HLK1 #H -elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K1 #V1 #HK12 #HV21 #H destruct -@(lbotr_inv_ldrop … HLK1 … HL1) -L1 -K1 -V1 // -qed. - -lemma lbotr_ldrop_trans_be_up: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → - ∀dd,ee. ⊒[dd, ee] L1 → - dd ≤ d + e → d + e ≤ dd + ee → - ⊒[d, dd + ee - d - e] L2. -#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hdde #Hddee -@lbotr_ldrop #I #K2 #V2 #i #Hdi #Hiddee #HLK2 -lapply (transitive_le ? ? (i+e)… Hdde ?) -Hdde /2 width=1/ #Hddie ->commutative_plus in Hiddee; >minus_minus_comm commutative_plus // -Hddie /2 width=1/ -qed. - -lemma lbotr_ldrop_trans_ge: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ∀dd,ee. ⊒[dd, ee] L1 → - d + e ≤ dd → ⊒[dd - e, ee] L2. -#L1 #L2 #d #e #HL12 #dd #ee #HL1 #Hddee -@lbotr_ldrop #I #K2 #V2 #i #Hddi #Hiddee #HLK2 -elim (le_inv_plus_l … Hddee) -Hddee #Hdde #Hedd ->plus_minus in Hiddee; // #Hiddee -lapply (transitive_le … Hdde Hddi) -Hdde #Hid -lapply (ldrop_trans_ge … HL12 … HLK2 ?) -L2 // -Hid #HL1K2 -@(lbotr_inv_ldrop … HL1K2 … HL1) -L1 >commutative_plus /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma deleted file mode 100644 index d23ed28e5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx.ma +++ /dev/null @@ -1,68 +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/grammar/lenv_px.ma". -include "basic_2/relocation/ldrop.ma". - -(* DROPPING *****************************************************************) - -(* Properties on pointwise extension ****************************************) - -lemma lpx_deliftable_dropable: ∀R. t_deliftable_sn R → dropable_sn (lpx R). -#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H - elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (lpx_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (HR … HV12 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5/ -] -qed. - -lemma lpx_liftable_dedropable: ∀R. reflexive ? R → - t_liftable R → dedropable_sn (lpx R). -#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e -[ #d #e #X #H >(lpx_inv_atom1 … H) -H /2 width=3/ -| #K1 #I #V1 #X #H - elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ -| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 - elim (IHLK1 … HK12) -K1 /3 width=5/ -| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H - elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (lift_total W2 d e) #V2 #HWV2 - lapply (H2R … HW12 … HWV1 … HWV2) -W1 - elim (IHLK1 … HK12) -K1 /3 width=5/ -] -qed. - -fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L2 → - d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx R K1 K2. -#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e -[ #d #e #X #H >(lpx_inv_atom2 … H) -H /2 width=3/ -| #K2 #I #V2 #X #H - elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/ -| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_ - elim (lpx_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12 ?) -L2 // /3 width=3/ -| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_ - >commutative_plus normalize #H destruct -] -qed-. - -lemma lpx_dropable: ∀R. dropable_dx (lpx R). -/2 width=5 by lpx_dropable_aux/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma index 98a7c7157..41490973f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/grammar/lenv_px_sn.ma". +include "basic_2/grammar/lpx_sn.ma". include "basic_2/relocation/ldrop.ma". (* DROPPING *****************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma index 7e7961eab..909b02125 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma @@ -35,14 +35,6 @@ inductive lift: nat → nat → relation term ≝ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). -definition t_liftable: relation term → Prop ≝ - λR. ∀T1,T2. R T1 T2 → ∀U1,d,e. ⇧[d, e] T1 ≡ U1 → - ∀U2. ⇧[d, e] T2 ≡ U2 → R U1 U2. - -definition t_deliftable_sn: relation term → Prop ≝ - λR. ∀U1,U2. R U1 U2 → ∀T1,d,e. ⇧[d, e] T1 ≡ U1 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & R T1 T2. - (* Basic inversion lemmas ***************************************************) fact lift_inv_refl_O2_aux: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → e = 0 → T1 = T2. @@ -378,24 +370,6 @@ lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇧[d,e] T1 ≡ T2). ] qed. -lemma t_liftable_TC: ∀R. t_liftable R → t_liftable (TC … R). -#R #HR #T1 #T2 #H elim H -T2 -[ /3 width=7/ -| #T #T2 #_ #HT2 #IHT1 #U1 #d #e #HTU1 #U2 #HTU2 - elim (lift_total T d e) /3 width=9/ -] -qed. - -lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R). -#R #HR #U1 #U2 #H elim H -U2 -[ #U2 #HU12 #T1 #d #e #HTU1 - elim (HR … HU12 … HTU1) -U1 /3 width=3/ -| #U #U2 #_ #HU2 #IHU1 #T1 #d #e #HTU1 - elim (IHU1 … HTU1) -U1 #T #HTU #HT1 - elim (HR … HU2 … HTU) -U /3 width=5/ -] -qed-. - (* Basic_1: removed theorems 7: lift_head lift_gen_head lift_weight_map lift_weight lift_weight_add lift_weight_add_O diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma deleted file mode 100644 index 89359533a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr.ma +++ /dev/null @@ -1,194 +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/grammar/lenv_length.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) - -inductive lsubr: nat → nat → relation lenv ≝ -| lsubr_sort: ∀d,e. lsubr d e (⋆) (⋆) -| lsubr_OO: ∀L1,L2. lsubr 0 0 L1 L2 -| lsubr_abbr: ∀L1,L2,V,e. lsubr 0 e L1 L2 → - lsubr 0 (e + 1) (L1. ⓓV) (L2.ⓓV) -| lsubr_abst: ∀L1,L2,I,V1,V2,e. lsubr 0 e L1 L2 → - lsubr 0 (e + 1) (L1. ⓑ{I}V1) (L2. ⓛV2) -| lsubr_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - lsubr d e L1 L2 → lsubr (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2) -. - -interpretation - "local environment refinement (substitution)" - 'SubEq L1 d e L2 = (lsubr d e L1 L2). - -definition lsubr_trans: ∀S. (lenv → relation S) → Prop ≝ λS,R. - ∀L2,s1,s2. R L2 s1 s2 → - ∀L1,d,e. L1 ⊑ [d, e] L2 → R L1 s1 s2. - -(* Basic properties *********************************************************) - -lemma lsubr_bind_eq: ∀L1,L2,e. L1 ⊑ [0, e] L2 → ∀I,V. - L1. ⓑ{I} V ⊑ [0, e + 1] L2.ⓑ{I} V. -#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ -qed. - -lemma lsubr_abbr_lt: ∀L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e → - L1. ⓓV ⊑ [0, e] L2.ⓓV. -#L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma lsubr_abst_lt: ∀L1,L2,I,V1,V2,e. L1 ⊑ [0, e - 1] L2 → 0 < e → - L1. ⓑ{I}V1 ⊑ [0, e] L2. ⓛV2. -#L1 #L2 #I #V1 #V2 #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ -qed. - -lemma lsubr_skip_lt: ∀L1,L2,d,e. L1 ⊑ [d - 1, e] L2 → 0 < d → - ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 ⊑ [d, e] L2. ⓑ{I2} V2. -#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ -qed. - -lemma lsubr_bind_lt: ∀I,L1,L2,V,e. L1 ⊑ [0, e - 1] L2 → 0 < e → - L1. ⓓV ⊑ [0, e] L2. ⓑ{I}V. -* /2 width=1/ qed. - -lemma lsubr_refl: ∀d,e,L. L ⊑ [d, e] L. -#d elim d -d -[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/ -| #d #IHd #e #L elim L -L // /2 width=1/ -] -qed. - -lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (λL. (TC … (R L))). -#S #R #HR #L1 #s1 #s2 #H elim H -s2 -[ /3 width=5/ -| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 - lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/ -] -qed. - -(* Basic inversion lemmas ***************************************************) - -fact lsubr_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L1 = ⋆ → - L2 = ⋆ ∨ (d = 0 ∧ e = 0). -#L1 #L2 #d #e * -L1 -L2 -d -e -[ /2 width=1/ -| /3 width=1/ -| #L1 #L2 #W #e #_ #H destruct -| #L1 #L2 #I #W1 #W2 #e #_ #H destruct -| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct -] -qed. - -lemma lsubr_inv_atom1: ∀L2,d,e. ⋆ ⊑ [d, e] L2 → - L2 = ⋆ ∨ (d = 0 ∧ e = 0). -/2 width=3/ qed-. - -fact lsubr_inv_skip1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → - ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d → - ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. -#L1 #L2 #d #e * -L1 -L2 -d -e -[ #d #e #I1 #K1 #V1 #H destruct -| #L1 #L2 #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/ -] -qed. - -lemma lsubr_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ⊑ [d, e] L2 → 0 < d → - ∃∃I2,K2,V2. K1 ⊑ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=5/ qed-. - -fact lsubr_inv_atom2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → L2 = ⋆ → - L1 = ⋆ ∨ (d = 0 ∧ e = 0). -#L1 #L2 #d #e * -L1 -L2 -d -e -[ /2 width=1/ -| /3 width=1/ -| #L1 #L2 #W #e #_ #H destruct -| #L1 #L2 #I #W1 #W2 #e #_ #H destruct -| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct -] -qed. - -lemma lsubr_inv_atom2: ∀L1,d,e. L1 ⊑ [d, e] ⋆ → - L1 = ⋆ ∨ (d = 0 ∧ e = 0). -/2 width=3/ qed-. - -fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → - ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e → - ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV. -#L1 #L2 #d #e * -L1 -L2 -d -e -[ #d #e #K1 #V #H destruct -| #L1 #L2 #K1 #V #_ #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/ -| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct -| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct -] -qed. - -lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ⊑ [0, e] K2.ⓓV → 0 < e → - ∃∃K1. K1 ⊑ [0, e - 1] K2 & L1 = K1.ⓓV. -/2 width=5/ qed-. - -fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → - ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d → - ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1. -#L1 #L2 #d #e * -L1 -L2 -d -e -[ #d #e #I1 #K1 #V1 #H destruct -| #L1 #L2 #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H - elim (lt_zero_false … H) -| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/ -] -qed. - -lemma lsubr_inv_skip2: ∀I2,L1,K2,V2,d,e. L1 ⊑ [d, e] K2.ⓑ{I2}V2 → 0 < d → - ∃∃I1,K1,V1. K1 ⊑ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1. -/2 width=5/ qed-. - -(* Basic forward lemmas *****************************************************) - -fact lsubr_fwd_length_full1_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → - d = 0 → e = |L1| → |L1| ≤ |L2|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize -[ // -| /2 width=1/ -| /3 width=1/ -| /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct -] -qed. - -lemma lsubr_fwd_length_full1: ∀L1,L2. L1 ⊑ [0, |L1|] L2 → |L1| ≤ |L2|. -/2 width=5/ qed-. - -fact lsubr_fwd_length_full2_aux: ∀L1,L2,d,e. L1 ⊑ [d, e] L2 → - d = 0 → e = |L2| → |L2| ≤ |L1|. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize -[ // -| /2 width=1/ -| /3 width=1/ -| /3 width=1/ -| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct -] -qed. - -lemma lsubr_fwd_length_full2: ∀L1,L2. L1 ⊑ [0, |L2|] L2 → |L2| ≤ |L1|. -/2 width=5/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma deleted file mode 100644 index 26a9530d0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsubr_lbotr.ma +++ /dev/null @@ -1,73 +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/relocation/lsubr.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) - -(* bottom element of the refinement *) -definition lbotr: nat → nat → predicate lenv ≝ - λd,e. NF_sn … (lsubr d e) (lsubr d e …). - -interpretation - "local environment full refinement (substitution)" - 'SubEqBottom d e L = (lbotr d e L). - -(* Basic properties *********************************************************) - -lemma lbotr_atom: ∀d,e. ⊒[d, e] ⋆. -#d #e #L #H -elim (lsubr_inv_atom2 … H) -H -[ #H destruct // -| * #H1 #H2 destruct // -] -qed. - -lemma lbotr_OO: ∀L. ⊒[0, 0] L. -// qed. - -lemma lbotr_abbr: ∀L,V,e. ⊒[0, e] L → ⊒[0, e + 1] L.ⓓV. -#L #V #e #HL #K #H -elim (lsubr_inv_abbr2 … H ?) -H //