From 12d58352dbd62df65d44becc0f69fc5a7b370866 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 May 2022 20:38:32 +0200 Subject: [PATCH] update in ground and delayed_updating + main theorem about dfr proved! + ground: duplicated lemma removed + some refactoring --- .../etc/dhd/downarrowrightsharp_2.etc | 19 +++++ .../delayed_updating/etc/dhd/path_dhd.etc | 70 +++++++++++++++++++ .../etc/dhd/path_dhd_structure.etc | 34 +++++++++ .../delayed_updating/reduction/dfr_ifr.ma | 6 +- .../syntax/path_head_depth.ma | 4 +- .../syntax/path_head_structure.ma | 36 +++++----- .../syntax/path_structure_labels.ma | 25 +++++++ .../unwind/unwind2_rmap_head.ma | 5 +- .../ground/arith/nat_rplus_succ.ma | 3 - .../unwind => ground/relocation}/nap.ma | 0 .../unwind => ground/relocation}/xap.ma | 2 +- 11 files changed, 175 insertions(+), 29 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_2.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_labels.ma rename matita/matita/contribs/lambdadelta/{delayed_updating/unwind => ground/relocation}/nap.ma (100%) rename matita/matita/contribs/lambdadelta/{delayed_updating/unwind => ground/relocation}/xap.ma (96%) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_2.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_2.etc new file mode 100644 index 000000000..171107d6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/downarrowrightsharp_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( ↳⧣[ term 46 n ] break term 70 p )" + non associative with precedence 70 + for @{ 'DownArrowRightSharp $n $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc new file mode 100644 index 000000000..f45fd1f69 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd.etc @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/path_labels.ma". +include "delayed_updating/notation/functions/downarrowrightsharp_2.ma". +include "ground/arith/pnat_plus.ma". + +(* HEAD BY DEPTH FOR PATH ***************************************************) + +rec definition path_dhd (m) (p) on p: path ≝ +match p with +[ list_empty ⇒ 𝗟∗∗m +| list_lcons l q ⇒ + match l with + [ label_d n ⇒ l◗(path_dhd (m+n) q) + | label_m ⇒ l◗(path_dhd m q) + | label_L ⇒ + match m with + [ punit ⇒ l◗𝐞 + | psucc o ⇒ l◗(path_dhd o q) + ] + | label_A ⇒ l◗(path_dhd m q) + | label_S ⇒ l◗(path_dhd m q) + ] +]. + +interpretation + "head by depth (reversed path)" + 'DownArrowRightSharp n p = (path_dhd n p). + +(* basic constructions ****************************************************) + +lemma path_dhd_empty (n:pnat): + (𝗟∗∗n) = ↳⧣[n]𝐞. +// qed. + +lemma path_dhd_d_sn (p) (n) (m): + (𝗱m◗↳⧣[n+m]p) = ↳⧣[n](𝗱m◗p). +// qed. + +lemma path_dhd_m_sn (p) (n): + (𝗺◗↳⧣[n]p) = ↳⧣[n](𝗺◗p). +// qed. + +lemma path_dhd_L_sn_unit (p): + (𝗟◗𝐞) = ↳⧣[𝟏](𝗟◗p). +// qed. + +lemma path_dhd_L_sn_succ (p) (n): + (𝗟◗↳⧣[n]p) = ↳⧣[↑n](𝗟◗p). +// qed. + +lemma path_dhd_A_sn (p) (n): + (𝗔◗↳⧣[n]p) = ↳⧣[n](𝗔◗p). +// qed. + +lemma path_dhd_S_sn (p) (n): + (𝗦◗↳⧣[n]p) = ↳⧣[n](𝗦◗p). +// qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc new file mode 100644 index 000000000..468d7167a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/dhd/path_dhd_structure.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/path_dhd.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_depth.ma". + +(* HEAD BY DEPTH FOR PATH ***************************************************) + +(* Constructions with structure *********************************************) + +lemma path_dhd_structure_L_sn (p) (q): + let r ≝ 𝗟◗p in + ⊗r = ↳⧣[♭⊗r]((⊗r)●q). +#p elim p -p // +* [ #n ] #p #IH #q // + [ list_append_rcons_sn nsucc_unfold >depth_reverse >depth_L_dx >reverse_lcons +[ -H0t1 -Ht1 -Ht2 >structure_L_sn >structure_reverse - H1n >path_head_structure_depth list_append_rcons_sn in H1n; tr_xap_ninj >Hn in ⊢ (??%?); ->(unwind2_rmap_head_append_xap_closed … Hn) -Hn // +>(unwind2_rmap_head_append_xap_closed … Hn) -Hn +