From dd93a0919b67bead0d4f07d49dfc198006edc9aa Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 5 Apr 2019 15:34:26 +0200 Subject: [PATCH] update in ground_2 static_2 basic_2 structures for decidability of the validity predicate + cpes, cnr, cpre resumed + minor corrections --- .../lambdadelta/basic_2/dynamic/cnv_aaa.ma | 2 +- .../lambdadelta/basic_2/dynamic/cnv_cpes.ma | 76 +++++++++++++++ .../lambdadelta/basic_2/dynamic/cnv_drops.ma | 2 +- .../lambdadelta/basic_2/dynamic/cnv_fqus.ma | 2 +- .../lambdadelta/basic_2/etc/cnr/cnr.etc | 97 ------------------- .../lambdadelta/basic_2/etc/cnr/cnr_lift.etc | 49 ---------- .../lambdadelta/basic_2/etc/cprs/cprs.etc | 7 -- .../basic_2/etc/scpes/scpes_scpes.etc | 7 -- .../relations/pconvstar_7.ma} | 4 +- .../relations/predeval_5.ma} | 4 +- .../{predsnstar_3.ma => predeval_6.ma} | 4 +- .../relations/prednormal_4.ma} | 4 +- .../basic_2/rt_computation/cpme.ma | 26 +++++ .../basic_2/rt_computation/cpre.ma | 22 +++++ .../basic_2/rt_computation/cpre_cpre.ma | 40 ++++++++ .../cpre_csx.ma} | 26 ++--- .../cprs_cnr.ma} | 21 ++-- .../scpes.etc => rt_equivalence/cpes.ma} | 34 ++++--- .../cpre.etc => rt_equivalence/cpes_aaa.ma} | 37 ++++--- .../lambdadelta/basic_2/rt_transition/cnr.ma | 83 ++++++++++++++++ .../basic_2/rt_transition/cnr_drops.ma | 77 +++++++++++++++ .../basic_2/rt_transition/cnr_simple.ma | 43 ++++++++ .../basic_2/rt_transition/cnr_tdeq.ma | 97 +++++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 19 ++-- .../ground_2/notation/xoa/ex_1_4.ma | 26 +++++ .../lambdadelta/ground_2/xoa/ex_1_4.ma | 28 ++++++ .../lambdadelta/ground_2/xoa/ex_4_1_props.ma | 2 +- .../lambdadelta/ground_2/xoa2.conf.xml | 1 + .../static_2/syntax/term_simple.ma | 9 ++ 29 files changed, 618 insertions(+), 231 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc/scpes/dpconvstar_8.etc => notation/relations/pconvstar_7.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/cpre/predeval_4.etc => notation/relations/predeval_5.ma} (91%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predsnstar_3.ma => predeval_6.ma} (85%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/cnr/prednormal_3.etc => notation/relations/prednormal_4.ma} (88%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/scpes/scpes_aaa.etc => rt_computation/cpre_csx.ma} (57%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/cpre/cpre_cpre.etc => rt_computation/cprs_cnr.ma} (64%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/scpes/scpes.etc => rt_equivalence/cpes.ma} (53%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/cpre/cpre.etc => rt_equivalence/cpes_aaa.ma} (52%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_simple.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_1_4.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/xoa/ex_1_4.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index 7f71bea7c..d8981613d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -15,7 +15,7 @@ include "basic_2/rt_computation/cpms_aaa.ma". include "basic_2/dynamic/cnv.ma". -(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Forward lemmas on atomic arity assignment for terms **********************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma new file mode 100644 index 000000000..c7da94159 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/cpms_cpms.ma". +include "basic_2/rt_equivalence/cpes.ma". +include "basic_2/dynamic/cnv.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with t-bound rt-equivalence for terms *************************) + +lemma cnv_appl_cpes (a) (h) (G) (L): + ∀n. (a = Ⓣ → n ≤ 1) → + ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] → + ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W → + ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h]. +#a #h #G #L #n #Hn #V #HV #T #HT #W * +/4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/ +qed. + +lemma cnv_cast_cpes (a) (h) (G) (L): + ∀U. ⦃G, L⦄ ⊢ U ![a, h] → + ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G, L⦄ ⊢ ⓝU.T ![a, h]. +#a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/ +qed. + +(* Inversion lemmas with t-bound rt-equivalence for terms *******************) + +lemma cnv_inv_appl_cpes (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → + ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U. +#a #h #G #L #V #T #H +elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU +/3 width=7 by cpms_div, ex5_4_intro/ +qed-. + +lemma cnv_inv_cast_cpes (a) (h) (G) (L): + ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] → + ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T. +#a #h #G #L #U #T #H +elim (cnv_inv_cast … H) -H +/3 width=3 by cpms_div, and3_intro/ +qed-. + +(* Eliminators with t-bound rt-equivalence for terms ************************) + +lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term): + (∀G,L,s. Q G L (⋆s)) → + (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) → + (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) → + (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] → + Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T) + ) → + (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] → + ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → + Q G L V → Q G L T → Q G L (ⓐV.T) + ) → + (∀G,L,U,T. ⦃G,L⦄⊢ U![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T → + Q G L U → Q G L T → Q G L (ⓝU.T) + ) → + ∀G,L,T. ⦃G,L⦄⊢ T![a,h] → Q G L T. +#a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H +elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma index e4d55446c..8c95ffcf6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_drops.ma @@ -15,7 +15,7 @@ include "basic_2/rt_computation/cpms_drops.ma". include "basic_2/dynamic/cnv.ma". -(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Advanced dproperties *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma index cb79dfcc8..113ffe922 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fqus.ma @@ -15,7 +15,7 @@ include "static_2/s_computation/fqus_fqup.ma". include "basic_2/dynamic/cnv_drops.ma". -(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) (* Properties with supclosure ***********************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc index 1a307432d..23a5dc473 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr.etc @@ -1,51 +1,3 @@ -(**************************************************************************) -(* ___ *) -(* ||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/prednormal_3.ma". -include "basic_2/reduction/cpr.ma". - -(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) - -definition cnr: relation3 genv lenv term ≝ λG,L. NF … (cpr G L) (eq …). - -interpretation - "normality for context-sensitive reduction (term)" - 'PRedNormal G L T = (cnr G L T). - -(* Basic inversion lemmas ***************************************************) - -lemma cnr_inv_delta: ∀G,L,K,V,i. ⬇[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄ → ⊥. -#G #L #K #V #i #HLK #H -elim (lift_total V 0 (i+1)) #W #HVW -lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct -elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/ -qed-. - -lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡ 𝐍⦃T⦄. -#a #G #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct // -] -qed-. - -lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡ 𝐍⦃T⦄. -#G #L #V1 #T1 #HVT1 @conj -[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct // -] -qed-. - lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃+ⓓV.T⦄ → ⊥. #G #L #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU @@ -58,57 +10,8 @@ lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃+ⓓV.T⦄ → ⊥. ] qed-. -lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ & 𝐒⦃T⦄. -#G #L #V1 #T1 #HVT1 @and3_intro -[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct // -| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H - [ elim (lift_total V1 0 1) #V2 #HV12 - lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by tpr_cpr, cpr_theta/ -HV12 #H destruct - | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by tpr_cpr, cpr_beta/ #H destruct -] -qed-. - -lemma cnr_inv_eps: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓝV.T⦄ → ⊥. -#G #L #V #T #H lapply (H T ?) -H -/2 width=4 by cpr_eps, discr_tpair_xy_y/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: nf2_sort *) -lemma cnr_sort: ∀G,L,s. ⦃G, L⦄ ⊢ ➡ 𝐍⦃⋆s⦄. -#G #L #s #X #H ->(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 (drop_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 >(drop_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 -elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct ->(HW … HW0) -W0 >(HT … HT0) -T0 // -qed. - -(* Basic_1: was only: nf2_appl_lref *) -lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄. -#G #L #V #T #HV #HT #HS #X #H -elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct ->(HV … HV0) -V0 >(HT … HT0) -T0 // -qed. - -(* Basic_1: was: nf2_dec *) -axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T1⦄ ∨ - ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). - -(* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc deleted file mode 100644 index eef9aefc8..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/cnr_lift.etc +++ /dev/null @@ -1,49 +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_lift.ma". -include "basic_2/reduction/cnr.ma". - -(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************) - -(* Advanced properties ******************************************************) - -(* 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 -elim (cpr_inv_lref1 … H) -H // * -#K0 #V1 #V2 #HLK0 #_ #_ -lapply (drop_mono … HLK … HLK0) -L #H destruct -qed. - -(* Relocation properties ****************************************************) - -(* Basic_1: was: nf2_lift *) -lemma cnr_lift: ∀G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → - ⬇[c, l, k] L0 ≡ L → ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄. -#G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H -elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 -<(HLT … HT1) in HT0; -L #HT0 ->(lift_mono … HT10 … HT0) -T1 -X // -qed. - -(* Note: this was missing in basic_1 *) -lemma cnr_inv_lift: ∀G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄ → - ⬇[c, l, k] L0 ≡ L → ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. -#G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H -elim (lift_total X l k) #X0 #HX0 -lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0 ->(HLT0 … HTX0) in HX0; -L0 -X0 #H ->(lift_inj … H … HT0) -T0 -X -c -l -k // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc index a51dba5d6..b20ba8ff8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc @@ -1,10 +1,3 @@ (* Basic_1: was: pr3_pr1 *) lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. /2 width=3 by lsubr_cprs_trans/ qed. - -(* Basic_1: was: nf2_pr3_unfold *) -lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U. -#G #L #T #U #H @(cprs_ind_dx … H) -T // -#T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc index 24ea20ec0..6ed660a42 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_scpes.etc @@ -28,13 +28,6 @@ qed-. (* Advanced properties ******************************************************) -lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → - ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T. -#h #o #G #L #T #d1 #d2 #Hd21 #Hd1 -elim (da_lstas … Hd1 … d2) #U #HTU #_ -/3 width=3 by scpds_div, lstas_scpds/ -qed. - lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 → ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T → ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_7.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_7.ma index f0210a6b8..a89f13d36 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/dpconvstar_8.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_7.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌* [ break term 46 h, break term 46 n1, break term 46 n2 ] break term 46 T2 )" non associative with precedence 45 - for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }. + for @{ 'PConvStar $h $n1 $n2 $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/predeval_4.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_5.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpre/predeval_4.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_5.ma index abf7b6558..cee1d0332 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/predeval_4.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * 𝐍 ⦃ break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 h ] 𝐍 ⦃ break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'PRedEval $G $L $T1 $T2 }. + for @{ 'PRedEval $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma similarity index 85% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma index 75777fb17..549a7902a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 h, break term 46 n ] 𝐍 ⦃ break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'PRedSnStar $G $L1 $L2 }. + for @{ 'PRedEval $h $n $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/prednormal_3.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_4.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cnr/prednormal_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_4.ma index a8806a1c7..c718260cf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cnr/prednormal_3.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐍 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ [ break term 46 h ] 𝐍 ⦃ break term 46 T ⦄ )" non associative with precedence 45 - for @{ 'PRedNormal $G $L $T }. + for @{ 'PRedNormal $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma new file mode 100644 index 000000000..78cf43d23 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpme.ma @@ -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/notation/relations/predeval_6.ma". +include "basic_2/rt_transition/cnr.ma". +include "basic_2/rt_computation/cpms.ma". + +(* EVALUATION FOR T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ON TERMS *) + +(* Basic_2A1: uses: cpre *) +definition cpme (h) (n) (G) (L): relation2 term term ≝ + λT1,T2. ∧∧ ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T2⦄. + +interpretation "evaluation for t-bound context-sensitive parallel rt-transition (term)" + 'PRedEval h n G L T1 T2 = (cpme h n G L T1 T2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma new file mode 100644 index 000000000..605915021 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predeval_5.ma". +include "basic_2/rt_computation/cpme.ma". +include "basic_2/rt_computation/cprs.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS ***********) + +interpretation "evaluation for context-sensitive parallel r-transition (term)" + 'PRedEval h G L T1 T2 = (cpme h O G L T1 T2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma new file mode 100644 index 000000000..202e1ccad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma @@ -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 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_computation/cprs_cnr.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/cpre.ma". + +(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS *********) + +(* Properties with context-sensitive parallel r-computation for terms ******) + +lemma cpre_cprs_conf (h) (G) (L) (T): + ∀T1. ⦃G,L⦄ ⊢ T ➡*[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄. +#h #G #L #T0 #T1 #HT01 #T2 * #HT02 #HT2 +elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20 +lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct +/2 width=1 by conj/ +qed-. + +(* Main properties *********************************************************) + +(* Basic_1: was: nf2_pr3_confluence *) +theorem cpre_mono (h) (G) (L) (T): + ∀T1. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → T1 = T2. +#h #G #L #T0 #T1 * #HT01 #HT1 #T2 * #HT02 #HT2 +elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20 +>(cprs_inv_cnr_sn … HT10 HT1) -T1 +>(cprs_inv_cnr_sn … HT20 HT2) -T2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma similarity index 57% rename from matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma index f42ebdbc9..9b01da5ae 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes_aaa.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_csx.ma @@ -12,18 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/computation/scpds_aaa.ma". -include "basic_2/equivalence/scpes.ma". +include "basic_2/rt_transition/cpm_cpx.ma". +include "basic_2/rt_transition/cnr_tdeq.ma". +include "basic_2/rt_computation/csx.ma". +include "basic_2/rt_computation/cpre.ma". -(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) +(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS **********) -(* Main inversion lemmas about atomic arity assignment on terms *************) +(* Properties with strong normalization for unbound rt-transition for terms *) -theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → - A1 = A2. -#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 -lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1 -lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2 -lapply (aaa_mono … HA1 … HA2) -L -T // +(* Basic_1: was just: nf2_sn3 *) +lemma csx_cpre (h) (G) (L): + ∀T1. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄. +#h #G #L #T1 #H +@(csx_ind … H) -T1 #T1 #_ #IHT1 +elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, conj/ ] * +#T0 #HT10 #HnT10 +elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ] +#T2 * /4 width=3 by cprs_step_sn, ex_intro, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre_cpre.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cnr.ma similarity index 64% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre_cpre.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cnr.ma index 4fd418119..2849fa0b7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre_cpre.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_cnr.ma @@ -12,17 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/cpre.ma". +include "basic_2/rt_transition/cnr.ma". +include "basic_2/rt_computation/cprs.ma". -(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************) +(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************) -(* Main properties *********************************************************) +(* Inversion lemmas with normal terms for r-transition **********************) -(* Basic_1: was: nf2_pr3_confluence *) -theorem cpre_mono: ∀G,L,T,T1. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2. -#G #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2 -elim (cprs_conf … H1T1 … H1T2) -T #T #HT1 ->(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2 ->(cprs_inv_cnr1 … HT2 H2T2) -T2 // +(* Basic_1: was: nf2_pr3_unfold *) +(* Basic_2A1: was: cprs_inv_cnr1 *) +lemma cprs_inv_cnr_sn (h) (G) (L): + ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T1⦄ → T1 = T2. +#h #G #L #T1 #T2 #H @(cprs_ind_sn … H) -T1 // +#T1 #T0 #HT10 #_ #IH #HT1 +lapply (HT1 … HT10) -HT10 #H destruct /2 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes.ma similarity index 53% rename from matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes.ma index 657763483..c864c81a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/scpes/scpes.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes.ma @@ -12,26 +12,32 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/dpconvstar_8.ma". -include "basic_2/computation/scpds.ma". +include "basic_2/notation/relations/pconvstar_7.ma". +include "basic_2/rt_computation/cpms.ma". -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************) -definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ - λh,o,d1,d2,G,L,T1,T2. - ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T. +(* Basic_2A1: uses: scpes *) +definition cpes (h) (n1) (n2): relation4 genv lenv term term ≝ + λG,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1,h] T & ⦃G, L⦄ ⊢ T2 ➡*[n2,h] T. -interpretation "stratified decomposed parallel equivalence (term)" - 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2). +interpretation "t-bound context-sensitive parallel rt-equivalence (term)" + 'PConvStar h n1 n2 G L T1 T2 = (cpes h n1 n2 G L T1 T2). (* Basic properties *********************************************************) -lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2. - ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → - ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +(* Basic_2A1: uses: scpds_div *) +lemma cpms_div (h) (n1) (n2): + ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1,h] T → + ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[n2,h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2. /2 width=3 by ex2_intro/ qed. -lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1. -#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/ +lemma cpes_refl (h): ∀G,L. reflexive … (cpes h 0 0 G L). +/2 width=3 by cpms_div/ qed. + +(* Basic_2A1: uses: scpes_sym *) +lemma cpes_sym (h) (n1) (n2): + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2 → ⦃G, L⦄ ⊢ T2 ⬌*[h,n2,n1] T1. +#h #n1 #n2 #G #L #T1 #T2 * /2 width=3 by cpms_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre.etc b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_aaa.ma similarity index 52% rename from matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre.etc rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_aaa.ma index d94fb6fba..aae663c8f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpes_aaa.ma @@ -12,24 +12,29 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predeval_4.ma". -include "basic_2/computation/cprs.ma". -include "basic_2/computation/csx.ma". +include "basic_2/rt_computation/cpms_aaa.ma". +include "basic_2/rt_equivalence/cpes.ma". -(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************) +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************) -definition cpre: relation4 genv lenv term term ≝ - λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃T2⦄. +(* Properties with atomic arity assignment on terms *************************) -interpretation "evaluation for context-sensitive parallel reduction (term)" - 'PRedEval G L T1 T2 = (cpre G L T1 T2). +(* Basic_2A1: uses: scpes_refl *) +lemma cpes_refl_aaa (h) (n): + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ T ⬌*[h,n,n] T. +#h #n #G #L #T #A #HA +elim (aaa_cpms_total h … n … HA) #U #HTU +/2 width=3 by cpms_div/ +qed. -(* Basic properties *********************************************************) +(* Main inversion lemmas with atomic arity assignment on terms **************) -(* Basic_1: was just: nf2_sn3 *) -lemma csx_cpre: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄. -#h #o #G #L #T1 #H @(csx_ind … H) -T1 -#T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3 by ex_intro, conj/ -* #T #H1T1 #H2T1 elim (IHT1 … H2T1) -IHT1 -H2T1 /2 width=2 by cpr_cpx/ -#T2 * /4 width=3 by cprs_strap2, ex_intro, conj/ -qed. +(* Basic_2A1: uses: scpes_aaa_mono *) +theorem cpes_aaa_mono (h) (n1) (n2): + ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → A1 = A2. +#h #n1 #n2 #G #L #T1 #T2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 +lapply (cpms_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (cpms_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr.ma new file mode 100644 index 000000000..aeb33e6dd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr.ma @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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/prednormal_4.ma". +include "basic_2/rt_transition/cpr.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************) + +definition cnr (h) (G) (L): predicate term ≝ NF … (cpm h G L 0) (eq …). + +interpretation + "normality for context-sensitive r-transition (term)" + 'PRedNormal h G L T = (cnr h G L T). + +(* Basic inversion lemmas ***************************************************) + +lemma cnr_inv_abst (h) (p) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓛ{p}V.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L.ⓛV⦄ ⊢ ➡[h] 𝐍⦃T⦄. +#h #p #G #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (ⓛ{p}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓛ{p}V1.T2) ?) -HVT1 /2 width=2 by cpm_bind/ -HT2 #H destruct // +] +qed-. + +(* Basic_2A1: was: cnr_inv_abbr *) +lemma cnr_inv_abbr_neg (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃-ⓓV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L.ⓓV⦄ ⊢ ➡[h] 𝐍⦃T⦄. +#h #G #L #V1 #T1 #HVT1 @conj +[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpm_bind/ -HT2 #H destruct // +] +qed-. + +(* Basic_2A1: was: cnr_inv_eps *) +lemma cnr_inv_cast (h) (G) (L): ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓝV.T⦄ → ⊥. +#h #G #L #V #T #H lapply (H T ?) -H +/2 width=4 by cpm_eps, discr_tpair_xy_y/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: nf2_sort *) +lemma cnr_sort (h) (G) (L): ∀s. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃⋆s⦄. +#h #G #L #s #X #H +>(cpr_inv_sort1 … H) // +qed. + +lemma cnr_gref (h) (G) (L): ∀l. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃§l⦄. +#h #G #L #l #X #H +>(cpr_inv_gref1 … H) // +qed. + +(* Basic_1: was: nf2_abst *) +lemma cnr_abst (h) (p) (G) (L): + ∀W,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓛ{p}W.T⦄. +#h #p #G #L #W #T #HW #HT #X #H +elim (cpm_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct +<(HW … HW0) -W0 <(HT … HT0) -T0 // +qed. + +lemma cnr_abbr_neg (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G, L.ⓓV⦄ ⊢ ➡[h] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃-ⓓV.T⦄. +#h #G #L #V #T #HV #HT #X #H +elim (cpm_inv_abbr1 … H) -H * +[ #V0 #T0 #HV0 #HT0 #H destruct + <(HV … HV0) -V0 <(HT … HT0) -T0 // +| #T0 #_ #_ #H destruct +] +qed. + + +(* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_drops.ma new file mode 100644 index 000000000..6bc4661ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_drops.ma @@ -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 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/cpr_drops.ma". +include "basic_2/rt_transition/cnr.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: nf2_csort_lref *) +lemma cnr_lref_atom (h) (b) (G) (L): + ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄. +#h #b #G #L #i #Hi #X #H +elim (cpr_inv_lref1_drops … H) -H // * #K #V1 #V2 #HLK +lapply (drops_gen b … HLK) -HLK #HLK +lapply (drops_mono … Hi … HLK) -L #H destruct +qed. + +(* Basic_1: was: nf2_lref_abst *) +lemma cnr_lref_abst (h) (G) (L): + ∀K,V,i. ⬇*[i] L ≘ K.ⓛV → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄. +#h #G #L #K #V #i #HLK #X #H +elim (cpr_inv_lref1_drops … H) -H // * +#K0 #V1 #V2 #HLK0 #_ #_ +lapply (drops_mono … HLK … HLK0) -L #H destruct +qed. + +lemma cnr_lref_unit (h) (I) (G) (L): + ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄. +#h #I #G #L #K #i #HLK #X #H +elim (cpr_inv_lref1_drops … H) -H // * +#K0 #V1 #V2 #HLK0 #_ #_ +lapply (drops_mono … HLK … HLK0) -L #H destruct +qed. + +(* Properties with generic relocation ***************************************) + +(* Basic_1: was: nf2_lift *) +(* Basic_2A1: uses: cnr_lift *) +lemma cnr_lifts (h) (G): d_liftable1 … (cnr h G). +#h #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H +elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 +lapply (HT … HT0) -G -K #H destruct /2 width=4 by lifts_mono/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: was: cnr_inv_delta *) +lemma cnr_inv_lref_abbr (h) (G) (L): + ∀K,V,i. ⬇*[i] L ≘ K.ⓓV → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄ → ⊥. +#h #G #L #K #V #i #HLK #H +elim (lifts_total V 𝐔❴↑i❵) #W #HVW +lapply (H W ?) -H [ /3 width=6 by cpm_delta_drops/ ] -HLK #H destruct +elim (lifts_inv_lref2_uni_lt … HVW) -HVW // +qed-. + +(* Inversion lemmas with generic relocation *********************************) + +(* Note: this was missing in Basic_1 *) +(* Basic_2A1: uses: cnr_inv_lift *) +lemma cnr_inv_lifts (h) (G): d_deliftable1 … (cnr h G). +#h #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H +elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 +lapply (HU … HU0) -G -L #H destruct /2 width=4 by lifts_inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_simple.ma new file mode 100644 index 000000000..5dcbada49 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_simple.ma @@ -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/rt_transition/cpm_simple.ma". +include "basic_2/rt_transition/cnr.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************) + +(* Inversion lemmas with simple terms ***************************************) + +lemma cnr_inv_appl (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T⦄ & 𝐒⦃T⦄. +#h #G #L #V1 #T1 #HVT1 @and3_intro +[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct // +| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H + [ elim (lifts_total V1 𝐔❴1❵) #V2 #HV12 + lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /2 width=3 by cpm_theta/ -HV12 #H destruct + | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /2 width=1 by cpm_beta/ #H destruct + ] +] +qed-. + +(* Properties with simple terms *********************************************) + +(* Basic_1: was only: nf2_appl_lref *) +lemma cnr_appl_simple (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓐV.T⦄. +#h #G #L #V #T #HV #HT #HS #X #H +elim (cpm_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct +<(HV … HV0) -V0 <(HT … HT0) -T0 // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma new file mode 100644 index 000000000..3efc47bba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnr_tdeq.ma @@ -0,0 +1,97 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/lifts_tdeq.ma". +include "basic_2/rt_transition/cpr_drops_basic.ma". +include "basic_2/rt_transition/cnr_simple.ma". +include "basic_2/rt_transition/cnr_drops.ma". + +(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************) + +(* Properties with context-free sort-irrelevant equivalence for terms *******) + +(* Basic_1: was: nf2_dec *) +(* Basic_2A1: uses: cnr_dec *) +lemma cnr_dec_tdeq (h) (G) (L): + ∀T1. ∨∨ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T1⦄ + | ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 & (T1 ≛ T2 → ⊥). +#h #G #L #T1 +@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * * +[ #s #HG #HL #HT destruct -IH + /3 width=4 by cnr_sort, or_introl/ +| #i #HG #HL #HT destruct -IH + elim (drops_F_uni L i) + [ /3 width=6 by cnr_lref_atom, or_introl/ + | * * [ #I | * #V ] #K #HLK + [ /3 width=7 by cnr_lref_unit, or_introl/ + | elim (lifts_total V 𝐔❴↑i❵) #W #HVW + @or_intror @(ex2_intro … W) [ /2 width=6 by cpm_delta_drops/ ] #H + lapply (tdeq_inv_lref1 … H) -H #H destruct + /2 width=5 by lifts_inv_lref2_uni_lt/ + | /3 width=7 by cnr_lref_abst, or_introl/ + ] + ] +| #l #HG #HL #HT destruct -IH + /3 width=4 by cnr_gref, or_introl/ +| #p * [ cases p ] #V1 #T1 #HG #HL #HT destruct + [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 -IH + elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ] + [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2 + @or_intror @(ex2_intro … X1) [ /2 width=3 by cpm_zeta/ ] #H + /2 width=7 by tdeq_lifts_inv_pair_sn/ + | @or_intror @(ex2_intro … (+ⓓV1.T2)) [ /2 width=1 by cpm_bind/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + | elim (IH G L V1) [ elim (IH G (L.ⓓV1) T1) [| * | // ] | * | // ] -IH + [ #HT1 #HV1 /3 width=6 by cnr_abbr_neg, or_introl/ + | #T2 #HT12 #HnT12 #_ + @or_intror @(ex2_intro … (-ⓓV1.T2)) [ /2 width=1 by cpm_bind/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_intro … (-ⓓV2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + | elim (IH G L V1) [ elim (IH G (L.ⓛV1) T1) [| * | // ] | * | // ] -IH + [ #HT1 #HV1 /3 width=6 by cnr_abst, or_introl/ + | #T2 #HT12 #HnT12 #_ + @or_intror @(ex2_intro … (ⓛ{p}V1.T2)) [ /2 width=1 by cpm_bind/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_intro … (ⓛ{p}V2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + ] +| * #V1 #T1 #HG #HL #HT destruct [| -IH ] + [ elim (IH G L V1) [ elim (IH G L T1) [| * | // ] | * | // ] -IH + [ #HT1 #HV1 + elim (simple_dec_ex T1) [| * #p * #W1 #U1 #H destruct ] + [ /3 width=6 by cnr_appl_simple, or_introl/ + | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1 + @or_intror @(ex2_intro … (ⓓ{p}W1.ⓐX1.U1)) [ /2 width=3 by cpm_theta/ ] #H + elim (tdeq_inv_pair … H) -H #H destruct + | @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H + elim (tdeq_inv_pair … H) -H #H destruct + ] + | #T2 #HT12 #HnT12 #_ + @or_intror @(ex2_intro … (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + | #V2 #HV12 #HnV12 + @or_intror @(ex2_intro … (ⓐV2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H + elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] + | @or_intror @(ex2_intro … T1) [ /2 width=1 by cpm_eps/ ] #H + /2 width=4 by tdeq_inv_pair_xy_y/ + ] +] +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 0d63a09a5..57e605d70 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 @@ -25,7 +25,7 @@ table { ] [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ] } ] } @@ -36,6 +36,10 @@ table { [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ] } ] + [ { "t-bound context-sensitive parallel rt-equivalence" * } { + [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" * ] + } + ] } ] class "blue" @@ -55,12 +59,14 @@ table { class "sky" [ { "rt-computation" * } { [ { "context-sensitive parallel r-computation" * } { + [ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_cpx" + "cpre_cpre" * ] [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ] [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ] - [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cprs" * ] + [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ] } ] [ { "t-bound context-sensitive parallel rt-computation" * } { + [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" * ] [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] @@ -90,6 +96,7 @@ table { } ] [ { "context-sensitive parallel r-transition" * } { + [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ] [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] [ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_drops_basic" + "cpr_tdeq" + "cpr_cpr" * ] @@ -129,7 +136,7 @@ class "italic" { 2 } ] [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] [ { "decomposed rt-equivalence" * } { - [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] + "scpes_cpcs" + "scpes_scpes" } ] [ [ "for lenvs on referred entries" ] "rpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "rpxs_length" + "rpxs_drops" + "rpxs_fqup" + "rpxs_rdeq" + "rpxs_fdeq" + "rpxs_aaa" + "rpxs_cpxs" + "rpxs_lpxs" + "rpxs_rpxs" * ] @@ -139,10 +146,6 @@ class "italic" { 2 } [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] } ] - [ { "evaluation for context-sensitive reduction" * } { - [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] - } - ] [ { "normal forms for context-sensitive rt-reduction" * } { [ [ "" ] "cnx_crx" + "cnx_cix" * ] } @@ -156,7 +159,7 @@ class "italic" { 2 } } ] [ { "normal forms for context-sensitive reduction" * } { - [ [ "" ] "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] + "cnr_crr" + "cnr_cir" } ] [ { "irreducible forms for context-sensitive reduction" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_1_4.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_1_4.ma new file mode 100644 index 000000000..0fbf2a458 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_1_4.ma @@ -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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (1, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_1_4.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_1_4.ma new file mode 100644 index 000000000..b5faca410 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_1_4.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_1_4.ma". + +(* multiple existental quantifier (1, 4) *) + +inductive ex1_4 (A0,A1,A2,A3:Type[0]) (P0:A0→A1→A2→A3→Prop) : Prop ≝ + | ex1_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → ex1_4 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (1, 4)" 'Ex4 P0 = (ex1_4 ? ? ? ? P0). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma index fe081386b..3841d916a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_4_1_props.ma @@ -14,7 +14,7 @@ include "ground_2/xoa/xoa.ma". -(* Properties with multiple existental quantifier (5, 1) ********************) +(* Properties with multiple existental quantifier (4, 1) ********************) lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop): (∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index d40726d02..8f974dbe0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -5,6 +5,7 @@ ground_2/xoa ground_2/notation/xoa basics/pts.ma + 1 4 5 1 5 7 9 3 diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.ma index 4bef6764d..a32b35268 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_simple.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/xoa/ex_1_4.ma". include "static_2/notation/relations/simple_1.ma". include "static_2/syntax/term.ma". @@ -40,3 +41,11 @@ lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. * /2 width=2 by ex_intro/ #p #I #V #T #H elim (simple_inv_bind … H) qed-. + +(* Basic properties *********************************************************) + +lemma simple_dec_ex (X): ∨∨ 𝐒⦃X⦄ | ∃∃p,I,T,U. X = ⓑ{p,I}T.U. +* [ /2 width=1 by simple_atom, or_introl/ ] +* [| /2 width=1 by simple_flat, or_introl/ ] +/3 width=5 by ex1_4_intro, or_intror/ +qed-. -- 2.39.2