From e5788b40c4a910069d1514b42c384f0e8b57050a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 29 Jan 2022 23:39:01 +0100
Subject: [PATCH] update in ground

+ additions to tr_compose
---
 .../lambdadelta/ground/lib/stream_hdtl_eq.ma  | 34 +++++++++++++++++++
 .../lambdadelta/ground/lib/stream_tls_eq.ma   |  5 ++-
 .../ground/relocation/tr_compose_eq.ma        | 29 ++++++++++++++++
 .../ground/relocation/tr_pap_eq.ma            |  5 ++-
 .../lambdadelta/ground/relocation/tr_pn_eq.ma | 31 +++++++++++++++++
 .../lambdadelta/ground/web/ground_src.tbl     |  6 ++--
 6 files changed, 101 insertions(+), 9 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
new file mode 100644
index 000000000..ebe087664
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
@@ -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 "ground/lib/stream_hdtl.ma".
+include "ground/lib/stream_eq.ma".
+
+(* HEAD AND TAIL FOR STREAMS ************************************************)
+
+(* Constructions with stream_eq *********************************************)
+
+lemma stream_hd_eq_repl (A):
+      stream_eq_repl A (λt1,t2. ⇃t1 = ⇃t2).
+#A * #a1 #t1 * #a2 #t2 #H
+elim (stream_eq_inv_cons_bi … H) -H
+/2 width=7 by/
+qed.
+
+lemma stream_tl_eq_repl (A):
+      stream_eq_repl A (λt1,t2. ⇂t1 ≗ ⇂t2).
+#A * #a1 #t1 * #a2 #t2 #H
+elim (stream_eq_inv_cons_bi … H) -H
+/2 width=7 by/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
index 28ae10cf0..a56c432fc 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/stream_eq.ma".
 include "ground/lib/stream_tls.ma".
+include "ground/lib/stream_hdtl_eq.ma".
 
 (* ITERATED TAIL FOR STREAMS ************************************************)
 
@@ -22,6 +22,5 @@ include "ground/lib/stream_tls.ma".
 lemma stream_tls_eq_repl (A) (n):
       stream_eq_repl A (λt1,t2. ⇂*[n] t1 ≗ ⇂*[n] t2).
 #A #n @(nat_ind_succ … n) -n //
-#n #IH * #n1 #t1 * #n2 #t2 #H
-elim (stream_eq_inv_cons_bi … H) /2 width=7 by/
+#n #IH /3 width=1 by stream_tl_eq_repl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_eq.ma
new file mode 100644
index 000000000..80b11090b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_eq.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.ma".
+include "ground/relocation/tr_pap_eq.ma".
+include "ground/lib/stream_tls_eq.ma".
+
+(* COMPOSITION FOR TOTAL RELOCATION MAPS ************************************)
+
+(* Constructions with stream_eq *********************************************)
+
+corec lemma tr_compose_eq_repl (f2) (g2):
+            f2 ≗ g2 → stream_eq_repl … (λf1,g1. f2∘f1 ≗ g2∘g1).
+#Hfg2 * #p1 #f1 * #q1 #g1 #H
+cases (stream_eq_inv_cons_bi … H) -H [|*: // ] * #Hfg1 -q1
+cases tr_compose_unfold cases tr_compose_unfold
+/5 width=1 by tr_pap_eq_repl, stream_tls_eq_repl, stream_eq_cons/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
index 0373fbd09..28a5af264 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
@@ -19,10 +19,9 @@ include "ground/relocation/tr_pap.ma".
 
 (* Main constructions with stream_eq ****************************************)
 
-(* Note: a better statement would be: tr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩) *)
 (*** apply_eq_repl *)
-theorem apply_eq_repl (i):
-        ∀f1,f2. f1 ≗ f2 → f1@❨i❩ = f2@❨i❩.
+theorem tr_pap_eq_repl (i):
+        stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
 elim (stream_eq_inv_cons_bi … H) -H [1,8: |*: // ] #Hp #Hf //
 <tr_pap_succ <tr_pap_succ /3 width=1 by eq_f2/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_eq.ma
new file mode 100644
index 000000000..278be5e27
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn_eq.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_eq.ma".
+include "ground/relocation/tr_pn.ma".
+
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
+
+(* Constructions with stream_eq *********************************************)
+
+lemma tr_push_eq_bi:
+      stream_eq_repl … (λf1,f2. ⫯f1 ≗ ⫯f2).
+/2 width=1 by stream_eq_cons/ qed.
+
+lemma tr_next_eq_repl:
+      stream_eq_repl … (λf1,f2. ↑f1 ≗ ↑f2).
+* #p1 #f1 * #p2 #f2 #H
+elim (stream_eq_inv_cons_bi … H) -H [|*: // ]
+/2 width=1 by stream_eq_cons/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 6100e278e..25a425139 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -32,10 +32,10 @@ table {
       [ { "total relocation" * } {
           [ "tr_uni ( 𝐮❨?❩ )" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
-          [ "tr_compose ( ?∘? )" "tr_compose_tls" "tr_compose_pn" "tr_compose_pap" "tr_compose_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 ( ⫯*[?]? )" * ]
-          [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
+          [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }
       ]
@@ -130,7 +130,7 @@ table {
   [ { "extensions to the library" * } {
       [ { "streams" * } {
           [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" "stream_tls_plus" * ]
-          [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" * ]
+          [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" "stream_hdtl_eq" * ]
           [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ]
           [ "stream ( ? ⨮{?} ? )" * ]
         }
-- 
2.39.2