From 4939d8280cb3467cd8fa648b1cea04f74d71e8b7 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 7 Dec 2022 17:46:39 +0100
Subject: [PATCH] update in ground

+ head-tail decomposition of a relocation map
+ injectivity of pnpred
---
 .../ground/arith/nat_plus_pplus.ma            | 28 +++++++++++++++
 .../lambdadelta/ground/arith/nat_pred_succ.ma |  9 +++++
 .../ground/arith/nat_rplus_pplus.ma           |  6 ++++
 .../lambdadelta/ground/lib/stream_hdtl_eq.ma  | 15 ++++++++
 .../lambdadelta/ground/relocation/nap.ma      | 34 ++++++++++++++++++-
 .../ground/relocation/tr_pap_hdtl.ma          | 25 ++++++++++++++
 .../ground/relocation/tr_pap_hdtl_eq.ma       | 26 ++++++++++++++
 .../lambdadelta/ground/relocation/xap.ma      |  9 +++--
 .../lambdadelta/ground/web/ground_src.tbl     |  4 +--
 9 files changed, 150 insertions(+), 6 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_plus_pplus.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl_eq.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_pplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_pplus.ma
new file mode 100644
index 000000000..d176fae49
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus_pplus.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_rplus_pplus.ma".
+include "ground/arith/nat_plus_rplus.ma".
+
+(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
+
+lemma nplus_inj_bi (p) (q):
+      ninj (pplus p q) = nplus (ninj p) (ninj q).
+// qed.
+
+lemma nplus_pnpred_sn (p) (q):
+      pnpred (p + q) = nplus (pnpred p) (ninj q).
+#p #q
+<pplus_comm >nplus_comm >nrplus_pnpred_dx //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index 4a6e23b01..5472d7c1b 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -43,6 +43,15 @@ lemma npred_succ (n): n = ↓↑n.
 * //
 qed.
 
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_pnpred_bi:
+      injective … pnpred.
+#p1 #p2 #Hp
+>(npsucc_pred p1) >(npsucc_pred p2)
+<Hp -Hp @refl
+qed-.
+
 (* Inversions with nsucc ****************************************************)
 
 (*** nat_split *)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma
index 661da6d71..f3ae67e31 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_rplus_pplus.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "ground/arith/pnat_plus.ma".
+include "ground/arith/nat_pred.ma".
 include "ground/arith/nat_rplus_succ.ma".
 
 (* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
@@ -23,6 +24,11 @@ lemma nrplus_inj_dx (p) (q):
       p + q = p + ninj q.
 // qed.
 
+lemma nrplus_pnpred_dx (p) (q):
+      pnpred (p+q) = nrplus p (pnpred q).
+#p * //
+qed.
+
 lemma nrplus_pplus_assoc (p,q:pnat) (n:nat):
       (p+q)+n = p+(q+n).
 #p #q #n
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
index ebe087664..f113e9988 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl_eq.ma
@@ -32,3 +32,18 @@ lemma stream_tl_eq_repl (A):
 elim (stream_eq_inv_cons_bi … H) -H
 /2 width=7 by/
 qed.
+
+lemma stream_hd_tl_eq_repl (A) (t1) (t2):
+      t1 ≗{A} t2 →
+      ∧∧ ⇃t1 = ⇃t2 & ⇂t1 ≗ ⇂t2.
+#A #t1 #t2 #H
+/3 width=1 by stream_tl_eq_repl, stream_hd_eq_repl, conj/
+qed-.
+
+(* Inversions with stram_eq *************************************************)
+
+lemma stream_eq_inv_hd_tl_bi (A) (t1) (t2):
+      ⇃t1 = ⇃t2 → ⇂t1 ≗ ⇂t2 → t1 ≗{A} t2.
+#A * #a1 #t1 * #a2 #t2
+/2 width=1 by stream_eq_cons/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
index 921863e50..6bd5d7715 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/nap.ma
@@ -1,9 +1,10 @@
 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_pap_hdtl_eq.ma".
 include "ground/notation/functions/atsection_2.ma".
 include "ground/arith/nat_lt.ma".
-include "ground/arith/nat_plus_rplus.ma".
+include "ground/arith/nat_plus_pplus.ma".
 include "ground/arith/nat_pred_succ.ma".
 
 lemma nlt_npsucc_bi (n1) (n2):
@@ -61,3 +62,34 @@ theorem tr_nap_eq_repl (i):
 <tr_nap_unfold <tr_nap_unfold
 /3 width=1 by tr_pap_eq_repl, eq_f/
 qed.
+
+lemma tr_eq_inv_nap_zero_tl_bi (f1) (f2):
+      f1＠§❨𝟎❩ = f2＠§❨𝟎❩ → ⇂f1 ≗ ⇂f2 → f1 ≗ f2.
+#f1 #f2
+<tr_nap_unfold <tr_nap_unfold #H1 #H2
+/3 width=1 by tr_eq_inv_pap_unit_tl_bi, eq_inv_pnpred_bi/
+qed-.
+
+lemma tr_nap_plus_sn (f) (m) (n):
+      (⫯⇂*[↑n]f)＠§❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
+#f #m @(nat_ind_succ … m) -m [| #m #_ ] #n
+[ <nplus_zero_sn <nplus_zero_sn //
+| <tr_nap_push <nplus_comm in ⊢ (???%);
+  <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+  <nsucc_pnpred <nrplus_inj_sn <nrplus_pnpred_dx
+  >nrplus_npsucc_sn <nrplus_inj_dx
+  <pplus_comm in ⊢ (???%); <tr_pap_plus //
+]
+qed.
+
+lemma tr_nap_plus_dx (f) (m) (n):
+      ⇂*[n]f＠§❨m❩+(⫯f)＠§❨n❩ = f＠§❨m+n❩.
+#f #m #n @(nat_ind_succ … n) -n [| #n #_ ]
+[ //
+| <tr_nap_push
+  <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+  <nsucc_pnpred <nplus_pnpred_sn
+  >nrplus_npsucc_sn <nrplus_inj_dx
+  <tr_pap_plus //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl.ma
new file mode 100644
index 000000000..f06670e6a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_hdtl.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with stream_hd *********************************************)
+
+lemma tr_pap_unit (f):
+      ⇃f = f＠⧣❨𝟏❩.
+* #p #f //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl_eq.ma
new file mode 100644
index 000000000..9fcff7858
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_hdtl_eq.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/relocation/tr_pap_hdtl.ma".
+include "ground/lib/stream_hdtl_eq.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Inversions with stream_eq and stream_tl **********************************)
+
+lemma tr_eq_inv_pap_unit_tl_bi (f1) (f2):
+      f1＠⧣❨𝟏❩ = f2＠⧣❨𝟏❩ → ⇂f1 ≗ ⇂f2 → f1 ≗ f2.
+#f1 #f2 #H1 #H2
+/2 width=1 by stream_eq_inv_hd_tl_bi/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index 0835ec53f..4c3e8fc39 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,5 +1,4 @@
 (**) (* reverse include *)
-include "ground/arith/nat_rplus_pplus.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/relocation/tr_compose_pn.ma".
 include "ground/relocation/nap.ma".
@@ -78,11 +77,15 @@ theorem tr_xap_eq_repl (i):
 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
 qed.
 
-lemma tr_nap_plus (f) (m) (n):
+lemma tr_nap_plus_dx_xap (f) (m) (n):
       ⇂*[↑n]f＠❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
-/2 width=1 by eq_inv_nsucc_bi/
+/2 width=1 by tr_nap_eq_repl/
 qed.
 
+lemma tr_nap_plus_sn_xap (f) (m) (n):
+      ⇂*[n]f＠§❨m❩+f＠❨n❩ = f＠§❨m+n❩.
+// qed.
+
 lemma tr_xap_pos (f) (n):
       n = ↑↓n → f＠❨n❩=↑↓(f＠❨n❩).
 #f #n #H0 >H0 -H0
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 80d76fbe0..81aeb39e9 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -33,7 +33,7 @@ table {
           [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_hdtl" "tr_uni_tls" "tr_uni_pap" "tr_uni_compose" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "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_pap ( ?＠⧣❨?❩ )" "tr_pap_eq" "tr_pap_hdtl" "tr_pap_hdtl_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
@@ -109,7 +109,7 @@ table {
           [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
           [ "nat_max ( ?∨? )" * ]
           [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
-          [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ]
+          [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" "nat_plus_pplus" * ]
           [ "nat_rplus ( ?+? )" "nat_rplus_pplus" "nat_rplus_succ" * ]
           [ "nat_pred ( ↓? )" "nat_pred_succ" * ]
           [ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
-- 
2.39.2