From 3c78efa39d4783f83638b1aabe8d776d83aabf35 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 3 May 2022 19:46:49 +0200 Subject: [PATCH] update in delayed_updating + some notation updated + some unused files removed --- .../delayed_updating/etc/lift/dfr.etc | 37 ------ .../delayed_updating/etc/lift/dfr_ifr.etc | 106 ------------------ .../delayed_updating/etc/lift/fsubst.etc | 28 ----- .../delayed_updating/etc/lift/fsubst_eq.etc | 33 ------ .../delayed_updating/etc/lift/ifr.etc | 36 ------ .../delayed_updating/reduction/dfr.ma | 4 +- .../delayed_updating/reduction/dfr_ifr.ma | 23 +++- .../delayed_updating/reduction/ifr.ma | 4 +- .../delayed_updating/syntax/path_depth.ma | 28 ++--- .../syntax/path_structure_depth.ma | 2 +- .../delayed_updating/unwind1/unwind.ma | 8 +- .../delayed_updating/unwind1/unwind_eq.ma | 10 +- .../unwind1/unwind_structure.ma | 22 ++-- .../unwind1/unwind_structure_depth.ma | 2 +- matita/matita/predefined_virtuals.ml | 2 +- 15 files changed, 60 insertions(+), 285 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_eq.etc delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/ifr.etc diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc deleted file mode 100644 index b568c322a..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr.etc +++ /dev/null @@ -1,37 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/prototerm_constructors.ma". -include "delayed_updating/syntax/prototerm_equivalence.ma". -include "delayed_updating/substitution/fsubst.ma". -include "delayed_updating/substitution/unwind.ma". -include "delayed_updating/syntax/path_structure.ma". -include "delayed_updating/syntax/path_balanced.ma". -include "delayed_updating/syntax/path_depth.ma". -include "delayed_updating/notation/relations/black_rightarrow_df_4.ma". -include "ground/xoa/ex_1_2.ma". -include "ground/xoa/and_4.ma". - -(* DELAYED FOCUSED REDUCTION ************************************************) - -definition dfr (p) (q): relation2 prototerm prototerm ≝ - λt1,t2. ∃∃b,n. - let r ≝ p●𝗔◗b●𝗟◗q in - ∧∧ ⊗b ϵ 𝐁 & ∀f. ↑❘q❘ = (↑[q]⫯f)@❨n❩ & r◖𝗱n ϵ t1 & - t1[⋔r←𝛗(n+❘b❘).(t1⋔(p◖𝗦))] ⇔ t2 -. - -interpretation - "focused balanced reduction with delayed updating (prototerm)" - 'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2). diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc deleted file mode 100644 index 069415421..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/dfr_ifr.etc +++ /dev/null @@ -1,106 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/dfr.ma". -include "delayed_updating/reduction/ifr.ma". -include "delayed_updating/substitution/fsubst_unwind.ma". -include "delayed_updating/substitution/fsubst_eq.ma". -include "delayed_updating/substitution/unwind_constructors.ma". -include "delayed_updating/substitution/unwind_preterm_eq.ma". -include "delayed_updating/substitution/unwind_structure_depth.ma". -include "delayed_updating/substitution/unwind_depth.ma". -include "delayed_updating/syntax/prototerm_proper_constructors.ma". -include "delayed_updating/syntax/path_structure_depth.ma". -include "ground/relocation/tr_uni_compose.ma". -include "ground/relocation/tr_pap_pushs.ma". - -(* DELAYED FOCUSED REDUCTION ************************************************) - -lemma tr_uni_eq_repl (n1) (n2): - n1 = n2 → 𝐮❨n1❩ ≗ 𝐮❨n2❩. -// qed. - -axiom pippo (b) (q) (n): - ↑❘q❘ = (↑[q]𝐢)@❨n❩ → - ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩. - -lemma unwind_rmap_tls_eq_id (p) (n): - ❘p❘ = ↑[p]𝐢@❨n❩ → - (𝐢) ≗ ⇂*[n]↑[p]𝐢. -#p @(list_ind_rcons … p) -p -[ #n tr_pushs_swap tr_id_unfold #Hn - lapply (pippo … b … Hn) -Hn #Hn - @tr_compose_eq_repl - [ Hn @(subset_eq_canc_sn … (lift_term_eq_repl_dx …)) [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ] - + unwind_lcons_alt // >unwind_append_rcons_sn //