--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
// 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.
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.
(*** 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 ******************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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-.
projects / helm.git / commitdiff