From: Ferruccio Guidi Date: Wed, 25 May 2022 18:38:32 +0000 (+0200) Subject: update in ground and delayed_updating X-Git-Tag: make_still_working~67 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=12d58352dbd62df65d44becc0f69fc5a7b370866;p=helm.git update in ground and delayed_updating + main theorem about dfr proved! + ground: duplicated lemma removed + some refactoring --- 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 +tr_compose_nap >tr_compose_push_bi // -qed. - -lemma tr_uni_xap_succ (n) (m): - ↑m + n = 𝐮❨n❩@❨↑m❩. -#n #m -tr_pushs_succ tr_compose_nap >tr_compose_push_bi // +qed. + +lemma tr_uni_xap_succ (n) (m): + ↑m + n = 𝐮❨n❩@❨↑m❩. +#n #m +tr_pushs_succ