From 8676e97d61b676fac6b740f6e10503672e992c00 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Jan 2014 22:01:30 +0000 Subject: [PATCH] normal forms for extended substitution --- .../notation/relations/psubstnormal_5.ma | 19 ++++ .../lambdadelta/basic_2/reduction/cnr.ma | 11 ++ .../lambdadelta/basic_2/reduction/cnr_lift.ma | 8 -- .../lambdadelta/basic_2/reduction/cnx.ma | 10 ++ .../lambdadelta/basic_2/reduction/cnx_lift.ma | 9 -- .../lambdadelta/basic_2/relocation/cny.ma | 102 ++++++++++++++++++ .../basic_2/relocation/cny_lift.ma | 72 +++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 + 8 files changed, 218 insertions(+), 17 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma new file mode 100644 index 000000000..ebe23f937 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstnormal_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ▶ break [ term 46 d , break term 46 e ] 𝐍 break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'PSubstNormal $G $L $T $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma index 26bb268ee..ad48736fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma @@ -82,6 +82,17 @@ lemma cnr_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐍⦃⋆k⦄. >(cpr_inv_sort1 … H) // qed. +lemma cnr_lref_free: ∀G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. +#G #L #i #Hi #X #H elim (cpr_inv_lref1 … H) -H // * +#K #V1 #V2 #HLK lapply (ldrop_fwd_length_lt2 … HLK) -HLK +#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ +qed. + +(* Basic_1: was only: nf2_csort_lref *) +lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. +#G #L #i #HL @cnr_lref_free >(ldrop_fwd_length … HL) -HL // +qed. + (* Basic_1: was: nf2_abst *) lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄. #a #G #L #W #T #HW #HT #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma index 48fa090bd..217646acf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma @@ -19,14 +19,6 @@ include "basic_2/reduction/cnr.ma". (* Advanced properties ******************************************************) -(* Basic_1: was only: nf2_csort_lref *) -lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. -#G #L #i #HL #X #H -elim (cpr_inv_lref1 … H) -H // * -#K #V1 #V2 #HLK #_ #_ -lapply (ldrop_mono … HL … HLK) -L #H destruct -qed. - (* Basic_1: was: nf2_lref_abst *) lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. #G #L #K #V #i #HLK #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index 61e6e6cc6..47f92caaa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -106,6 +106,16 @@ lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ ➡[h, g] lapply (deg_iter … l Hkl) -Hkl (ldrop_fwd_length … HL) -HL // +qed. + lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}W.T⦄. #h #g #a #G #L #W #T #HW #HT #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma index 65c035f4a..7f3bedbd0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma @@ -17,15 +17,6 @@ include "basic_2/reduction/cnx.ma". (* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) -(* Advanced properties ******************************************************) - -lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄. -#h #g #G #L #i #HL #X #H -elim (cpx_inv_lref1 … H) -H // * -#I #K #V1 #V2 #HLK #_ #_ -lapply (ldrop_mono … HL … HLK) -L #H destruct -qed. - (* Relocation properties ****************************************************) lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⇩[s, d, e] L0 ≡ L → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma new file mode 100644 index 000000000..ed3acca9f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/psubstnormal_5.ma". +include "basic_2/relocation/cpy.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) + +definition cny: ∀d,e. relation3 genv lenv term ≝ + λd,e,G,L. NF … (cpy d e G L) (eq …). + +interpretation + "normality for context-sensitive extended substitution (term)" + 'PSubstNormal G L T d e = (cny d e G L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cny_inv_lref: ∀G,L,d,e,i. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄ → + ∨∨ yinj i < d | d + e ≤ yinj i | |L| ≤ i. +#G #L #d #e #i #H elim (ylt_split i d) /2 width=1 by or3_intro0/ +#Hdi elim (ylt_split i (d+e)) /2 width=1 by or3_intro1/ +#Hide elim (lt_or_ge i (|L|)) /2 width=1 by or3_intro2/ +#Hi elim (ldrop_O1_lt L i) // +#I #K #V #HLK elim (lift_total V 0 (i+1)) +#W #HVW lapply (H W ?) -H /2 width=5 by cpy_subst/ -HLK +#H destruct elim (lift_inv_lref2_be … HVW) -L -d -e // +qed-. + +lemma cny_inv_bind: ∀a,I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄. +#a #I #G #L #V1 #T1 #d #e #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓑ{a,I}V2.T1) ?) -HVT1 +| #T2 #HT2 lapply (HVT1 (ⓑ{a,I}V1.T2) ?) -HVT1 +] +/2 width=1 by cpy_bind/ #H destruct // +qed-. + +lemma cny_inv_flat: ∀I,G,L,V,T,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄ → + ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. +#I #G #L #V1 #T1 #d #e #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓕ{I}V2.T1) ?) -HVT1 +| #T2 #HT2 lapply (HVT1 (ⓕ{I}V1.T2) ?) -HVT1 +] +/2 width=1 by cpy_flat/ #H destruct // +qed-. + +(* Basic properties *********************************************************) + +lemma cny_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃⋆k⦄. +#G #L #d #e #k #X #H elim (cpy_inv_sort1 … H) -H // +qed. + +lemma cny_lref_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hi #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #_ #_ #HLK #_ lapply (ldrop_fwd_length_lt2 … HLK) -HLK +#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ +qed. + +lemma cny_lref_atom: ∀G,L,d,e,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #HL @cny_lref_free >(ldrop_fwd_length … HL) -HL // +qed. + +lemma cny_lref_top: ∀G,L,d,e,i. d+e ≤ yinj i → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hdei #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #_ #H elim (ylt_yle_false … H) // +qed. + +lemma cny_lref_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃#i⦄. +#G #L #d #e #i #Hid #X #H elim (cpy_inv_lref1 … H) -H // * +#I #K #V #H elim (ylt_yle_false … H) // +qed. + +lemma cny_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃§p⦄. +#G #L #d #e #p #X #H elim (cpy_inv_gref1 … H) -H // +qed. + +lemma cny_bind: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → + ∀I,T. ⦃G, L.ⓑ{I}V⦄ ⊢ ▶[⫯d, e] 𝐍⦃T⦄ → + ∀a. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓑ{a,I}V.T⦄. +#G #L #V1 #d #e #HV1 #I #T1 #HT1 #a #X #H +elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct +>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // +qed. + +lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → + ∀T. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → + ∀I. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃ⓕ{I}V.T⦄. +#G #L #V1 #d #e #HV1 #T1 #HT1 #I #X #H +elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct +>(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma new file mode 100644 index 000000000..d3f2f5ffc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/cpy_lift.ma". +include "basic_2/relocation/cny.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION *****************) + +(* Properties on relocation *************************************************) + +lemma cny_lift_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdetd #U2 #HU12 +elim (cpy_inv_lift1_le … HU12 … HLK … HTU1) // -L -Hdetd #T2 #HT12 +>(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +lemma cny_lift_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt ≤ d → yinj d ≤ dt + et → ⦃G, L⦄ ⊢ ▶[dt, et+e] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hdtd #Hddet #U2 #HU12 +elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hdtd -Hddet #T2 +>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +lemma cny_lift_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → d ≤ dt → ⦃G, L⦄ ⊢ ▶[dt+e, et] 𝐍⦃U⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HT1 #HLK #HTU1 #Hddt #U2 #HU12 +elim (cpy_inv_lift1_ge … HU12 … HLK … HTU1) /2 width=1 by monotonic_yle_plus_dx/ -L -Hddt #T2 +>yplus_minus_inj #HT12 >(HT1 … HT12) -K /2 width=5 by lift_mono/ +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma cny_lift_inv_le: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt + et ≤ d → ⦃G, K⦄ ⊢ ▶[dt, et] 𝐍⦃T⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdetd #T2 #HT12 +elim (lift_total T2 d e) #U2 #HTU2 +lapply (cpy_lift_le … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hdetd #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. + +lemma cny_lift_inv_be: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → dt ≤ d → yinj d + e ≤ dt + et → ⦃G, K⦄ ⊢ ▶[dt, et-e] 𝐍⦃T⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdtd #Hdedet #T2 #HT12 +lapply (yle_fwd_plus_ge_inj … Hdedet) // #Heet +elim (yle_inv_plus_inj2 … Hdedet) -Hdedet #Hddete #Hedet +elim (lift_total T2 d e) #U2 #HTU2 +lapply (cpy_lift_be … HT12 … HLK … HTU1 … HTU2 ? ?) // [ >yplus_minus_assoc_inj // ] -K -Hdtd -Hddete +>ymax_pre_sn // -Heet #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. + +lemma cny_lift_inv_ge: ∀G,L,K,T,U,s,d,dt,e,et. ⦃G, L⦄ ⊢ ▶[dt, et] 𝐍⦃U⦄ → ⇩[s, d, e] L ≡ K → + ⇧[d, e] T ≡ U → yinj d + e ≤ dt → ⦃G, K⦄ ⊢ ▶[dt-e, et] 𝐍⦃T⦄. +#G #L #K #T1 #U1 #s #d #dt #e #et #HU1 #HLK #HTU1 #Hdedt #T2 #HT12 +elim (yle_inv_plus_inj2 … Hdedt) -Hdedt #Hddte #Hedt +elim (lift_total T2 d e) #U2 #HTU2 +lapply (cpy_lift_ge … HT12 … HLK … HTU1 … HTU2 ?) // -K -Hddte +>ymax_pre_sn // -Hedt #HU12 +lapply (HU1 … HU12) -L /2 width=5 by lift_inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 7b7c453e4..9aa3bd04d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -212,6 +212,10 @@ table { [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" + "lleq_ext" * ] } ] + [ { "normal forms for context-sensitive extended substitution" * } { + [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ] + } + ] [ { "contxt-sensitive extended multiple substitution" * } { [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*×[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*×[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } -- 2.39.2