From: Ferruccio Guidi Date: Fri, 28 Jan 2022 22:24:01 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~99 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=01b17de504f0049c15eadcdad651a19adaa954f7 update in ground + additions to tr_compose --- diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma new file mode 100644 index 000000000..314a1fd17 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma @@ -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 "ground/arith/pnat_plus.ma". +include "ground/arith/nat_rplus.ma". + +(* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************) + +(* Constructions with pplus *************************************************) + +lemma nrplus_inj_dx (p) (q): + p + q = p + ninj q. +// qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_plus.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_plus.ma new file mode 100644 index 000000000..7219f8498 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_plus.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat_plus.ma". +include "ground/lib/stream_tls.ma". + +(* ITERATED TAIL FOR STREAMS ************************************************) + +(* Constructions with nplus *************************************************) + +lemma stream_tls_plus (A) (n1) (n2) (t): + ⇂*[n1]⇂*[n2]t = ⇂*{A}[n1+n2]t. +#A #n1 #n2 #t +nsucc_inj gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold - /3 width=5 by gr_after_next/ +| #p2 >tr_next_unfold #H cases (tr_compose_inv_next_sn … H) -H * -p + /3 width=5 by pr_after_next/ ] qed-. -theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1. -/2 width=1 by after_total_aux/ qed. +(*** after_total *) +theorem tr_after_total: + ∀f1,f2. 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f2 ∘ f1❩. +/2 width=1 by tr_after_total_aux/ qed. (* Inversion lemmas on after (specific) ***************************************) @@ -112,7 +131,3 @@ lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f → (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f. /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-. -(* Properties on apply ******************************************************) - -lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. -/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma new file mode 100644 index 000000000..97ffc0d30 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.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_compose.ma". +include "ground/relocation/tr_pap_tls.ma". + +(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************) + +(* Constructions with tr_pap ************************************************) + +(*** compose_apply *) +lemma tr_compose_pap (i) (f1) (f2): + f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩. +#i elim i -i +[ * #p1 #f1 #f2 + nsucc_inj // +qed. + +(* Note: to be removed *) (*** compose_next *) -lemma tr_compose_next_sn (f2) (f1): - ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f. +fact tr_compose_next_sn_aux (f2) (f1): + ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f. #f2 * #p1 #f1 #f nsucc_inj nrplus_inj_dx >nrplus_inj_sn + nsucc_inj // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 05ba00fe4..6100e278e 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -32,8 +32,8 @@ table { [ { "total relocation" * } { [ "tr_uni ( 𝐮❨?❩ )" * ] [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ] - [ "tr_compose ( ?∘? )" "tr_compose_pn" * ] - [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ] + [ "tr_compose ( ?∘? )" "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 ( ⫯*[?]? )" * ] [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ] [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ] @@ -110,7 +110,7 @@ table { [ "nat_max ( ?∨? )" * ] [ "nat_minus ( ?-? )" "nat_minus_plus" * ] [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ] - [ "nat_rplus ( ?+? )" "nat_rplus_succ" * ] + [ "nat_rplus ( ?+? )" "nat_rplus_pplus" "nat_rplus_succ" * ] [ "nat_pred ( ↓? )" "nat_pred_succ" * ] [ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ] [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri" ] @@ -129,7 +129,7 @@ table { class "yellow" [ { "extensions to the library" * } { [ { "streams" * } { - [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" * ] + [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" "stream_tls_plus" * ] [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" * ] [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ] [ "stream ( ? ⨮{?} ? )" * ]