1 files changed, 156 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
new file mode 100644
index 00000000..f58b87d8
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -0,0 +1,156 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i $Id: NAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+
+Require Export NBase.
+
+Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
+
+Open Local Scope NatScope.
+
+Theorem add_wd :
+  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
+Proof NZadd_wd.
+
+Theorem add_0_l : forall n : N, 0 + n == n.
+Proof NZadd_0_l.
+
+Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m).
+Proof NZadd_succ_l.
+
+(** Theorems that are valid for both natural numbers and integers *)
+
+Theorem add_0_r : forall n : N, n + 0 == n.
+Proof NZadd_0_r.
+
+Theorem add_succ_r : forall n m : N, n + S m == S (n + m).
+Proof NZadd_succ_r.
+
+Theorem add_comm : forall n m : N, n + m == m + n.
+Proof NZadd_comm.
+
+Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
+Proof NZadd_assoc.
+
+Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
+Proof NZadd_shuffle1.
+
+Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
+Proof NZadd_shuffle2.
+
+Theorem add_1_l : forall n : N, 1 + n == S n.
+Proof NZadd_1_l.
+
+Theorem add_1_r : forall n : N, n + 1 == S n.
+Proof NZadd_1_r.
+
+Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
+Proof NZadd_cancel_l.
+
+Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
+Proof NZadd_cancel_r.
+
+(* Theorems that are valid for natural numbers but cannot be proved for Z *)
+
+Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
+Proof.
+intros n m; induct n.
+(* The next command does not work with the axiom add_0_l from NAddSig *)
+rewrite add_0_l. intuition reflexivity.
+intros n IH. rewrite add_succ_l.
+setoid_replace (S (n + m) == 0) with False using relation iff by
+ (apply -> neg_false; apply neq_succ_0).
+setoid_replace (S n == 0) with False using relation iff by
+ (apply -> neg_false; apply neq_succ_0). tauto.
+Qed.
+
+Theorem eq_add_succ :
+  forall n m : N, (exists p : N, n + m == S p) <->
+                    (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
+Proof.
+intros n m; cases n.
+split; intro H.
+destruct H as [p H]. rewrite add_0_l in H; right; now exists p.
+destruct H as [[n' H] | [m' H]].
+symmetry in H; false_hyp H neq_succ_0.
+exists m'; now rewrite add_0_l.
+intro n; split; intro H.
+left; now exists n.
+exists (n + m); now rewrite add_succ_l.
+Qed.
+
+Theorem eq_add_1 : forall n m : N,
+  n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
+Proof.
+intros n m H.
+assert (H1 : exists p : N, n + m == S p) by now exists 0.
+apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
+left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
+apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
+right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
+apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
+Qed.
+
+Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
+Proof.
+intro n; induct m.
+apply neq_symm. apply neq_succ_0.
+intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
+unfold not in IH; now apply IH.
+Qed.
+
+Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
+Proof.
+intros n m; cases n.
+intro H; now elim H.
+intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ.
+Qed.
+
+Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
+Proof.
+intros n m H; rewrite (add_comm n (P m));
+rewrite (add_comm n m); now apply add_pred_l.
+Qed.
+
+(* One could define n <= m as exists p : N, p + n == m. Then we have
+dichotomy:
+
+forall n m : N, n <= m \/ m <= n,
+
+i.e.,
+
+forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n)     (1)
+
+We will need (1) in the proof of induction principle for integers
+constructed as pairs of natural numbers. The formula (1) can be proved
+using properties of order and truncated subtraction. Thus, p would be
+m - n or n - m and (1) would hold by theorem sub_add from Sub.v
+depending on whether n <= m or m <= n. However, in proving induction
+for integers constructed from natural numbers we do not need to
+require implementations of order and sub; it is enough to prove (1)
+here. *)
+
+Theorem add_dichotomy :
+  forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n).
+Proof.
+intros n m; induct n.
+left; exists m; apply add_0_r.
+intros n IH.
+destruct IH as [[p H] | [p H]].
+destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
+rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l.
+left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
+right; exists (S p). rewrite add_succ_l; now rewrite H.
+Qed.
+
+End NAddPropFunct.
+