From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 20 Jan 2023 18:17:38 +0000 (+0100)
Subject: update from master branch
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=70e25b49cc5bc42e7eac421d0c74b00e4fb09b74

update from master branch
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma
new file mode 100644
index 000000000..4232017c7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_minus.ma".
+include "ground/arith/nat_minus.ma".
+include "ground/relocation/tr_map.ma".
+
+(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
+
+corec definition tr_minus: nat → tr_map → tr_map.
+* [ #f @f ] #q * #p #f
+@((p-q)⨮(tr_minus (ninj (↑q)-ninj p) f))
+defined.
+
+interpretation
+  "right minus (total relocation maps)"
+  'minus f n = (tr_minus n f).
+
+(* Basic constructions ******************************************************)
+
+lemma tr_minus_zero_dx (f):
+      f = f - 𝟎 .
+* #f #p <(stream_unfold … ((f⨮p)-𝟎)) //
+qed.
+
+lemma tr_minus_cons_inj (f) (p) (q):
+      (p-q)⨮(f-(ninj (↑q)-ninj p)) = (p⨮f)-(ninj q).
+#f #p #q <(stream_unfold … ((p⨮f)-(ninj q))) //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma
new file mode 100644
index 000000000..46a7696be
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_eq.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/relocation/tr_minus.ma".
+include "ground/lib/stream_eq.ma".
+
+(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
+
+(* Constructions with tr_eq *************************************************)
+
+corec lemma tr_minus_eq_repl (n):
+            stream_eq_repl … (λf1,f2. f1-n ≗ f2-n).
+cases n -n
+[ #f1 #f2 #Hf -tr_minus_eq_repl //
+| #q * #p1 #f1 * #p2 #f2 #Hf
+  cases (stream_eq_inv_cons_bi … Hf) -Hf  [|*: // ] * #Hf -p2
+  cases tr_minus_cons_inj cases tr_minus_cons_inj
+  @stream_eq_cons //
+  @tr_minus_eq_repl //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
new file mode 100644
index 000000000..f27e43c65
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pap.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/relocation/tr_minus_pn.ma".
+include "ground/relocation/tr_pap_pn.ma".
+include "ground/relocation/tr_pap_lt.ma".
+include "ground/arith/nat_rplus_succ.ma".
+include "ground/arith/pnat_le.ma".
+
+(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
+
+(* Constructions with tr_pap ************************************************)
+
+lemma tr_pap_minus_le (n) (p) (f):
+      f＠⧣❨p❩ ≤ p + n →
+      p = (f-n)＠⧣❨p❩.
+#n @(nat_ind_succ … n) -n [| #n #IHn ]
+[ #p #f #H1f
+  lapply (tr_pap_increasing f p) #H2f
+  >(ple_antisym … H2f H1f) in ⊢ (??%?); -H1f -H2f //
+| #p elim p -p [| #p #IHp ]
+  #f elim (tr_map_split f) * #g #H0 destruct
+  [ //
+  |2,4:
+    <tr_pap_next <nrplus_succ_dx #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    <tr_minus_next_succ /2 width=1 by/
+  | <tr_minus_push_succ <tr_pap_push <tr_pap_push <nrplus_succ_sn #Hf
+    lapply (ple_inv_succ_bi … Hf) -Hf #Hf
+    <IHp -IHp //
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pn.ma b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pn.ma
new file mode 100644
index 000000000..0bff10907
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/relocation/tr_minus_pn.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/relocation/tr_minus.ma".
+include "ground/relocation/tr_pn.ma".
+include "ground/arith/nat_succ.ma".
+
+(* RIGHT SUBTRACTION FOR TOTAL RELOCATION MAPS ******************************)
+
+(* Constructions with tr_push ***********************************************)
+
+lemma tr_minus_push_succ (f) (n):
+      (⫯(f-↑n)) = (⫯f)-↑n.
+#f #n <tr_minus_cons_inj //
+qed.
+
+(* Constructions with tr_next ***********************************************)
+
+lemma tr_minus_next_succ (n) (f:tr_map):
+      f-n = (↑f)-↑n.
+* [| #n ] * #p #f
+<tr_minus_cons_inj //
+<tr_minus_cons_inj //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index a136174bc..114eddb1e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -24,7 +24,7 @@ lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
 // qed.
 
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >nminus_comm <nminus_assoc_comm_23 //
+#a #b #c1 #H >nminus_comm_21 <nminus_assoc_comm_23 //
 qed-.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index e4ccf83f4..6f1168272 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -70,11 +70,11 @@ lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
 qed.
 
 (*** minus_minus_comm *)
-lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
-#o #m #n @(nat_ind_succ … n) -n //
+lemma nminus_comm_21 (m) (n1) (n2): m - n1 - n2 = m - n2 - n1.
+#m #n1 #n2 @(nat_ind_succ … n2) -n2 //
 qed.
 
 (*** minus_minus_comm3 *)
-lemma nminus_comm_231 (n) (m1) (m2) (m3):
-      n-m1-m2-m3 = n-m2-m3-m1.
+lemma nminus_comm_231 (m) (n1) (n2) (n3):
+      m-n1-n2-n3 = m-n2-n3-n1.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
index e910fdaa0..97c24dbd4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
@@ -38,7 +38,7 @@ qed.
 
 (*** minus_plus_plus_l *)
 lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
-#m #n #o <nminus_plus_assoc <nminus_comm //
+#m #n #o <nminus_plus_assoc <nminus_comm_21 //
 qed.
 
 (* Helper constructions with nplus ******************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma
new file mode 100644
index 000000000..389510e67
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_minus.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_pred.ma".
+include "ground/arith/pnat_iter.ma".
+
+(* SUBTRACTION FOR NON-NEGATIVE INTEGERS ************************************)
+
+definition pminus: pnat → pnat → pnat ≝
+           λp,q. (ppred^q) p.
+
+interpretation
+  "minus (positive integers)"
+  'minus p q = (pminus p q).
+
+(* Basic constructions ******************************************************)
+
+lemma pminus_unit_dx (p): ↓p = p - 𝟏.
+// qed.
+
+lemma pminus_succ_dx (p) (q): ↓(p - q) = p - ↑q.
+#p #q @(piter_succ … ppred)
+qed.
+
+(* Advanced constructions ***************************************************)
+
+lemma pminus_pred_sn (p) (q): ↓(p - q) = ↓p - q.
+#p #q @(piter_appl … ppred)
+qed.
+
+lemma pminus_unit_sn (q): 𝟏 = 𝟏 - q.
+#q elim q -q //
+qed.
+
+lemma pminus_succ_bi (p) (q): p - q = ↑p - ↑q.
+#p #q elim q -q //
+qed.
+
+lemma pminus_succ_dx_pred_sn (p) (q): ↓p - q = p - ↑q.
+// qed-.
+
+lemma pminus_refl (p): 𝟏 = p - p.
+#p elim p -p //
+qed.
+
+lemma pminus_succ_sn_refl (p): 𝟏 = ↑p - p.
+#p elim p -p //
+qed.
+
+lemma pminus_comm_21 (p) (q1) (q2): p - q1 - q2 = p - q2 - q1.
+#p #q1 #q2 elim q2 -q2 //
+qed.
+
+lemma pminus_comm_231 (p) (q1) (q2) (q3):
+      p-q1-q2-q3 = p-q2-q3-q1.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.ma
new file mode 100644
index 000000000..32ce73d45
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_lt.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_pat.ma".
+include "ground/relocation/pr_pat_lt.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with plt ***************************************************)
+
+lemma tr_pap_increasing (f) (p):
+      p ≤ f＠⧣❨p❩.
+/2 width=2 by pr_pat_increasing/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
index 2418afd11..c38aad712 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pn.ma
@@ -47,3 +47,12 @@ lemma tr_inj_push (f): ⫯𝐭❨f❩ = 𝐭❨⫯f❩.
 lemma tr_inj_next (f): ↑𝐭❨f❩ = 𝐭❨↑f❩.
 * //
 qed.
+
+(* Basic eliminations *******************************************************)
+
+lemma tr_map_split (f:tr_map):
+      ∨∨ ∃g. ⫯g = f
+       | ∃g. ↑g = f.
+* *
+/3 width=2 by ex_intro, or_introl, or_intror/
+qed-.