From 85fcff9664b400a1cf25f383505638ffe34222b6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 31 Jan 2022 22:51:55 +0100 Subject: [PATCH] update in delayed updating + additions to lift + bugs fixed in dtr and itr --- .../delayed_updating/reduction/dfr.ma | 2 +- .../delayed_updating/reduction/dfr_ifr.ma | 2 +- .../delayed_updating/reduction/ifr.ma | 3 +- .../substitution/fsubst_lift.ma | 2 +- .../substitution/lift_constructors.ma | 24 ++--------- .../delayed_updating/substitution/lift_eq.ma | 12 ++++++ .../substitution/lift_prototerm.ma | 7 +--- .../substitution/lift_prototerm_eq.ma | 40 +++++++++++++++++++ .../substitution/lift_structure.ma | 1 - 9 files changed, 61 insertions(+), 32 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index e118134dd..42d9e0c76 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -29,7 +29,7 @@ include "ground/xoa/and_4.ma". definition dfr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃∃b,n. let r ≝ p●𝗔◗b●𝗟◗q in - ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]f)@❨n❩ & r◖𝗱n ϵ t1 & + ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 & t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2 . diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma index c555072f6..9a376bed0 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -32,7 +32,7 @@ lemma dfr_lift_bi (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → >tr_pushs_swap (lift_path_eq_repl … (tr_compose_assoc …)) // -| tr_compose_push_bi // -] -qed. - -include "delayed_updating/substitution/lift_prototerm.ma". - -axiom lift_term_after (t) (f1) (f2): - ↑[f2]↑[f1]t ⇔ ↑[f2∘f1]t. - +include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/syntax/prototerm_constructors.ma". (* LIFT FOR PROTOTERM *******************************************************) -lemma lift_iref_after_sn (f) (t) (n:pnat): - (↑[f∘𝐮❨n❩]t) ⊆ ↑[f](𝛗n.t). +lemma lift_iref_after_sn (f) (t:prototerm) (n:pnat): + ↑[f∘𝐮❨n❩]t ⊆ ↑[f](𝛗n.t). #f #t #n #p * #q #Hq #H0 destruct @(ex2_intro … (𝗱n◗𝗺◗q)) /2 width=1 by in_comp_iref/ diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma index 9e23b2cb9..dc3000c15 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma @@ -13,6 +13,8 @@ (**************************************************************************) include "delayed_updating/substitution/lift.ma". +include "ground/relocation/tr_compose_compose.ma". +include "ground/relocation/tr_compose_pn.ma". include "ground/relocation/tr_compose_eq.ma". include "ground/relocation/tr_pn_eq.ma". @@ -99,3 +101,13 @@ lemma lift_path_A_sn (f) (p): lemma lift_path_S_sn (f) (p): (𝗦◗↑[f]p) = ↑[f](𝗦◗p). // qed. + +lemma lift_path_after (p) (f1) (f2): + ↑[f2]↑[f1]p = ↑[f2∘f1]p. +#p @(path_ind_lift … p) -p // [ #n #l #p | #p ] #IH #f1 #f2 +[ (lift_path_eq_repl … (tr_compose_assoc …)) // +| tr_compose_push_bi // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma index 4a0615a3c..6555b5d9e 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma @@ -14,7 +14,7 @@ include "delayed_updating/substitution/lift.ma". include "delayed_updating/syntax/prototerm.ma". -include "ground/lib/subset_ext_equivalence.ma". +include "ground/lib/subset_ext.ma". (* LIFT FOR PROTOTERM *******************************************************) @@ -28,8 +28,3 @@ lemma in_comp_lift_bi (f) (p) (t): p ϵ t → ↑[f]p ϵ ↑[f]t. /2 width=1 by subset_in_ext_f1_dx/ qed. - -lemma eq_lift_bi (f) (t1) (t2): - t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2. -/2 width=1 by subset_equivalence_ext_f1_bi/ -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma new file mode 100644 index 000000000..44ec5a366 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.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 "ground/lib/subset_ext_equivalence.ma". +include "delayed_updating/substitution/lift_eq.ma". +include "delayed_updating/substitution/lift_prototerm.ma". + +(* LIFT FOR PROTOTERM *******************************************************) + +(* Constructions with subset_equivalence ************************************) + +lemma lift_term_eq_repl_sn (f1) (f2) (t): + f1 ≗ f2 → ↑[f1]t ⇔ ↑[f2]t. +/3 width=1 by subset_equivalence_ext_f1_exteq, lift_path_eq_repl/ +qed. + +lemma lift_term_eq_repl_dx (f) (t1) (t2): + t1 ⇔ t2 → ↑[f]t1 ⇔ ↑[f]t2. +/2 width=1 by subset_equivalence_ext_f1_bi/ +qed. + +lemma lift_term_after (f1) (f2) (t): + ↑[f2]↑[f1]t ⇔ ↑[f2∘f1]t. +#f1 #f2 #t @subset_eq_trans +[ +| @subset_inclusion_ext_f1_compose +| @subset_equivalence_ext_f1_exteq /2 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma index b9bc27c54..449317ee6 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma @@ -16,7 +16,6 @@ include "delayed_updating/substitution/lift_eq.ma". include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_proper.ma". include "ground/xoa/ex_4_2.ma". -include "ground/xoa/ex_3_2.ma". (* LIFT FOR PATH ***********************************************************) -- 2.39.2