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 (file)
index 0000000..314a1fd
--- /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 (file)
index 0000000..7219f84
--- /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
+<nplus_comm @(niter_plus … t)
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
index 645b3b07bcde924b1c38a36116f47b5b938e9344..bbecabe017d40e11c70bd844451751844b0b8041 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
@@ -15,7 +15,7 @@
 include "ground/lib/stream_tls.ma".
 include "ground/relocation/tr_pap.ma".
 
-(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
 
 corec definition tr_compose: tr_map → tr_map → tr_map.
 #f2 * #p1 #f1

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_compose.ma
new file mode 100644 (file)
index 0000000..cdb539d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_compose.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_pap.ma".
+include "ground/relocation/tr_compose_tls.ma".
+include "ground/relocation/tr_eq.ma".
+
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
+
+(* Main constructions *******************************************************)
+
+corec theorem tr_compose_assoc (f3) (f2) (f1):
+              (f3 ∘ f2) ∘ f1 ≗ f3 ∘ (f2 ∘ f1).
+cases f1 -f1 #p1 #f1
+cases tr_compose_unfold cases tr_compose_unfold cases tr_compose_unfold
+cases tr_compose_tls
+/2 width=1 by stream_eq_cons/
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index 4c8586c31c9deb75d53d58df8f2d66b7f62d5be8..c7f41134f666a7159cea49e7d9f37e7875c2a91e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -12,46 +12,65 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(*
 include "ground/relocation/pstream_tls.ma".
 include "ground/relocation/pstream_istot.ma".
-include "ground/relocation/rtmap_after.ma".
+*)
+include "ground/arith/pnat_plus.ma".
+include "ground/relocation/pr_after.ma".
+include "ground/relocation/tr_map.ma".
 
 (* Properties on after (specific) *********************************************)
 
-lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
-                ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
+(*** after_O2 *)
+lemma tr_after_push_dx:
+      ∀f2,f1,f. 𝐭❨f2❩ ⊚ f1 ≘ 𝐭❨f❩ →
+      ∀p. 𝐭❨p⨮f2❩ ⊚ ⫯f1 ≘ 𝐭❨p⨮f❩.
 #f2 #f1 #f #Hf #p elim p -p
-/2 width=7 by gr_after_refl, gr_after_next/
+/2 width=7 by pr_after_refl, pr_after_next/
 qed.
 
-lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
-                ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
+(*** after_S2 *) 
+lemma tr_after_next_dx:
+      ∀f2,f1,f,p1,p. 𝐭❨f2❩ ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨p⨮f❩ →
+      ∀p2. 𝐭❨p2⨮f2❩ ⊚ 𝐭❨↑p1⨮f1❩ ≘ 𝐭❨(p+p2)⨮f❩.
 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
-/2 width=7 by gr_after_next, gr_after_push/
+/2 width=7 by pr_after_next, pr_after_push/
 qed.
 
-lemma after_apply: ∀p1,f2,f1,f.
-      (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
+include "ground/lib/stream_tls.ma".
+include "ground/relocation/tr_pap.ma".
+
+(*** after_apply *)
+lemma tr_after_pap:
+      ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
+      (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@❨p1❩⨮f❩.
 #p1 elim p1 -p1
-[ * /2 width=1 by after_O2/
+[ * /2 width=1 by tr_after_push_dx/
 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
-  /3 width=1 by after_S2/
+  /3 width=1 by tr_after_next_dx/
 ]
 qed-.
 
-corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
+include "ground/relocation/tr_compose_pn.ma".
+
+(*** after_total_aux *)
+corec fact tr_after_total_aux:
+      ∀f2,f1,f. f2 ∘ f1 = f → 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩.
 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
 [ cases p1 -p1
-  [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
-  | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
+  [ #H cases (tr_compose_inv_push_dx … H) -H /3 width=7 by pr_after_refl, eq_f2/
+  | #p1 #H cases (tr_compose_inv_succ_dx … H) -H * -p /3 width=7 by pr_after_push/
   ]
-| #p2 >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 (file)
index 0000000..97ffc0d
--- /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
+  <tr_compose_unfold <tr_pap_unit <tr_pap_unit //
+| #i #IH * #p1 #f1 #f2
+  <tr_compose_unfold <tr_pap_succ <tr_pap_succ //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
index e6e9ae515b71696c83f0be08d7278ebb0485aa41..acc891d4bf1e1158c25e061ef4d8c0b1b4c01393 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
@@ -16,20 +16,38 @@ include "ground/relocation/tr_pn_tls.ma".
 include "ground/relocation/tr_pap_pn.ma".
 include "ground/relocation/tr_compose.ma".
 
-(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
 
-(* Constructions with tr_push anf tr_next ***********************************)
+(* Constructions with tr_push and tr_next ***********************************)
 
+lemma tr_compose_push_bi (f2) (f1):
+      (⫯(f2∘f1)) = (⫯f2)∘(⫯f1).
+#f2 #f1
+<tr_compose_unfold //
+qed.
+
+lemma tr_compose_push_next (f2) (f1):
+      ↑(f2∘f1) = (⫯f2)∘(↑f1).
+#f2 * #p1 #f1
+<tr_next_unfold <tr_compose_unfold <tr_compose_unfold <tr_next_unfold
+<tr_pap_push >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
 <tr_compose_unfold <tr_compose_unfold * -f
 <tr_pap_next 
 /3 width=1 by compose_repl_fwd_dx/
-qed.
+qed-.
+
+lemma tr_compose_next_sn (f2) (f1):
+      ↑(f2∘f1) = (↑f2)∘f1.
+/2 width=1 by tr_compose_next_sn_aux/ qed.
 
-(* Inversions with tr_push anf tr_next **************************************)
+(* Inversions with tr_push and tr_next **************************************)
 
 (*** compose_inv_O2 *)
 lemma tr_compose_inv_push_dx (f2) (f1):

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
new file mode 100644 (file)
index 0000000..1a7947f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/stream_tls_plus.ma".
+include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_rplus_pplus.ma".
+
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
+
+(* Advanced constructions with stream_tls ***********************************)
+
+lemma tr_compose_tls (i) (f2) (f1):
+      (⇂*[f1@❨i❩]f2)∘⇂*[i]f1 = ⇂*[i](f2∘f1).
+#i elim i -i
+[ #f2 * #p1 #f1 //
+| #i #IH #f2 * #p1 #f1
+  >nsucc_inj <stream_tls_swap <stream_tls_swap
+  <tr_pap_succ >nrplus_inj_dx >nrplus_inj_sn
+  <tr_compose_unfold <IH -IH //
+]
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
new file mode 100644 (file)
index 0000000..978d360
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_pap.ma".
+include "ground/lib/stream_tls.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with stream_tls ********************************************)
+
+lemma tr_pap_plus (i1) (i2) (f):
+      (⇂*[ninj i2]f)@❨i1❩+f@❨i2❩ = f@❨i1+i2❩.
+#i1 #i2 elim i2 -i2
+[ * #p #f //
+| #i #IH * #p #f
+  <pplus_succ_dx <tr_pap_succ <tr_pap_succ
+  <IH -IH >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 05ba00fe433c991a9ff89ecacfb7e5344d9cdb5b..6100e278ebe9b2ad37159c5651edab7f09157b54 100644 (file)
--- 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 ( ? ⨮{?} ? )" * ]