From 9709aaeb059e24359d5d8a3997ef22974bff3718 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Tue, 30 Nov 2021 17:31:19 +0100
Subject: [PATCH] update in ground

+ total relocation begins
---
 .../ground/etc/relocation/pstream.etc         |  16 ---
 .../lambdadelta/ground/relocation/tr_map.ma   |  46 +++++++
 .../lambdadelta/ground/relocation/tr_pap.ma   |  88 +++++++++++++
 .../lambdadelta/ground/relocation/tr_pat.ma   | 124 ++++++------------
 .../lambdadelta/ground/web/ground_src.tbl     |   3 +-
 5 files changed, 173 insertions(+), 104 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
index 90626a1d5..cc8863b59 100644
--- a/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
+++ b/matita/matita/contribs/lambdadelta/ground/etc/relocation/pstream.etc
@@ -54,22 +54,6 @@ lemma eq_inv_gr_next_bi: injective ? ? gr_next.
 * #p1 #f1 * #p2 #f2 <gr_next_unfold <gr_next_unfold #H destruct //
 qed-.
 
-lemma push_inv_seq_sn: ∀f,g,p. p⨮g = ⫯f → ∧∧ 𝟏 = p & g = f.
-#f #g #p <gr_push_unfold #H destruct /2 width=1 by conj/
-qed-.
-
-lemma push_inv_seq_dx: ∀f,g,p. ⫯f = p⨮g → ∧∧ 𝟏 = p & g = f.
-#f #g #p <gr_push_unfold #H destruct /2 width=1 by conj/
-qed-.
-
-lemma next_inv_seq_sn: ∀f,g,p. p⨮g = ↑f → ∃∃q. q⨮g = f & ↑q = p.
-* #q #f #g #p <gr_next_unfold #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma next_inv_seq_dx: ∀f,g,p. ↑f = p⨮g → ∃∃q. q⨮g = f & ↑q = p.
-* #q #f #g #p <gr_next_unfold #H destruct /2 width=3 by ex2_intro/
-qed-.
-
 lemma case_prop (Q:predicate gr_map):
       (∀f. Q (⫯f)) → (∀f. Q (↑f)) → ∀f. Q f.
 #Q #H1 #H2 * * //
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
index 80a67e320..b50b08175 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_map.ma
@@ -40,3 +40,49 @@ qed.
 lemma tr_inj_unfold_succ (f): ∀p. ↑𝐭❨p⨮f❩ = 𝐭❨↑p⨮f❩.
 #f #p <(stream_unfold … (𝐭❨↑p⨮f❩)) in ⊢ (???%); //
 qed.
