From: Ferruccio Guidi Date: Mon, 3 Feb 2014 21:57:36 +0000 (+0000) Subject: we start total substitution ... X-Git-Tag: make_still_working~981 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=09f9b390eb43b7dfddd4c8859a2ee7ac09a30aca;p=helm.git we start total substitution ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubsteval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubsteval_6.ma new file mode 100644 index 000000000..360f43d29 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubsteval_6.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 T1 ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PSubstEval $G $L $T1 $T2 $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstevalalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstevalalt_6.ma new file mode 100644 index 000000000..dc32bedc3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubstevalalt_6.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 T1 ▶ ▶ * break [ term 46 d , break term 46 e ] break 𝐍 ⦃ term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'PRedEval $G $L $T1 $T2 $d $e }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma index ed3acca9f..81919dc4b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny.ma @@ -57,6 +57,13 @@ qed-. (* Basic properties *********************************************************) +lemma lsuby_cny_conf: ∀G,d,e. + ∀L1,T. ⦃G, L1⦄ ⊢ ▶[d, e] 𝐍⦃T⦄ → + ∀L2. L1 ⊑×[d, e] L2 → ⦃G, L2⦄ ⊢ ▶[d, e] 𝐍⦃T⦄. +#G #d #e #L1 #T1 #HT1 #L2 #HL12 #T2 #HT12 +@HT1 /3 width=3 by lsuby_cpy_trans/ +qed-. + 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. @@ -100,3 +107,8 @@ lemma cny_flat: ∀G,L,V,d,e. ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃V⦄ → elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct >(HV1 … HV12) -V2 >(HT1 … HT12) -T2 // qed. + +lemma cny_narrow: ∀G,L,T,d1,e1. ⦃G, L⦄ ⊢ ▶[d1, e1] 𝐍⦃T⦄ → + ∀d2,e2. d1 ≤ d2 → d2 + e2 ≤ d1 + e1 → ⦃G, L⦄ ⊢ ▶[d2, e2] 𝐍⦃T⦄. +#G #L #T1 #d1 #e1 #HT1 #d2 #e2 #Hd12 #Hde21 #T2 #HT12 +@HT1 /2 width=5 by cpy_weak/ 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 index d3f2f5ffc..b1acaafaf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cny_lift.ma @@ -70,3 +70,18 @@ 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-. + +(* Advanced properties ******************************************************) + +fact cny_subst_aux: ∀G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → + ⇩[i+1] L ≡ K → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ → + ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄. +#G #L #K #V #W #i #d #e #Hdi #Hide #HLK #HV #HVW +lapply (cny_lift_be … HV … HLK … HVW ? ?) // -HV -HLK -HVW +#HW @(cny_narrow … HW) -HW // +qed-. + +lemma cny_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d + e → + ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ ▶[O, ⫰(d+e-i)] 𝐍⦃V⦄ → + ⇧[O, i+1] V ≡ W → ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃W⦄. +/3 width=13 by cny_subst_aux, ldrop_fwd_drop2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma new file mode 100644 index 000000000..c93e64972 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/psubsteval_6.ma". +include "basic_2/relocation/cny.ma". +include "basic_2/substitution/cpys.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +definition cpye: ynat → ynat → relation4 genv lenv term term ≝ + λd,e,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] T2 ∧ ⦃G, L⦄ ⊢ ▶[d, e] 𝐍⦃T2⦄. + +interpretation "evaluation for context-sensitive extended substitution (term)" + 'PSubstEval G L T1 T2 d e = (cpye d e G L T1 T2). + +(* Basic_properties *********************************************************) + +lemma cpye_sort: ∀G,L,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃⋆k⦄. +/3 width=5 by cny_sort, conj/ qed. + +lemma cpye_free: ∀G,L,d,e,i. |L| ≤ i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_free, conj/ qed. + +lemma cpye_top: ∀G,L,d,e,i. d + e ≤ yinj i → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_top, conj/ qed. + +lemma cpye_skip: ∀G,L,d,e,i. yinj i < d → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃#i⦄. +/3 width=6 by cny_lref_skip, conj/ qed. + +lemma cpye_gref: ∀G,L,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃§p⦄. +/3 width=5 by cny_gref, conj/ qed. + +lemma cpye_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃ⓑ{a,I}V2.T2⦄. +#G #L #V1 #V2 #d #e * #HV12 #HV2 #I #T1 #T2 * +/5 width=8 by cpys_bind, cny_bind, lsuby_cny_conf, lsuby_succ, conj/ +qed. + +lemma cpye_flat: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ → + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃ⓕ{I}V2.T2⦄. +#G #L #V1 #V2 #d #e * #HV12 #HV2 #T1 #T2 * +/3 width=7 by cpys_flat, cny_flat, conj/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.ma new file mode 100644 index 000000000..a14708dfc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye_lift.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/relocation/cny_lift.ma". +include "basic_2/substitution/fqup.ma". +include "basic_2/substitution/cpys_lift.ma". +include "basic_2/substitution/cpye.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE EXTENDED SUBSTITUTION ON TERMS **********) + +lemma cpye_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e → + ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*[O, ⫰(d+e-i)] 𝐍⦃V2⦄ → + ⇧[O, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ▶*[d, e] 𝐍⦃W2⦄. +#I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK * +/4 width=13 by cpys_subst, cny_subst_aux, ldrop_fwd_drop2, conj/ +qed. + +lemma cpys_total: ∀G,L,T1,d,e. ∃T2. ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄. +#G #L #T1 @(fqup_wf_ind_eq … G L T1) -G -L -T1 +#Z #Y #X #IH #G #L * * +[ #k #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ +| #i #HG #HL #HT #d #e destruct + elim (ylt_split i d) /3 width=2 by cpye_skip, ex_intro/ + elim (ylt_split i (d+e)) /3 width=2 by cpye_top, ex_intro/ + elim (lt_or_ge i (|L|)) /3 width=2 by cpye_free, ex_intro/ + #Hi #Hide #Hdi elim (ldrop_O1_lt L i) // -Hi + #I #K #V1 #HLK elim (IH G K V1 … 0 (⫰(d+e-i))) -IH /2 width=2 by fqup_lref/ + #V2 elim (lift_total V2 0 (i+1)) /3 width=8 by ex_intro, cpye_subst/ +| #p #HG #HL #HT #d #e destruct -IH /2 width=2 by ex_intro/ +| #a #I #V1 #T1 #HG #HL #HT #d #e destruct + elim (IH G L V1 … d e) // elim (IH G (L.ⓑ{I}V1) T1 … (⫯d) e) // + /3 width=2 by cpye_bind, ex_intro/ +| #I #V1 #T1 #HG #HL #HT #d #e destruct + elim (IH G L V1 … d e) // elim (IH G L T1 … d e) // + /3 width=2 by cpye_flat, ex_intro/ +] +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 9aa3bd04d..43e2aa669 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,12 +212,8 @@ 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" * ] + [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] [ { "iterated structural successor for closures" * } { @@ -242,8 +238,12 @@ table { ] class "orange" [ { "relocation" * } { + [ { "normal forms for context-sensitive extended substitution" * } { + [ "cny ( ⦃?,?⦄ ⊢ ▶[?,?] 𝐍⦃?⦄ )" "cny_lift" * ] + } + ] [ { "contxt-sensitive extended ordinary substitution" * } { - [ "cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? )" "cpy_lift" + "cpy_cpy" * ] + [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ] } ] [ { "local env. ref. for extended substitution" * } {