From d108bcea8ebae11b03e8d8a155dfd3f2eb445127 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 11 Dec 2022 19:29:08 +0100 Subject: [PATCH] update in delayed_updating + bug fixed in the "crux of the proof" allows to certify more reductions + restricted form of closed path not used anymore --- .../etc/height/path_closed_height.etc | 19 ++- .../etc/height/unwind2_rmap_closed_height.etc | 44 +++++++ .../reduction/dbfr_constructors.etc} | 0 .../reduction/dbfr_unprotected.etc} | 0 .../reduction/ibfr_constructors.etc} | 0 .../etc/unwind2_rmap_closed_1.etc | 110 ++++++++++++++++ .../etc/unwind2_rmap_closed_2.etc | 57 ++++++++ .../lambdadelta/delayed_updating/names.txt | 2 + .../lambdadelta/delayed_updating/notes.txt | 7 +- .../delayed_updating/reduction/dbfr.ma | 10 +- .../delayed_updating/reduction/dbfr_ibfr.ma | 49 +++---- .../delayed_updating/reduction/dbfr_lift.ma | 19 +-- .../delayed_updating/reduction/ibfr.ma | 10 +- .../delayed_updating/reduction/ibfr_eq.ma | 36 ++++++ .../delayed_updating/reduction/ibfr_lift.ma | 19 +-- .../delayed_updating/reduction/ibfr_unwind.ma | 59 +++++---- .../substitution/lift_rmap_closed.ma | 3 +- .../delayed_updating/syntax/prototerm_eq.ma | 12 ++ .../unwind/unwind2_rmap_closed.ma | 122 ++++-------------- .../unwind/unwind2_rmap_crux.ma | 46 +++++++ ...p_unprotected.ma => unwind2_rmap_guard.ma} | 37 ++---- 21 files changed, 453 insertions(+), 208 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/height/unwind2_rmap_closed_height.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_constructors.ma => etc/reduction/dbfr_constructors.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_unprotected.ma => etc/reduction/dbfr_unprotected.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/ibfr_constructors.ma => etc/reduction/ibfr_constructors.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_1.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_eq.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind2_rmap_unprotected.ma => unwind2_rmap_guard.ma} (58%) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc index 88b0e413f..72b6dead7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/height/path_closed_height.etc @@ -18,10 +18,17 @@ include "delayed_updating/syntax/path_depth.ma". (* CLOSED CONDITION FOR PATH ************************************************) -(* Constructions with height and depth **************************************) +(* Destructions with height and depth ***************************************) -lemma path_closed_depth (p) (n): - p ϵ 𝐂❨n❩ → ♯p + n = ♭p. -#p #n #Hn elim Hn -Hn // -#p #n #_ #IH (npsucc_pred k) in ⊢ (%→?); (path_closed_des_succ_depth … Hq) +@(stream_eq_trans … (tls_unwind2_rmap_d_dx …)) +>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold +<(path_closed_des_succ_depth … Hq) -Hq +H0 -H0 Ho // Ho // nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold +>nplus_succ_dx (xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb +>(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq // +qed-. + +lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n): + b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ → + ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q). +#o #f #p #b #q #m #n #Hb #Hq +>nplus_succ_dx list_append_assoc +@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb +/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc new file mode 100644 index 000000000..58b1aab8d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap_closed_2.etc @@ -0,0 +1,57 @@ +include "delayed_updating/unwind/unwind2_rmap_closed.ma". + +lemma pippo (o) (q) (n): + (q◖𝗟) ϵ 𝐂❨o,n❩ → + (𝗟◗q) ϵ 𝐂❨o,n❩. +#o #q elim q -q // +* [ #k ] #q #IH #n #H0 +elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn +[ elim (pcc_inv_d_dx … H0) -H0 #_ #H0 + >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/ +| lapply (pcc_inv_m_dx … H0) -H0 #H0 + >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/ +| elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn + >Hn -Hn /4 width=1 by pcc_L_dx/ +| lapply (pcc_inv_A_dx … H0) -H0 #H0 + >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/ +| lapply (pcc_inv_S_dx … H0) -H0 #H0 + >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/ +] +qed-. + + +lemma pippo (o) (f) (q) (n): + q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q＠⧣❨↑n❩. +#o #f #q #n #H0 elim H0 -q -n // +#q #n [ #k #_ ] #_ #IH +[ list_append_rcons_dx >list_append_assoc - unwind2_rmap_A_dx - /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/ - ] + /2 width=1 by unwind2_rmap_uni_crux/ (* Note: crux of the proof ends *) | // | /2 width=2 by ex_intro/ | // ] ] +qed-. + +theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ 𝐓 → + t1 ➡𝐝𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2. +#f #t1 #t2 #r #Ht1 #Ht12 +lapply (dbfr_des_ibfr_push (𝐢) … Ht1 Ht12) -Ht1 -Ht12 #Ht12 +/2 width=1 by ibfr_structure_unwind_bi/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma index 0c6ab932f..e1446df2d 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma @@ -19,6 +19,7 @@ include "delayed_updating/substitution/fsubst_eq.ma". include "delayed_updating/substitution/lift_prototerm_constructors.ma". include "delayed_updating/substitution/lift_path_structure.ma". include "delayed_updating/substitution/lift_path_closed.ma". +include "delayed_updating/substitution/lift_path_guard.ma". include "delayed_updating/substitution/lift_rmap_closed.ma". (* DELAYED BALANCED FOCUSED REDUCTION ***************************************) @@ -28,17 +29,19 @@ include "delayed_updating/substitution/lift_rmap_closed.ma". theorem dbfr_lift_bi (f) (t1) (t2) (r): t1 ➡𝐝𝐛𝐟[r] t2 → 🠡[f]t1 ➡𝐝𝐛𝐟[🠡[f]r] 🠡[f]t2. #f #t1 #t2 #r -* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct -@(ex6_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩)) -[ -Hb -Hm -Hn -Ht1 -Ht2 // -| -Hm -Hn -Ht1 -Ht2 // -| -Hb -Hn -Ht1 -Ht2 +* #p #b #q #m #n #Hr #Hp #Hb #Hm #Hn #Ht1 #Ht2 destruct +@(ex7_5_intro … (🠡[f]p) (🠡[🠢[f](p◖𝗔)]b) (🠡[🠢[f](p◖𝗔●b◖𝗟)]q) (🠢[f](p●𝗔◗b)＠❨m❩) (🠢[f](p●𝗔◗b●𝗟◗q)＠§❨n❩)) +[ -Hp -Hb -Hm -Hn -Ht1 -Ht2 // +| -Hb -Hm -Hn -Ht1 -Ht2 + /2 width=1 by lift_path_guard/ +| -Hp -Hm -Hn -Ht1 -Ht2 // +| -Hp -Hb -Hn -Ht1 -Ht2 /2 width=1 by lift_path_closed/ -| -Hb -Hm -Ht1 -Ht2 +| -Hp -Hb -Hm -Ht1 -Ht2 /2 width=1 by lift_path_rmap_closed_L/ -| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn +| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -Hn -Hp list_append_assoc - unwind2_rmap_A_dx - /2 width=2 by tls_succ_plus_unwind2_rmap_append_closed_bLq_dx/ - ] + /2 width=1 by unwind2_rmap_uni_crux/ (* Note: crux of the proof ends *) | // | /2 width=2 by ex_intro/ | // ] ] +qed-. + +lemma ibfr_unwind_bi (f) (t1) (t2) (r): + t1 ϵ 𝐓 → r ϵ 𝐈 → + t1 ➡𝐢𝐛𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐛𝐟[⊗r] ▼[f]t2. +#f #t1 #t2 #r #Ht1 #Hr #Ht12 +lapply (ibfr_unwind_bi_push (𝐢) … Ht1 Hr Ht12) -Ht1 -Hr -Ht12 #Ht12 +/2 width=1 by ibfr_structure_unwind_bi/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma index ec386108e..9e8a3a99e 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma @@ -59,7 +59,8 @@ qed-. lemma nap_plus_lift_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n): q ϵ 𝐂❨o,n❩ → - 🠢[f](p)＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩. + 🠢[f]p＠❨m❩+🠢[f](p●𝗟◗q)＠§❨n❩ = 🠢[f](p●𝗟◗q)＠§❨m+n❩. #o #f #p #q #m #n #Hq +H0 -H0 Ho // (nplus_zero_sn n) +<(nap_plus_unwind2_rmap_append_closed_Lq_dx … Hn) -Hn +nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold // qed-. -lemma tls_plus_unwind2_rmap_closed_true (f) (q) (n): - q ϵ 𝐂❨Ⓣ,n❩ → - ∀m. ⇂*[m]f ≗ ⇂*[m+n]▶[f]q. -#f #q #n #Hq elim Hq -q -n // -#q #n #k #Ho #_ #IH #m ->Ho // nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold ->nplus_succ_dx (xap_unwind2_rmap_append_closed_true_dx_depth f p … Hb) -Hb ->(nap_plus_unwind2_rmap_append_closed_Lq_dx_depth … Hq) -Hq // -qed-. - -lemma tls_succ_plus_unwind2_rmap_append_closed_bLq_dx (o) (f) (p) (b) (q) (m) (n): - b ϵ 𝐂❨Ⓣ,m❩ → q ϵ 𝐂❨o,n❩ → - ▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●b●𝗟◗q). -#o #f #p #b #q #m #n #Hb #Hq ->nplus_succ_dx list_append_assoc -@(stream_eq_trans … (tls_unwind2_rmap_append_closed_true_dx … Hb)) -Hb -/3 width=2 by stream_tls_eq_repl, tls_succ_unwind2_rmap_append_closed_Lq_dx/ + ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q). +#o #f #p #q #n #Hn #m +/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/ qed-. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma new file mode 100644 index 000000000..c919221da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind/unwind2_rmap_closed.ma". +include "delayed_updating/unwind/unwind2_rmap_guard.ma". + +(* TAILED UNWIND FOR RELOCATION MAP *****************************************) + +(* Crucial constructions with tr_uni ****************************************) + +(* Note: crux of the commutation between unwind and balanced focused reduction *) +lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n): + p ϵ 𝐆 → b ϵ 𝐂❨Ⓕ,m❩ → q ϵ 𝐂❨Ⓕ,n❩ → + (𝐮❨↑(♭b+♭q)❩ ∘ ▶[⫯f]p ≗ ▶[⫯f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩). +#f #p #b #q #m #n #Hp #Hm #Hn +list_append_assoc +>list_append_rcons_sn >(list_append_rcons_sn … b) +@(stream_eq_trans … (tr_compose_uni_dx_pap …)) nsucc_unfold >nplus_succ_dx >nplus_succ_dx tr_nap_plus_dx stream_tls_succ