From 04f2f61dbe017ee5a60fd30ae4b6ef355b6e8be4 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 20 Dec 2021 19:08:34 +0100
Subject: [PATCH] update in ground

+ composition for total relocation maps
---
 .../ground/relocation/tr_compose.ma           | 58 +++++++++++++++++++
 .../tr_compose_etc.ma}                        | 48 ---------------
 .../ground/relocation/tr_compose_pn.ma        | 50 ++++++++++++++++
 .../tr_pn_hdtl.ma}                            | 14 +++--
 .../tr_pn_tls.ma}                             | 13 +++--
 .../lambdadelta/ground/web/ground_src.tbl     |  3 +-
 6 files changed, 127 insertions(+), 59 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
 rename matita/matita/contribs/lambdadelta/ground/{etc/relocation/pstream_after.etc => relocation/tr_compose_etc.ma} (75%)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
 rename matita/matita/contribs/lambdadelta/ground/{etc/relocation/pstream_tl.etc => relocation/tr_pn_hdtl.ma} (78%)
 rename matita/matita/contribs/lambdadelta/ground/{etc/relocation/pstream_tls.etc => relocation/tr_pn_tls.ma} (77%)

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
new file mode 100644
index 000000000..645b3b07b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lib/stream_tls.ma".
+include "ground/relocation/tr_pap.ma".
+
+(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+
+corec definition tr_compose: tr_map → tr_map → tr_map.
+#f2 * #p1 #f1
+@(stream_cons … (f2@❨p1❩))
+@(tr_compose ? f1) -tr_compose -f1
+@(⇂*[p1]f2)
+defined.
+
+interpretation
+  "composition (total relocation maps)"
+  'compose f2 f1 = (tr_compose f2 f1).
+
+(* Basic constructions ******************************************************)
+
+(*** compose_rew *)
+lemma tr_compose_unfold (f2) (f1):
+      ∀p1. f2@❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
+#f2 #f1 #p1 <(stream_unfold … (f2∘(p1⨮f1))) //
+qed.
+
+(* Basic inversions *********************************************************)
+
+(*** compose_inv_rew *)
+lemma tr_compose_inv_unfold (f2) (f1):
+      ∀f,p1,p. f2∘(p1⨮f1) = p⨮f →
+      ∧∧ f2@❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
+#f2 #f1 #f #p1 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+qed-.
+
+(*** compose_inv_S2 *)
+lemma tr_compose_inv_succ_dx (f2) (f1):
+      ∀f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
+      ∧∧ f2@❨p1❩+p2 = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p2 #p1 #p
+<tr_compose_unfold #H destruct
+>nsucc_inj <stream_tls_swap
+/2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
similarity index 75%
rename from matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc
rename to matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index 1f5bceffe..663dfc9b6 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_after.etc
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -16,54 +16,6 @@ include "ground/relocation/pstream_tls.ma".
 include "ground/relocation/pstream_istot.ma".
 include "ground/relocation/rtmap_after.ma".
 
-(* RELOCATION P-STREAM ******************************************************)
-
-corec definition compose: gr_map → gr_map → gr_map.
-#f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1
-@(â«°*[p1]f2)
-defined.
-
-interpretation "functional composition (nstream)"
-   'compose f2 f1 = (compose f2 f1).
-
-(* Basic properties on compose ***********************************************)
-
-lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1).
-#f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize //
-qed.
-
-lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
-#f2 * #p1 #f1 #f <compose_rew <compose_rew
-* -f /2 width=1 by eq_f2/
-qed.
-
-(* Basic inversion lemmas on compose ****************************************)
-
-lemma compose_inv_rew: ∀f2,f1,f,p1,p. f2∘(p1⨮f1) = p⨮f →
-                       f2@❨p1❩ = p ∧ (⫰*[p1]f2)∘f1 = f.
-#f2 #f1 #f #p1 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
-lemma compose_inv_O2: ∀f2,f1,f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
-                      p2 = p ∧ f2∘f1 = f.
-#f2 #f1 #f #p2 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
-lemma compose_inv_S2: ∀f2,f1,f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
-                      f2@❨p1❩+p2 = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
-#f2 #f1 #f #p2 #p1 #p <compose_rew
-#H destruct >nsucc_inj <stream_tls_swap
-/2 width=1 by conj/
-qed-.
-
-lemma compose_inv_S1: ∀f2,f1,f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
-                      ↑(f2@❨p1❩) = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
-#f2 #f1 #f #p1 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
 (* Properties on after (specific) *********************************************)
 
 lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
new file mode 100644
index 000000000..e6e9ae515
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_pn_tls.ma".
+include "ground/relocation/tr_pap_pn.ma".
+include "ground/relocation/tr_compose.ma".
+
+(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+
+(* Constructions with tr_push anf tr_next ***********************************)
+
+(*** compose_next *)
+lemma tr_compose_next_sn (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.
+
+(* Inversions with tr_push anf tr_next **************************************)
+
+(*** compose_inv_O2 *)
+lemma tr_compose_inv_push_dx (f2) (f1):
+      ∀f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
+      ∧∧ p2 = p & f2∘f1 = f.
+#f2 #f1 #f #p2 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+qed-.
+
+(*** compose_inv_S1 *)
+lemma tr_compose_inv_next_sn (f2) (f1):
+      ∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
+      ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p1 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_hdtl.ma
similarity index 78%
rename from matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc
rename to matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_hdtl.ma
index 9fa3b818e..e4bb4e583 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tl.etc
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_hdtl.ma
@@ -13,14 +13,18 @@
 (**************************************************************************)
 
 include "ground/lib/stream_hdtl.ma".
-include "ground/relocation/pstream.ma".
+include "ground/relocation/tr_pn.ma".
 
-(* RELOCATION P-STREAM ******************************************************)
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
 
-(* Properties with stream_tl *************************************************)
+(* Constructions with stream_tl *********************************************)
 
-lemma tl_push: ∀f. f = ⫰⫯f.
+(*** tl_push *)
+lemma tr_tl_push (f):
+      f = ⇂⫯f.
 // qed.
 
-lemma tl_next: ∀f. ⫰f = ⫰↑f.
+(*** tl_next *)
+lemma tr_tl_next (f):
+      ⇂f = ⇂↑f.
 * // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_tls.ma
similarity index 77%
rename from matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc
rename to matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_tls.ma
index d6837045f..58d7d7cad 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream_tls.etc
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_tls.ma
@@ -14,12 +14,15 @@
 
 include "ground/lib/stream_tls.ma".
 include "ground/arith/nat_pred_succ.ma".
-include "ground/relocation/pstream_tl.ma".
+include "ground/relocation/tr_pn_hdtl.ma".
 
-(* RELOCATION P-STREAM ******************************************************)
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
 
-(* Properties with stream_tls ************************************************)
+(* Constructions with stream_tls ********************************************)
 
-lemma tls_next: ∀f. ∀p:pnat. ⫰*[p]f = ⫰*[p]↑f.
-#f #p >(npsucc_pred p) <stream_tls_swap <stream_tls_swap //
+(*** tls_next *)
+lemma tr_tls_next (f):
+      ∀p:pnat. ⇂*[p]f = ⇂*[p]↑f.
+#f #p
+>(npsucc_pred p) <stream_tls_swap <stream_tls_swap //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 6253faa4c..a903cf088 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -30,8 +30,9 @@ table {
         }
       ]
       [ { "total relocation" * } {
+          [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
           [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
-          [ "tr_pn ( ⫯? ) ( ↑? )" * ]
+          [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }
       ]
-- 
2.39.2