From 61bc42e04598a9f5e489c3867af72e700c7fda04 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Aug 2022 00:20:11 +0200 Subject: [PATCH] partial commit in delayed_updating + reversing paths in component "unwind" --- .../black_diamond_2.etc} | 0 .../black_downtriangle_1.etc} | 0 .../black_righttriangle_1.etc} | 0 .../delayed_updating/etc/unwind2_rmap.etc | 5 + .../substitution/lift_path.ma | 1 - .../substitution/lift_rmap_eq.ma | 12 +- .../delayed_updating/syntax/path_inner.ma | 34 +++ .../delayed_updating/syntax/path_structure.ma | 157 ++++++++++ .../unwind/preunwind2_rmap.ma | 55 ++++ ...ind_gen_after.ma => preunwind2_rmap_eq.ma} | 18 +- .../unwind/preunwind2_rmap_lift.ma | 34 +++ .../unwind/unwind2_constructors.ma | 21 +- .../delayed_updating/unwind/unwind2_path.ma | 180 +++++++++--- .../unwind2_path_after.ma} | 21 +- .../unwind/unwind2_path_append.ma | 244 ++++++++++++++++ .../unwind/unwind2_path_eq.ma | 22 +- .../unwind/unwind2_path_lift.ma | 44 ++- .../unwind/unwind2_path_structure.ma | 123 -------- .../unwind/unwind2_preterm_eq.ma | 26 +- .../unwind/unwind2_preterm_fsubst.ma | 20 +- .../unwind/unwind2_prototerm.ma | 2 +- ...d_gen_eq.ma => unwind2_prototerm_after.ma} | 27 +- .../unwind/unwind2_prototerm_eq.ma | 11 +- .../unwind/unwind2_prototerm_inner.ma | 4 +- .../unwind/unwind2_prototerm_lift.ma | 6 +- .../delayed_updating/unwind/unwind2_rmap.ma | 89 +++--- .../unwind/unwind2_rmap_after.ma | 36 +++ .../unwind/unwind2_rmap_eq.ma | 24 +- .../unwind/unwind2_rmap_head.ma | 107 +++---- .../unwind/unwind2_rmap_labels.ma | 4 +- .../unwind/unwind2_rmap_lift.ma | 43 +++ .../unwind/unwind2_rmap_structure.ma | 13 +- .../delayed_updating/unwind/unwind_gen.ma | 86 ------ .../unwind/unwind_gen_structure.ma | 269 ------------------ 34 files changed, 954 insertions(+), 784 deletions(-) rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_diamond_2.ma => etc/black_diamond_2.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_downtriangle_1.ma => etc/black_downtriangle_1.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_righttriangle_1.ma => etc/black_righttriangle_1.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind_gen_after.ma => preunwind2_rmap_eq.ma} (70%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/uparrow_4.ma => unwind/unwind2_path_after.ma} (66%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind_gen_eq.ma => unwind2_prototerm_after.ma} (61%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_diamond_2.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_diamond_2.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_1.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_1.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_righttriangle_1.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_righttriangle_1.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc new file mode 100644 index 000000000..7a18aa34e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc @@ -0,0 +1,5 @@ +include "delayed_updating/notation/functions/black_righttriangle_1.ma". + +interpretation + "unwind map (reversed path)" + 'BlackRightTriangle p = (unwind2_rmap tr_id p). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma index 1ffe94862..2154e4a55 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma @@ -14,7 +14,6 @@ include "delayed_updating/substitution/prelift_label.ma". include "delayed_updating/substitution/lift_rmap.ma". -include "ground/xoa/ex_3_2.ma". (* LIFT FOR PATH ************************************************************) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma index a2f841e43..bf5151f00 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma @@ -13,9 +13,8 @@ (**************************************************************************) include "delayed_updating/substitution/lift_rmap.ma". -include "ground/relocation/tr_pn_eq.ma". +include "delayed_updating/substitution/prelift_rmap_eq.ma". include "ground/lib/stream_tls_plus.ma". -include "ground/lib/stream_tls_eq.ma". include "ground/arith/nat_plus_rplus.ma". include "ground/arith/nat_rplus_pplus.ma". @@ -26,13 +25,8 @@ include "ground/arith/nat_rplus_pplus.ma". lemma lift_rmap_eq_repl (p): stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2). #p elim p -p // -* [ #k ] #p #IH #f1 #f2 #Hf -[ /3 width=1 by stream_tls_eq_repl/ -| /2 width=1 by/ -| /3 width=1 by tr_push_eq_repl/ -| /2 width=1 by/ -| /2 width=1 by/ -] +#l #p #IH #f1 #f2 #Hf +/3 width=1 by prelift_rmap_eq_repl/ qed. lemma tls_lift_rmap_d_dx (f) (p) (n) (k): diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma index 98501e8df..0db6d2f65 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma @@ -59,3 +59,37 @@ lemma pic_inv_d_dx (p) (k): p◖𝗱k ϵ 𝐈 → ⊥. #p #k #H0 @H0 -H0 // qed-. + +(* Constructions with path_lcons ********************************************) + +lemma pic_m_sn (p): + p ϵ 𝐈 → 𝗺◗p ϵ 𝐈. +* [| * [ #k ] #p #Hp list_cons_comm #H0 +elim (eq_inv_append_structure … H0) -H0 #r1 #r2 +list_cons_comm #H0 +elim (eq_inv_append_structure … H0) -H0 #r1 #r2 +list_cons_comm #H0 +elim (eq_inv_append_structure … H0) -H0 #r1 #r2 +list_cons_comm #H0 +elim (eq_inv_append_structure … H0) -H0 #r1 #r2 +list_cons_comm #H0 +elim (eq_inv_append_structure … H0) -H0 #r1 #r2 + "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 70 - for @{ 'UpArrow ? $k $p $f }. +(* Properties with tr_after *************************************************) -notation > "hvbox( ↑{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )" - non associative with precedence 70 - for @{ 'UpArrow $S $k $p $f }. +lemma unwind2_path_after (g) (f) (p): + ▼[g]▼[f]p = ▼[g∘f]p. +#g #f * // * [ #k ] #p // +tr_compose_pap +/2 width=3 by tr_pap_eq_repl/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma new file mode 100644 index 000000000..3114e9edd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma @@ -0,0 +1,244 @@ +(**************************************************************************) +(* ___ *) +(* ||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_path.ma". +include "delayed_updating/syntax/path_inner.ma". +include "delayed_updating/syntax/path_proper.ma". +include "ground/xoa/ex_4_2.ma". + +(* TAILED UNWIND FOR PATH ***************************************************) + +(* Constructions with inner condition for path ******************************) + +lemma unwind2_path_inner (f) (p): + p ϵ 𝐈 → ⊗p = ▼[f]p. +#f * // * // #k #q #Hq +elim (pic_inv_d_dx … Hq) +qed-. + +(* Constructions with append and inner condition for path *******************) + +lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 → + (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q). +#f #p * [ #Hp | * [ #k ] #q #_ ] // +[ <(unwind2_path_inner … Hp) -Hp // +| list_cons_comm #H0 + elim (unwind2_path_inv_append_proper_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2 + elim (eq_inv_d_dx_structure … Hr1) +] +qed-. + +lemma eq_inv_m_sn_unwind2_path (f) (q) (p): + (𝗺◗q) = ▼[f]p → ⊥. +#f #q #p +>list_cons_comm #H0 +elim (unwind2_path_des_append_inner_sn … H0) list_cons_comm #H0 +elim (unwind2_path_des_append_inner_sn … H0) list_cons_comm #H0 +elim (unwind2_path_des_append_inner_sn … H0) list_cons_comm #H0 +elim (unwind2_path_des_append_inner_sn … H0) (unwind2_path_eq_repl … (tr_compose_assoc …)) // -| <(unwind2_path_L_sn … f1) tr_compose_push_bi // -] -qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma index ac2166a46..5af9e1664 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma @@ -12,35 +12,31 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_path_eq.ma". -include "delayed_updating/substitution/lift_path_prelift.ma". +include "delayed_updating/unwind/unwind2_path.ma". +include "delayed_updating/unwind/unwind2_rmap_lift.ma". +include "delayed_updating/substitution/lift_path_structure.ma". -(* UNWIND FOR PATH **********************************************************) +(* TAILED UNWIND FOR PATH ***************************************************) (* Constructions with lift_path *********************************************) -lemma lift_unwind2_path_after (p) (f1) (f2): - ↑[f2]▼[f1]p = ▼[f2∘f1]p. -#p @(path_ind_unwind … p) -p // [ #n | #p ] #IH #f1 #f2 -[ tr_compose_push_bi // -] +lemma lift_unwind2_path_after (g) (f) (p): + ↑[g]▼[f]p = ▼[g∘f]p. +#g #f * // * [ #k ] #p // +tr_compose_pap +/4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/ qed. -lemma unwind2_path_after_lift (p) (f1) (f2): - ▼[f2]↑[f1]p = ▼[f2∘f1]p. -#p @(path_ind_unwind … p) -p // [ #n #l ] #p #IH #f1 #f2 -[ lift_path_lcons_prelift - >IH -IH - >(unwind2_path_eq_repl … (tr_compose_assoc …)) - >(unwind2_path_eq_repl … (tr_compose_assoc …)) - tr_compose_push_bi // +lemma unwind2_lift_path_after (g) (f) (p): + ▼[g]↑[f]p = ▼[g∘f]p. +#g #f * // * [ #k ] #p +[ tr_compose_pap + /4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/ +| (Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p /2 width=1 by in_comp_unwind2_path_term/ qed-. lemma unwind2_term_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 → - ▼[▶[f]pᴿ](t⋔p) ⇔ (▼[f]t)⋔(⊗p). + ▼[▶[f]p](t⋔p) ⇔ (▼[f]t)⋔(⊗p). /3 width=1 by unwind2_term_grafted_sn, unwind2_term_grafted_dx, conj/ qed. lemma unwind2_term_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 → - (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]pᴿ](t⋔(p◖𝗦)). + (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]p](t⋔(p◖𝗦)). #f #t #p #Hp #Ht #q * #r #Hr -list_append_rcons_sn #H0 elim (unwind2_path_inv_append_proper_dx … (sym_eq … H0)) -H0 // #p0 #q0 #Hp0 #Hq0 #H0 destruct -<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p -elim (unwind2_path_inv_S_sn … (sym_eq … Hq0)) -Hq0 +>(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p +elim (eq_inv_S_sn_unwind2_path … Hq0) -Hq0 #r1 #r2 #Hr1 #Hr2 #H0 destruct lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1) [ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct @@ -57,10 +57,10 @@ lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1) qed-. lemma unwind2_term_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 → - ▼[▶[f]pᴿ](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦). + ▼[▶[f]p](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦). #f #t #p #Hp #Ht @conj -[ >unwind2_rmap_S_sn >reverse_rcons >structure_S_dx +[ >unwind2_rmap_S_dx >structure_S_dx @unwind2_term_grafted_sn // (**) (* auto fails *) | /2 width=1 by unwind2_term_grafted_S_dx/ ] diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma index 452c913e5..19634dccc 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma @@ -13,33 +13,33 @@ (**************************************************************************) include "delayed_updating/unwind/unwind2_prototerm_eq.ma". -include "delayed_updating/unwind/unwind2_path_structure.ma". +include "delayed_updating/unwind/unwind2_path_append.ma". include "delayed_updating/substitution/fsubst.ma". include "delayed_updating/syntax/preterm.ma". include "delayed_updating/syntax/prototerm_proper.ma". -(* UNWIND FOR PRETERM *******************************************************) +(* TAILED UNWIND FOR PRETERM ************************************************) (* Constructions with fsubst ************************************************) lemma unwind2_term_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 → - (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u] ⊆ ▼[f](t[⋔p←u]). + (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]). #f #t #u #p #Hu #ql * * [ #rl * #r #Hr #H1 #H2 destruct >unwind2_path_append_proper_dx /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/ | * #q #Hq #H1 #H0 @(ex2_intro … H1) @or_intror @conj // * - [ nrplus_inj_dx +lemma tls_unwind2_rmap_d_dx (f) (p) (n) (k): + ⇂*[n+k]▶[f]p ≗ ⇂*[n]▶[f](p◖𝗱k). +#f #p #n #k +nrplus_inj_dx /2 width=1 by tr_tls_compose_uni_dx/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma index f6fbae181..853f07e9c 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma @@ -19,45 +19,45 @@ include "ground/relocation/xap.ma". include "ground/lib/stream_eq_eq.ma". include "ground/arith/nat_le_plus.ma". -(* UNWIND MAP FOR PATH ******************************************************) +(* TAILED UNWIND FOR RELOCATION MAP *****************************************) (* Constructions with path_head *********************************************) -lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k): - p = ↳[n]p → k ≤ n → - ▶[f](p●q)@❨k❩ = ▶[f]↳[n](p●q)@❨k❩. -#f #p elim p -p -[ #q #n #k #Hq - <(eq_inv_path_empty_head … Hq) -n #Hk - <(nle_inv_zero_dx … Hk) -k // -| #l #p #IH #q #n @(nat_ind_succ … n) -n - [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH // - | #n #_ #k cases l [ #m ] - [ IH -IH IH -IH tr_xap_ninj >(path_head_refl_append q … Hn) in ⊢ (??%?); +>tr_xap_ninj >(path_head_refl_append p … Hn) in ⊢ (??%?); >(unwind2_rmap_head_xap_closed … Hn) -Hn nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn