From ad49f5895fadff5a1d9845debb1c852a1455c6c9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 15 Feb 2022 00:21:15 +0100 Subject: [PATCH] update in ground + additions to tr_compose --- .../lambdadelta/ground/etc/relocation/tr.etc | 8 ----- .../lambdadelta/ground/lib/stream_tls.ma | 6 ++++ .../ground/relocation/tr_id_compose.ma | 31 +++++++++++++++++++ .../ground/relocation/tr_uni_compose.ma | 28 +++++++++++++++-- .../lambdadelta/ground/web/ground_src.tbl | 2 +- 5 files changed, 64 insertions(+), 11 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc index ba3287eb6..a0aba6e51 100644 --- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc +++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc @@ -3,14 +3,6 @@ lemma pippo (f): * #p #f // qed. -corec lemma tr_compose_id_dx (f): - f ≗ f∘𝐢. -cases tr_id_unfold -cases tr_compose_unfold -cases (pippo f) in ⊢ (??%?); -@stream_eq_cons /2 width=1 by/ -qed. - axiom pippo2 (f) (p): f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma index b2f042c1f..eb7210e22 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma @@ -46,3 +46,9 @@ qed. lemma stream_tls_swap (A) (n) (t): (⇂*[n]⇂t) = ⇂*{A}[↑n]t. // qed. + +(* Advanced constructions ***************************************************) + +lemma stream_tls_unit (A) (t): + ⇂t = ⇂*{A}[𝟏]t. +// qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma new file mode 100644 index 000000000..518154d68 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_compose.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/tr_id_pap.ma". +include "ground/relocation/tr_compose_pap.ma". +include "ground/relocation/tr_pap_eq.ma". + +(* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************) + +(* Coonstructions with tr_compose *******************************************) + +lemma tr_compose_id_sn (f): + f ≗ 𝐢∘f. +#f @nstream_eq_inv_ext #q // +qed. + +lemma tr_compose_id_dx (f): + f ≗ f∘𝐢. +#f @nstream_eq_inv_ext #q // +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma index 064873819..3d329e795 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma @@ -13,11 +13,35 @@ (**************************************************************************) include "ground/relocation/tr_uni_pap.ma". -include "ground/relocation/tr_compose_pap.ma". -include "ground/relocation/tr_pap_eq.ma". +include "ground/relocation/tr_id_compose.ma". +include "ground/relocation/tr_compose_pn.ma". +include "ground/lib/stream_hdtl_eq.ma". (* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************) +(* Constructions with tr_compose and tr_tl **********************************) + +lemma tr_tl_compose_uni_sn (n) (f): + ⇂f ≗ ⇂(𝐮❨n❩∘f). +#n @(nat_ind_succ … n) -n // +/2 width=1 by stream_tl_eq_repl/ +qed. + +(* Constructions with tr_compose and tr_tls *********************************) + +lemma tr_tl_compose_uni_dx (f) (n): + ⇂*[↑n]f ≗ ⇂(f∘𝐮❨n❩). +// qed. + +lemma tr_tls_compose_uni_dx (f) (p) (n): + ⇂*[p+n]f ≗ ⇂*[p](f∘𝐮❨n❩). +#f #p elim p -p [| #p #IH ] #n +[ nsucc_inj >nsucc_inj + /2 width=3 by stream_tl_eq_repl/ +] +qed. + (* Main constructions with tr_compose and tr_tls ****************************) theorem tr_compose_uni_dx (f) (p): diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 485443977..a4a802c68 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -31,7 +31,7 @@ table { ] [ { "total relocation" * } { [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ] - [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ] + [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" "tr_id_compose" * ] [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pap" "tr_compose_compose" * ] [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ] [ "tr_pushs ( ⫯*[?]? )" * ] -- 2.39.2