From e6482f7f499fbb88aff8a205d2a2c808158042c5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 27 Apr 2022 19:24:30 +0200 Subject: [PATCH] update un delayed updating + some parked files --- .../etc/relocation/sbr_pap.etc | 48 ++++ .../etc/relocation/sbr_pap_eq.etc | 30 ++ .../relocation/sbr_pap_id.etc} | 20 +- .../etc/relocation/sbr_pap_push.etc | 31 ++ .../etc/relocation/sbr_push.etc | 30 ++ .../relocation/sbr_push_eq.etc} | 23 +- .../etc/relocation/sbr_push_uni.etc | 24 ++ .../etc/relocation/upspoonverticalbar_2.etc | 19 ++ .../etc/relocation/verticalbarat_2.etc | 19 ++ .../unwind.ma => etc/unwind2/unwind.etc} | 0 .../unwind2/unwind_constructors.etc} | 0 .../unwind2/unwind_depth.etc} | 0 .../unwind2/unwind_eq.etc} | 0 .../etc/unwind2/unwind_etc.etc | 10 + .../unwind2/unwind_fsubst.etc} | 0 .../unwind2/unwind_height.etc} | 0 .../unwind2/unwind_preterm_eq.etc} | 0 .../unwind2/unwind_prototerm.etc} | 0 .../unwind2/unwind_prototerm_eq.etc} | 0 .../unwind2/unwind_structure.etc} | 0 .../unwind2/unwind_structure_depth.etc} | 0 .../delayed_updating/etc/unwind3/unwind.etc | 189 ++++++++++++ .../etc/unwind3/unwind_constructors.etc | 44 +++ .../etc/unwind3/unwind_depth.etc | 31 ++ .../etc/unwind3/unwind_eq.etc | 124 ++++++++ .../etc/unwind3/unwind_fsubst.etc | 61 ++++ .../etc/unwind3/unwind_length.etc | 35 +++ .../etc/unwind3/unwind_lift.etc | 32 +++ .../etc/unwind3/unwind_preterm_eq.etc | 68 +++++ .../etc/unwind3/unwind_prototerm.etc | 30 ++ .../etc/unwind3/unwind_prototerm_eq.etc | 41 +++ .../etc/unwind3/unwind_structure.etc | 269 ++++++++++++++++++ .../etc/unwind3/unwind_structure_depth.etc | 31 ++ 33 files changed, 1181 insertions(+), 28 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap_eq.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/lift_id.ma => etc/relocation/sbr_pap_id.etc} (75%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap_push.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_push.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/lift_prototerm_id.ma => etc/relocation/sbr_push_eq.etc} (70%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_push_uni.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/upspoonverticalbar_2.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/verticalbarat_2.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind.ma => etc/unwind2/unwind.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_constructors.ma => etc/unwind2/unwind_constructors.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_depth.ma => etc/unwind2/unwind_depth.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_eq.ma => etc/unwind2/unwind_eq.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_fsubst.ma => etc/unwind2/unwind_fsubst.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_height.ma => etc/unwind2/unwind_height.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_preterm_eq.ma => etc/unwind2/unwind_preterm_eq.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_prototerm.ma => etc/unwind2/unwind_prototerm.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_prototerm_eq.ma => etc/unwind2/unwind_prototerm_eq.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_structure.ma => etc/unwind2/unwind_structure.etc} (100%) rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind2/unwind_structure_depth.ma => etc/unwind2/unwind_structure_depth.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_constructors.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_depth.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_eq.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_fsubst.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_length.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_lift.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_preterm_eq.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure_depth.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap.etc new file mode 100644 index 000000000..c35244d88 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/arith/pnat_plus.ma". +include "ground/relocation/tr_map.ma". +include "delayed_updating/notation/functions/verticalbarat_2.ma". + +(* POSITIVE APPLICATION FOR STACKS OF BASIC RELOCATION MAPS *****************) + +rec definition sbr_pap (i: pnat) on i: tr_map → pnat. +* #p #f cases i -i +[ @(p) +| #i cases p -p + [ lapply (sbr_pap i f) -sbr_pap -i -f + #i @(↑i) + | #p @(i+↑p) + ] +] +defined. + +interpretation + "functional positive application (stack of relocation maps)" + 'VerticalBarAt f i = (sbr_pap i f). + +(* Basic constructions ******************************************************) + +lemma sbr_pap_unfold_unit (f): + ∀p. p = (p⨮f)❘@❨𝟏❩. +// qed. + +lemma sbr_pap_unfold_unit_succ (f): + ∀i. ↑(f❘@❨i❩) = (𝟏⨮f)❘@❨↑i❩. +// qed. + +lemma sbr_pap_unfold_succ_bi (f): + ∀p,i. i+↑p = (↑p⨮f)❘@❨↑i❩. +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap_eq.etc new file mode 100644 index 000000000..10b0d939e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_pap_eq.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/sbr_pap.ma". +include "ground/relocation/tr_eq.ma". + +(* POSITIVE APPLICATION FOR STACKS OF BASIC RELOCATION MAPS *****************) + +(* Main constructions with stream_eq ****************************************) + +theorem sbr_pap_eq_repl_sn (i): + stream_eq_repl … (λf1,f2. f1❘@❨i❩ = f2❘@❨i❩). +#i elim i -i [| #i #IH ] +* [ #p1 | * [| #p1 ]] #f1 +* #p2 #f2 #H +elim (stream_eq_inv_cons_bi … H) -H [1,8,15: |*: // ] #Hp #Hf destruct // +(lift_path_id p) -/2 width=1 by in_comp_lift_bi/ -qed-. +(* PUSH FOR STACKS OF BASIC RELOCATION MAPS *********************************) -lemma lift_term_id_dx (t): - ↑[𝐢]t ⊆ t. -#t #p * #q #Hq #H destruct // -qed-. +(* Main constructions with stream_eq ****************************************) -lemma lift_term_id (t): - t ⇔ ↑[𝐢]t. -/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/ -qed. +theorem sbr_push_eq_repl_dx (p): + stream_eq_repl … (λf1,f2. p⫯❘f1 ≗ p⫯❘f2). +/2 width=1 by stream_eq_cons/ qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_push_uni.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_push_uni.etc new file mode 100644 index 000000000..edfd82efd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/sbr_push_uni.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/sbr_push.ma". +include "ground/relocation/tr_uni.ma". + +(* PUSH FOR STACKS OF BASIC RELOCATION MAPS *********************************) + +(* Constructions with tr_uni ************************************************) + +theorem sbr_push_id (p:pnat): + (𝐮❨p❩) = p⫯❘𝐢. +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/upspoonverticalbar_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/upspoonverticalbar_2.etc new file mode 100644 index 000000000..4b4866516 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/upspoonverticalbar_2.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation "hvbox( hd ⫯❘ break tl )" + right associative with precedence 47 + for @{ 'UpSpoonVerticalBar $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/verticalbarat_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/verticalbarat_2.etc new file mode 100644 index 000000000..ce7cd1410 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/relocation/verticalbarat_2.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR DELAYED UPDATING ********************************************) + +notation "hvbox( f ❘@❨ break term 46 a ❩ )" + non associative with precedence 60 + for @{ 'VerticalBarAt $f $a }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_constructors.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_constructors.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_constructors.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_depth.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_depth.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_depth.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_eq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind2/unwind_eq.ma rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_eq.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc new file mode 100644 index 000000000..a9e563db6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_etc.etc @@ -0,0 +1,10 @@ +include "delayed_updating/unwind2/unwind_depth.ma". +include "ground/relocation/tr_uni_compose.ma". + +lemma pippo (q) (p): + ▼[p]𝐢 ≗ ⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢. +#q @(list_ind_rcons … q) -q // +#q * [ #n ] #IH #p // +list_cons_shift list_cons_shift unwind_lcons_alt // >unwind_append_rcons_sn // + unwind_lcons_alt >unwind_append_rcons_sn // + unwind_lcons_alt >unwind_append_rcons_sn // + unwind_lcons_alt unwind_append_proper_dx + /4 width=5 by in_comp_unwind_bi, in_ppc_comp_trans, or_introl, ex2_intro/ +| * #q #Hq #H1 #H0 + @(ex2_intro … H1) @or_intror @conj // * + [ list_cons_shift list_cons_shift unwind_rmap_S_dx >structure_S_dx + @unwind_grafted_sn // +| /2 width=1 by unwind_grafted_S_dx/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc new file mode 100644 index 000000000..c4a103b61 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind3/unwind.ma". +include "delayed_updating/syntax/prototerm.ma". +include "ground/lib/subset_ext.ma". + +(* UNWIND FOR PROTOTERM *****************************************************) + +interpretation + "unwind (prototerm)" + 'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind_gen ? proj_path f) t). + +(* Basic constructions ******************************************************) + +lemma in_comp_unwind_bi (f) (p) (t): + p ϵ t → ▼[f]p ϵ ▼[f]t. +/2 width=1 by subset_in_ext_f1_dx/ +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc new file mode 100644 index 000000000..01d302f3e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_prototerm_eq.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind3/unwind_eq.ma". +include "delayed_updating/unwind3/unwind_prototerm.ma". + +(* UNWIND FOR PROTOTERM *****************************************************) + +(* Constructions with subset_equivalence ************************************) + +lemma unwind_term_eq_repl_sn (f1) (f2) (t): + f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t. +/3 width=1 by subset_equivalence_ext_f1_exteq, unwind_path_eq_repl/ +qed. + +lemma unwind_term_eq_repl_dx (f) (t1) (t2): + t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2. +/2 width=1 by subset_equivalence_ext_f1_bi/ +qed. + +lemma unwind_term_after_id_sn (f) (t): + ▼[𝐢]▼[f]t ⇔ ▼[f]t. +#f #t @subset_eq_trans +[ +| @subset_inclusion_ext_f1_compose +| @subset_equivalence_ext_f1_exteq + #p @unwind_path_after_id_sn +] +qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc new file mode 100644 index 000000000..c52a43871 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure.etc @@ -0,0 +1,269 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unwind3/unwind_eq.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_inner.ma". +include "delayed_updating/syntax/path_proper.ma". +include "ground/xoa/ex_4_2.ma". + +(* UNWIND FOR PATH *********************************************************) + +(* Basic constructions with structure **************************************) + +lemma structure_unwind (p) (f): + ⊗p = ⊗▼[f]p. +#p @(path_ind_unwind … p) -p // #p #IH #f +