From 8db3579bec4d9a97af526f95a179587a2fbfe3e3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 4 Jan 2022 13:09:51 +0100 Subject: [PATCH] update in delayed_updating + immediate reduction defined + some lemmas with lift simplified --- .../relations/black_rightarrow_df_4.ma} | 10 ++- ...ightarrow_4.ma => black_rightarrow_f_4.ma} | 4 +- .../delayed_updating/reduction/dfr.ma | 8 +-- .../delayed_updating/reduction/dfr_ifr.ma | 23 +++++++ .../delayed_updating/reduction/ifr.ma | 31 +++++++++ .../delayed_updating/substitution/lift.ma | 47 +++++++++++++ .../delayed_updating/substitution/lift_eq.ma | 45 +++++++------ .../substitution/lift_preterm.ma | 25 +++++++ .../substitution/lift_structure.ma | 67 ++++--------------- 9 files changed, 176 insertions(+), 84 deletions(-) rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/preterm_dephi.ma => notation/relations/black_rightarrow_df_4.ma} (78%) rename matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/{black_rightarrow_4.ma => black_rightarrow_f_4.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma index 60c5a4a41..ca059fc5c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma @@ -12,10 +12,8 @@ (* *) (**************************************************************************) -include "delayed_updating/syntax/path_dephi.ma". -include "delayed_updating/syntax/preterm_constructors.ma". +(* NOTATION FOR DELAYED UPDATING ********************************************) -(* DEPHI FOR PRETERM ********************************************************) - -definition preterm_dephi (f) (t): preterm ≝ - λp. ∃∃q. q ϵ t & p = path_dephi f q. +notation "hvbox( t1 ➡𝐝𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )" + non associative with precedence 45 + for @{ 'BlackRightArrowDF $t1 $p $q $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma index f27fa0bad..c69d6c79b 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR DELAYED UPDATING ********************************************) -notation "hvbox( t1 ➡'d''f'[ break term 46 p, break term 46 q ] break term 46 t2 )" +notation "hvbox( t1 ➡𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )" non associative with precedence 45 - for @{ 'BlackRightArrow $t1 $p $q $t2 }. + for @{ 'BlackRightArrowF $t1 $p $q $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma index a99d8ca06..8c84de0f2 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma @@ -15,9 +15,9 @@ include "delayed_updating/syntax/path_structure.ma". include "delayed_updating/syntax/path_balanced.ma". include "delayed_updating/substitution/fsubst.ma". -include "delayed_updating/notation/relations/black_rightarrow_4.ma". +include "delayed_updating/notation/relations/black_rightarrow_df_4.ma". -(* DELAYED FOCALIZED REDUCTION **********************************************) +(* DELAYED FOCUSED REDUCTION ************************************************) inductive dfr (p) (q) (t): predicate preterm ≝ | dfr_beta (b) (n): @@ -26,5 +26,5 @@ inductive dfr (p) (q) (t): predicate preterm ≝ . interpretation - "delayed focalized reduction (preterm)" - 'BlackRightArrow t1 p q t2 = (dfr p q t1 t2). + "focused balanced reduction with delayed updating (preterm)" + 'BlackRightArrowDF t1 p q t2 = (dfr p q t1 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 new file mode 100644 index 000000000..bd62d8e6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/reduction/ifr.ma". +include "delayed_updating/reduction/dfr.ma". + +(* DELAYED FOCUSED REDUCTION ************************************************) + +lemma dfr_lift_bi (f) (p) (q) (t1) (t2): + t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2. +#f #p #q #t1 #t2 +* #b #n #Hr #Hb diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma new file mode 100644 index 000000000..53853273b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_balanced.ma". +include "delayed_updating/substitution/fsubst.ma". +include "delayed_updating/substitution/lift_preterm.ma". +include "delayed_updating/notation/relations/black_rightarrow_f_4.ma". + +(* IMMEDIATE FOCUSED REDUCTION ************************************************) + +inductive ifr (p) (q) (t): predicate preterm ≝ +| ifr_beta (b) (n): + let r ≝ p●𝗔◗b●𝗟◗q in + r◖𝗱❨n❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨n❩]t⋔(p◖𝗦)]) +. + +interpretation + "focused balanced reduction with immediate updating (preterm)" + 'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma index a396beb46..5db8fa945 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma @@ -81,3 +81,50 @@ lemma lift_A_sn (A) (k) (p) (f): lemma lift_S_sn (A) (k) (p) (f): ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩. // qed. + +(* Basic constructions with proj_path ***************************************) + +lemma lift_path_d_empty_sn (f) (n): + 𝗱❨f@❨n❩❩◗𝐞 = ↑[f](𝗱❨n❩◗𝐞). +// qed. + +lemma lift_path_d_lcons_sn (f) (p) (l) (n): + ↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱❨n❩◗l◗p). +// qed. + +(* Basic constructions with proj_rmap ***************************************) + +lemma lift_rmap_d_empty_sn (f) (n): + f = ↑[𝗱❨n❩◗𝐞]f. +// qed. + +lemma lift_rmap_d_lcons_sn (f) (p) (l) (n): + ↑[l◗p](f∘𝐮❨ninj n❩) = ↑[𝗱❨n❩◗l◗p]f. +// qed. + +lemma lift_rmap_L_sn (f) (p): + ↑[p](⫯f) = ↑[𝗟◗p]f. +// qed. + +lemma lift_rmap_A_sn (f) (p): + ↑[p]f = ↑[𝗔◗p]f. +// qed. + +lemma lift_rmap_S_sn (f) (p): + ↑[p]f = ↑[𝗦◗p]f. +// qed. + +(* Advanced eliminations with path ******************************************) + +lemma path_ind_lift (Q:predicate …): + Q 𝐞 → + (∀n. Q 𝐞 → Q (𝗱❨n❩◗𝐞)) → + (∀n,l,p. Q (l◗p) → Q (𝗱❨n❩◗l◗p)) → + (∀p. Q p → Q (𝗟◗p)) → + (∀p. Q p → Q (𝗔◗p)) → + (∀p. Q p → Q (𝗦◗p)) → + ∀p. Q p. +#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p +elim p -p [| * [ #n * ] ] +/2 width=1 by/ +qed-. 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 c0d7dcbf5..ae3ffbdc6 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma @@ -28,9 +28,9 @@ interpretation lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f): k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩. -#A #p elim p -p +#A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ] [ #k1 #k2 #f #Hk lift_lcons_alt >lift_append_rcons_sn - lift_lcons_alt >lift_append_rcons_sn - lift_lcons_alt >lift_append_rcons_sn - lift_lcons_alt >lift_append_rcons_sn - lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt >lift_append_rcons_sn + lift_lcons_alt lift_lcons_alt