+
+(* Basic inversions *********************************************************)
+
+(*** push_inv_seq_sn *)
+lemma eq_inv_cons_pr_push (f) (g):
+      ∀p. 𝐭❨p⨮g❩ = ⫯f → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
+#f #g *
+[ <tr_inj_unfold_unit
+  /3 width=1 by eq_inv_pr_push_bi, conj/
+| #p <tr_inj_unfold_succ #H
+  elim (eq_inv_pr_next_push … H)
+]
+qed-.
+
+(*** push_inv_seq_dx *)
+lemma eq_inv_pr_push_cons (f) (g):
+      ∀p. ⫯f = 𝐭❨p⨮g❩ → ∧∧ 𝟏 = p & 𝐭❨g❩ = f.
+#f #g *
+[ <tr_inj_unfold_unit
+  /3 width=1 by eq_inv_pr_push_bi, conj/
+| #p <tr_inj_unfold_succ #H
+  elim (eq_inv_pr_push_next … H)
+]
+qed-.
+
+(*** next_inv_seq_sn *)
+lemma eq_inv_cons_pr_next (f) (g):
+      ∀p. 𝐭❨p⨮g❩ = ↑f → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
+#f #g *
+[ <tr_inj_unfold_unit #H
+  elim (eq_inv_pr_push_next … H)
+| #p <tr_inj_unfold_succ #H
+  /3 width=3 by eq_inv_pr_next_bi, ex2_intro/
+]
+qed-.
+
+(*** next_inv_seq_dx *)
+lemma eq_inv_pr_next_cons (f) (g):
+      ∀p. ↑f = 𝐭❨p⨮g❩ → ∃∃q. 𝐭❨q⨮g❩ = f & ↑q = p.
+#f #g *
+[ <tr_inj_unfold_unit #H
+  elim (eq_inv_pr_next_push … H)
+| #p <tr_inj_unfold_succ #H
+  /3 width=3 by eq_inv_pr_next_bi, ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
new file mode 100644
index 000000000..7acf280d2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/functions/apply_2.ma".
+include "ground/relocation/tr_pat.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(*** apply *)
+rec definition tr_pap (i: pnat) on i: tr_map → pnat.
+* #p #f cases i -i
+[ @p
+| #i lapply (tr_pap i f) -tr_pap -i -f
+  #i @(i+p)
+]
+defined.
+
+interpretation
+  "functional positive application (total relocation maps)"
+  'Apply f i = (tr_pap i f).
+
+(* Constructions with pr_pat ***********************************************)
+
+(*** at_total *)
+lemma tr_pat_total: ∀i1,f. @❨i1,𝐭❨f❩❩ ≘ f@❨i1❩.
+#i1 elim i1 -i1
+[ * // | #i #IH * /3 width=1 by pr_pat_succ_sn/ ]
+qed.
+
+(* Inversions with pr_pat ***************************************************)
+
+lemma at_inv_total: ∀f,i1,i2. @❨i1, f❩ ≘ i2 → f@❨i1❩ = i2.
+/2 width=6 by fr2_nat_mono/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma apply_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
+// qed.
+
+lemma apply_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
+// qed.
+
+lemma apply_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
+elim (eq_inv_seq_aux … H) -H #Hp #Hf //
+>apply_S1 >apply_S1 /3 width=1 by eq_f2/
+qed.
+
+lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
+* #p #f * //
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+/2 width=4 by gr_pat_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
+[ @(Hf (𝟏))
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+  lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct
+  lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
+  /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
+]
+qed-.
+
+(*
+include "ground/relocation/pstream_eq.ma".
+*)
+
+(*
+include "ground/relocation/rtmap_istot.ma".
+
+lemma at_istot: ∀f. 𝐓❨f❩.
+/2 width=2 by ex_intro/ qed.
+*)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
index e977cb54a..208d9e7c0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
@@ -12,118 +12,68 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/apply_2.ma".
-include "ground/arith/pnat_plus.ma".
-include "ground/relocation/pr_pat.ma".
-include "ground/relocation/tr_map.ma".
-(*
 include "ground/arith/pnat_le_plus.ma".
-include "ground/relocation/pstream_eq.ma".
-include "ground/relocation/rtmap_istot.ma".
-*)
-(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
-
-(*** apply *)
-rec definition tr_pat (i: pnat) on i: tr_map → pnat.
-* #p #f cases i -i
-[ @p
-| #i lapply (tr_pat i f) -tr_pat -i -f
-  #i @(i+p)
-]
-defined.
+include "ground/relocation/pr_pat_lt.ma".
+include "ground/relocation/tr_map.ma".
 
-interpretation
-  "functional positive application (total relocation maps)"
-  'apply f i = (tr_pat i f).
+(* TOTAL RELOCATION MAPS ****************************************************)
 
 (* Constructions with pr_pat ***********************************************)
 
 (*** at_O1 *)
-lemma pr_pat_unit_sn: ∀i2,f. @❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
-#i2 elim i2 -i2 /2 width=5 by gr_pat_refl, gr_pat_next/
-qed.
-
-lemma at_S1: ∀p,f,i1,i2. @❨i1, f❩ ≘ i2 → @❨↑i1, p⨮f❩ ≘ i2+p.
-#p elim p -p /3 width=7 by gr_pat_push, gr_pat_next/
+lemma tr_pat_unit_sn: ∀i2,f. @❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
+#i2 elim i2 -i2 /2 width=5 by pr_pat_refl, pr_pat_next/
 qed.
 
-lemma at_total: ∀i1,f. @❨i1, f❩ ≘ f@❨i1❩.
-#i1 elim i1 -i1
-[ * // | #i #IH * /3 width=1 by at_S1/ ]
+(*** at_S1 *)
+lemma tr_pat_succ_sn: ∀p,f,i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → @❨↑i1, 𝐭❨p⨮f❩❩ ≘ i2+p.
+#p elim p -p /3 width=7 by pr_pat_push, pr_pat_next/
 qed.
 
-lemma at_istot: ∀f. 𝐓❨f❩.
-/2 width=2 by ex_intro/ qed.
-
-lemma at_plus2: ∀f,i1,i,p,q. @❨i1, p⨮f❩ ≘ i → @❨i1, (p+q)⨮f❩ ≘ i+q.
+(*** at_plus2 *)
+lemma tr_pat_plus_dx (f):
+      ∀i1,i,p,q. @❨i1, 𝐭❨p⨮f❩❩ ≘ i → @❨i1, 𝐭❨(p+q)⨮f❩❩ ≘ i+q.
 #f #i1 #i #p #q #H elim q -q
-/2 width=5 by gr_pat_next/
+/2 width=5 by pr_pat_next/
 qed.
 
-(* Inversion lemmas on at (specific) ******************************************)
+(* Inversions with pr_pat ***************************************************)
 
-lemma at_inv_O1: ∀f,p,i2. @❨𝟏, p⨮f❩ ≘ i2 → p = i2.
-#f #p elim p -p /2 width=6 by gr_pat_inv_unit_push/
-#p #IH #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
+(*** at_inv_O1 *)
+lemma tr_pat_inv_unit_sn (f):
+      ∀p,i2. @❨𝟏, 𝐭❨p⨮f❩❩ ≘ i2 → p = i2.
+#f #p elim p -p /2 width=6 by pr_pat_inv_unit_push/
+#p #IH #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
 #j2 #Hj * -i2 /3 width=1 by eq_f/
 qed-.
 
-lemma at_inv_S1: ∀f,p,j1,i2. @❨↑j1, p⨮f❩ ≘ i2 →
-                 ∃∃j2. @❨j1, f❩ ≘ j2 & j2+p = i2.
-#f #p elim p -p /2 width=5 by gr_pat_inv_succ_push/
-#p #IH #j1 #i2 #H elim (gr_pat_inv_next … H) -H [|*: // ]
+(*** at_inv_S1 *)
+lemma tr_pat_inv_succ_sn (f):
+      ∀p,j1,i2. @❨↑j1, 𝐭❨p⨮f❩❩ ≘ i2 →
+      ∃∃j2. @❨j1, 𝐭❨f❩❩ ≘ j2 & j2+p = i2.
+#f #p elim p -p /2 width=5 by pr_pat_inv_succ_push/
+#p #IH #j1 #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
 #i2 #Hi * -j2 /2 width=3 by ex2_intro/
 qed-.
 
-lemma at_inv_total: ∀f,i1,i2. @❨i1, f❩ ≘ i2 → f@❨i1❩ = i2.
-/2 width=6 by fr2_nat_mono/ qed-.
-
-(* Forward lemmas on at (specific) *******************************************)
+(* Destructions with pr_pat *************************************************)
 
-lemma at_increasing_plus: ∀f,p,i1,i2. @❨i1, p⨮f❩ ≘ i2 → i1 + p ≤ ↑i2.
+(* Note: a better conclusion would be: "i1 + ↓p ≤ i2" *)
+(*** at_increasing_plus *)
+lemma tr_pat_increasing_plus (f):
+      ∀p,i1,i2. @❨i1, 𝐭❨p⨮f❩❩ ≘ i2 → i1 + p ≤ ↑i2.
 #f #p *
-[ #i2 #H <(at_inv_O1 … H) -i2 //
-| #i1 #i2 #H elim (at_inv_S1 … H) -H
+[ #i2 #H <(tr_pat_inv_unit_sn … H) -i2 //
+| #i1 #i2 #H elim (tr_pat_inv_succ_sn … H) -H
   #j1 #Ht * -i2 <pplus_succ_sn 
-  /4 width=2 by gr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
+  /4 width=2 by pr_pat_increasing, ple_plus_bi_dx, ple_succ_bi/
 ]
 qed-.
 
-lemma at_fwd_id: ∀f,p,i. @❨i, p⨮f❩ ≘ i → 𝟏 = p.
-#f #p #i #H elim (gr_pat_des_id … H) -H
-#g #H elim (push_inv_seq_dx … H) -H //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tr_pat_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
-// qed.
-
-lemma tr_pat_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
-// qed.
-
-lemma tr_pat_eq_repl (i): gr_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
-#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
-elim (eq_inv_seq_aux … H) -H #Hp #Hf //
->tr_pat_S1 >tr_pat_S1 /3 width=1 by eq_f2/
-qed.
-
-lemma tr_pat_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
-* #p #f * //
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem tr_pat_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
-/2 width=4 by gr_pat_inj/ qed-.
-
-corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
-* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
-[ @(Hf (𝟏))
-| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
-  ltr_pat (Hf (𝟏)) >tr_pat_O1 >tr_pat_O1 #H destruct
-  ltr_pat (Hf (↑i)) >tr_pat_S1 >tr_pat_S1 #H
-  /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
-]
+(*** at_fwd_id *)
+lemma tr_pat_des_id (f):
+      ∀p,i. @❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
+#f #p #i #H lapply (pr_pat_des_id … H) -H #H
+elim (eq_inv_pr_push_cons … H) -H //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 6294abc43..a4c2883e4 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -30,7 +30,8 @@ table {
         }
       ]
       [ { "total relocation" * } {
-          [ "tr_map ( 𝐭❨?❩ )" "tr_nexts" "tr_eq" * ]
+          [ "tr_pap ( ?@❨?❩ )" * ]
+          [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" * ]
         }
       ]
       [ { "partial relocation" * } {
-- 
2.39.2