From: Ferruccio Guidi Date: Thu, 17 Nov 2022 22:08:19 +0000 (+0100) Subject: update in delayed_updating X-Git-Tag: make_still_working~25 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f31020f1ae14e28c246b6cd9cf91b5864f4f536a update in delayed_updating + example of unprotected balanced reduction continued and simplified --- diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma index b9b724633..7e4e6dbe3 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma @@ -34,3 +34,12 @@ definition dbfr (r): relation2 prototerm prototerm ≝ interpretation "balanced focused reduction with delayed updating (prototerm)" 'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2). + +(* Constructions with subset_equivalence ************************************) + +lemma dbfr_eq_trans (t) (t1) (t2) (r): + t1 ➡𝐝𝐛𝐟[r] t → t ⇔ t2 → t1 ➡𝐝𝐛𝐟[r] t2. +#t #t1 #t2 #r +* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2 +/3 width=13 by subset_eq_trans, ex6_5_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma new file mode 100644 index 000000000..4dd861087 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dbfr.ma". +include "delayed_updating/substitution/fsubst_constructors.ma". +include "delayed_updating/substitution/fsubst_eq.ma". +include "delayed_updating/syntax/prototerm_constructors_eq.ma". + +(* DELAYED BALANCED FOCUSED REDUCTION ***************************************) + +(* Constructions with constructors for prototerm ****************************) + +lemma dbfr_abst_hd (t1) (t2) (r): + t1 ➡𝐝𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐝𝐛𝐟[𝗟◗r] 𝛌.t2. +#t1 #t2 #r * +#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct +@(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn +[ -Ht2 // +| -Ht2 /2 width=1 by in_comp_abst_hd/ +| @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2 + @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl + @fsubst_eq_repl // @iref_eq_repl + >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) // +] +qed. + +lemma dbfr_appl_hd (v) (t1) (t2) (r): + t1 ➡𝐝𝐛𝐟[r] t2 → ＠v.t1 ➡𝐝𝐛𝐟[𝗔◗r] ＠v.t2. +#v #t1 #t2 #r * +#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct +@(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn +[ -Ht2 // +| -Ht2 /2 width=1 by in_comp_appl_hd/ +| @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ] + @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ] + @fsubst_eq_repl // @iref_eq_repl + >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) // +] +qed. + +lemma dbfr_appl_sd (v1) (v2) (t) (r): + v1 ➡𝐝𝐛𝐟[r] v2 → ＠v1.t ➡𝐝𝐛𝐟[𝗦◗r] ＠v2.t. +#v1 #v2 #t #r * +#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct +@(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn +[ -Hv2 // +| -Hv2 /2 width=1 by in_comp_appl_sd/ +| @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ] + @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ] + @fsubst_eq_repl // @iref_eq_repl + >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) // +] +qed. + +lemma dbfr_beta_0 (v) (t) (q) (n): + q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t → + ＠v.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←𝛕↑n.v]). +#v #t #q #n #Hn #Ht +@(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn +[ // +| // +| // +| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/ +| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ] + @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl + @fsubst_eq_repl // list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … )) + @(subset_eq_canc_sn … (grafted_empty_dx … )) // +] +qed. +(* +lemma dbfr_beta_1 (v) (v1) (t) (q) (n): + q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t → + ＠v.＠v1.𝛌.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]). +#v #v1 #t #q #n #Hn #Ht +@(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn +[ // +| /2 width=1 by pbc_empty, pbc_redex/ +| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/ +| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/ +| @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ] + @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ] + @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl + @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl + @fsubst_eq_repl // list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … )) + @(subset_eq_canc_sn … (grafted_empty_dx … )) // +] +qed. +*) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma index 7c9276021..753d38c68 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma @@ -12,32 +12,33 @@ (* *) (**************************************************************************) +include "delayed_updating/reduction/dbfr_constructors.ma". include "delayed_updating/reduction/ibfr_constructors.ma". +include "delayed_updating/unwind/unwind2_prototerm_constructors.ma". include "delayed_updating/substitution/lift_prototerm_constructors.ma". include "ground/arith/pnat_two.ma". (* DELAYED BALANCED FOCUSED REDUCTION ***************************************) -(* Prerequisites ************************************************************) +(* Example of unprotected balanced β-reduction ******************************) -lemma list_rcons_prop_1 (A) (a1) (a2): - ⓔ ⨭ a1 ⨭{A} a2 = a1 ⨮ (ⓔ ⨭ a2). -// qed. +definition l3_t: prototerm ≝ + (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.⧣𝟏). -(* Example of unprotected balanced β-reduction ******************************) +definition l3_i1: prototerm ≝ + (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣𝟏). -definition l3_t0: prototerm ≝ - (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.⧣𝟏). +definition l3_i2: prototerm ≝ + (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛌.⧣↑𝟐). -definition l3_t1: prototerm ≝ - (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣𝟏)). +definition l3_d1: prototerm ≝ + (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.⧣𝟏). -definition l3_t2: prototerm ≝ - (𝛌.＠(⧣𝟏).＠(𝛌.＠(⧣𝟐).⧣𝟏).𝛌.(𝛌.＠(⧣↑𝟐).⧣↑𝟐)). +definition l3_d2: prototerm ≝ + (＠(⧣𝟏).＠(𝛌.⧣𝟏).𝛌.𝛕𝟏.𝛌.𝛕𝟏.⧣𝟏). -lemma l3_t01: - l3_t0 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝐞] l3_t1. -@ibfr_abst_hd +lemma l3_ti1: + l3_t ➡𝐢𝐛𝐟[𝗔◗𝗔◗𝗟◗𝐞] l3_i1. @ibfr_appl_hd @ibfr_eq_trans [| @ibfr_beta_0 // ] @appl_eq_repl [ // ] @@ -45,24 +46,40 @@ lemma l3_t01: @(subset_eq_canc_sn … (fsubst_empty_rc …)) @(subset_eq_canc_sn … (lift_term_abst …)) @abst_eq_repl -@(subset_eq_canc_sn … (lift_term_appl … )) -@appl_eq_repl @(subset_eq_canc_sn … (lift_term_oref_pap … )) // qed. -lemma l3_t12: - l3_t1 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗔◗𝗟◗𝗟◗𝗔◗𝐞] l3_t2. -@ibfr_abst_hd -@ibfr_eq_trans -[| @(ibfr_beta_1 … (𝟎)) [|