From d02c188ee3d4bd9885490447e63453adb2cb4ea1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 11 May 2018 21:28:42 +0200 Subject: [PATCH] update in basic_2 + first file on r-equivalence + renaming --- .../lambdadelta/basic_2/equivalence/cpcs.ma | 96 ---------------- .../basic_2/notation/relations/pconv_5.ma | 2 +- .../{pconvstar_4.ma => pconvstar_5.ma} | 4 +- .../basic_2/rt_equivalence/cpcs.ma | 104 ++++++++++++++++++ .../cpcs_aaa.ma | 0 .../cpcs_cpcs.ma | 0 .../cpcs_cprs.ma | 0 .../basic_2/rt_equivalence/partial.txt | 1 + .../{equivalence => rt_equivalence}/scpes.ma | 0 .../scpes_aaa.ma | 0 .../scpes_cpcs.ma | 0 .../scpes_scpes.ma | 0 .../lambdadelta/basic_2/web/basic_2_src.tbl | 10 +- .../contribs/lambdadelta/compile_partial.sh | 2 + 14 files changed, 115 insertions(+), 104 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{pconvstar_4.ma => pconvstar_5.ma} (92%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/cpcs_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/cpcs_cpcs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/cpcs_cprs.ma (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/scpes.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/scpes_aaa.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/scpes_cpcs.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{equivalence => rt_equivalence}/scpes_scpes.ma (100%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma deleted file mode 100644 index 75964c615..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma +++ /dev/null @@ -1,96 +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/notation/relations/pconvstar_4.ma". -include "basic_2/conversion/cpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -definition cpcs: relation4 genv lenv term term ≝ - λG. CTC … (cpc G). - -interpretation "context-sensitive parallel equivalence (term)" - 'PConvStar G L T1 T2 = (cpcs G L T1 T2). - -(* Basic eliminators ********************************************************) - -lemma cpcs_ind: ∀G,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T2. -normalize /3 width=6 by TC_star_ind/ -qed-. - -lemma cpcs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T1. -normalize /3 width=6 by TC_star_ind_dx/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: pc3_refl *) -lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L). -/2 width=1 by inj/ qed. - -(* Basic_1: was: pc3_s *) -lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L). -normalize /3 width=1 by cpc_sym, TC_symmetric/ -qed-. - -lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/2 width=1 by inj/ qed. - -lemma cpcs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -normalize /2 width=3 by step/ -qed-. - -lemma cpcs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -normalize /2 width=3 by TC_strap/ -qed-. - -(* Basic_1: was: pc3_pr2_r *) -lemma cpr_cpcs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=1 by cpc_cpcs, or_introl/ qed. - -(* Basic_1: was: pc3_pr2_x *) -lemma cpr_cpcs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡ T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=1 by cpc_cpcs, or_intror/ qed. - -lemma cpcs_cpr_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap1, or_introl/ qed-. - -(* Basic_1: was: pc3_pr2_u *) -lemma cpcs_cpr_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap2, or_introl/ qed-. - -lemma cpcs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap1, or_intror/ qed-. - -lemma cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpr_cpcs_dx, cpcs_strap1, or_intror/ qed-. - -(* Basic_1: was: pc3_pr2_u2 *) -lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap2, or_intror/ qed-. - -(* Basic_1: removed theorems 9: - clear_pc3_trans pc3_ind_left - pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 - pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0 - pc3_gen_abst pc3_gen_abst_shift -*) -(* Basic_1: removed local theorems 6: - pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left - pc3_wcpr0_t_aux -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma index 4c9e62514..40765b785 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_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 h ] 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 @{ 'PConv $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma index f263e5d06..83f5e2cbd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_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 @{ 'PConvStar $G $L $T1 $T2 }. + for @{ 'PConvStar $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma new file mode 100644 index 000000000..8fc12c258 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/lib/star.ma". +include "basic_2/notation/relations/pconvstar_5.ma". +include "basic_2/rt_conversion/cpc.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +definition cpcs: sh → relation4 genv lenv term term ≝ + λh,G. CTC … (cpc h G). + +interpretation "context-sensitive parallel r-equivalence (term)" + 'PConvStar h G L T1 T2 = (cpcs h G L T1 T2). + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: was: cpcs_ind_dx *) +lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1. +normalize /3 width=6 by TC_star_ind_dx/ +qed-. + +(* Basic_2A1: was: cpcs_ind *) +lemma cpcs_ind_dx (h): ∀G,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2. +normalize /3 width=6 by TC_star_ind/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: pc3_refl *) +lemma cpcs_refl (h): ∀G. c_reflexive … (cpcs h G). +/2 width=1 by inj/ qed. + +(* Basic_1: was: pc3_s *) +lemma cpcs_sym (h): ∀G,L. symmetric … (cpcs h G L). +#h #G #L @TC_symmetric +/2 width=1 by cpc_sym/ +qed-. + +lemma cpc_cpcs (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/2 width=1 by inj/ qed. + +(* Basic_2A1: was: cpcs_strap2 *) +lemma cpcs_step_sn (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +normalize /2 width=3 by TC_strap/ +qed-. + +(* Basic_2A1: was: cpcs_strap1 *) +lemma cpcs_step_dx (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +normalize /2 width=3 by step/ +qed-. + +(* Basic_1: was: pc3_pr2_r *) +lemma cpr_cpcs_dx (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=1 by cpc_cpcs, or_introl/ qed. + +(* Basic_1: was: pc3_pr2_x *) +lemma cpr_cpcs_sn (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=1 by cpc_cpcs, or_intror/ qed. + +(* Basic_1: was: pc3_pr2_u *) +(* Basic_2A1: was: cpcs_cpr_strap2 *) +lemma cpcs_cpr_step_sn (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_sn, or_introl/ qed-. + +(* Basic_2A1: was: cpcs_cpr_strap1 *) +lemma cpcs_cpr_step_dx (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_dx, or_introl/ qed-. + +lemma cpcs_cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_dx, or_intror/ qed-. + +lemma cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-. + +(* Basic_1: was: pc3_pr2_u2 *) +lemma cpcs_cpr_conf (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_sn, or_intror/ qed-. + +(* Basic_1: removed theorems 9: + clear_pc3_trans pc3_ind_left + pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 + pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0 + pc3_gen_abst pc3_gen_abst_shift +*) +(* Basic_1: removed local theorems 6: + pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left + pc3_wcpr0_t_aux +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt new file mode 100644 index 000000000..5072a8ac4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt @@ -0,0 +1 @@ +cpcs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma 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 46255ef35..3fe65458a 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 @@ -44,20 +44,20 @@ table { ] } ] -(* class "prune" - [ { "equivalence" * } { + [ { "rt-equivalence" * } { +(* [ { "decomposed rt-equivalence" * } { [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] } ] - [ { "context-sensitive equivalence" * } { - [ [ "" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ] +*) + [ { "context-sensitive parallel r-equivalence" * } { + [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ] } ] } ] -*) class "blue" [ { "rt-conversion" * } { [ { "context-sensitive parallel r-conversion" * } { diff --git a/matita/matita/contribs/lambdadelta/compile_partial.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh index cc92f87dc..59b18afc7 100644 --- a/matita/matita/contribs/lambdadelta/compile_partial.sh +++ b/matita/matita/contribs/lambdadelta/compile_partial.sh @@ -1,6 +1,8 @@ ../../matitac.opt `cat partial.txt` cd basic_2/rt_computation/ ../../../../matitac.opt `cat partial.txt` +cd ../rt_equivalence/ +../../../../matitac.opt `cat partial.txt` cd ../dynamic/ ../../../../matitac.opt `cat partial.txt` cd ../../ -- 2.39.2