An update on axiomatization of numbers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 277 insertions, 22 deletions

diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 3b0c1c5eb..12cecca18 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -91,7 +91,21 @@ Definition le (n m : N) := lt n m || e n m.
 Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m.
 Proof.
 intros n m. rewrite E_equiv_e. unfold le.
-do 4 rewrite eq_true_unfold.
+do 3 rewrite eq_true_unfold.
+assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true).
+split; [apply orb_prop | apply orb_true_intro].
+now rewrite H.
+Qed.
+
+Theorem le_intro_left : forall n m, lt n m -> le n m.
+Proof.
+intros; rewrite le_lt; now left.
+Qed.
+
+Theorem le_intro_right : forall n m, n == m -> le n m.
+Proof.
+intros; rewrite le_lt; now right.
+Qed.
 
 Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true).
 unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_Set.
@@ -129,6 +143,11 @@ Qed.
 as error "Impossible to unify", not just, e.g., "Cannot solve second-order
 unification problem". Something is probably wrong. *)
 
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+intros x1 x2 H1 x3 x4 H2; unfold le; rewrite H1; now rewrite H2.
+Qed.
+
 Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n.
 Proof.
 intro n; unfold lt; now rewrite recursion_0.
@@ -174,8 +193,9 @@ now unfold eq_bool.
 unfold fun2_wd; intros; now apply lt_wd.
 Qed.
 
-Theorem lt_S : forall m n, lt m (S n) <-> lt m n \/ m == n.
+Theorem lt_S : forall m n, lt m (S n) <-> le m n.
 Proof.
+assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n).
 induct m.
 nondep_induct n;
 [split; intro; [now right | apply lt_0_1] |
@@ -188,8 +208,8 @@ false_hyp H lt_0. false_hyp H S_0.
 intro m. pose proof (IH m) as H; clear IH.
 assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_Sn_Sm |].
 assert (lt (S n) (S m) <-> lt n m); [apply lt_Sn_Sm |].
-assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|].
-tauto.
+assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|]. tauto.
+intros; rewrite le_lt; apply A.
 Qed.
 
 (*****************************************************)
@@ -347,18 +367,32 @@ Module NDefaultOrderModule <: NOrderSignature.
 Module NatModule := NatMod.
 
 Definition lt := lt.
+Definition le := le.
 
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Proof.
 exact lt_wd.
 Qed.
 
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+exact le_wd.
+Qed.
+
+(* This produces a warning about a morphism redeclaration. Why is not
+there a warning after declaring lt? *)
+
+Theorem le_lt : forall x y, le x y <-> lt x y \/ x == y.
+Proof.
+exact le_lt.
+Qed.
+
 Theorem lt_0 : forall x, ~ (lt x 0).
 Proof.
 exact lt_0.
 Qed.
 
-Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x == y.
+Theorem lt_S : forall x y, lt x (S y) <-> le x y.
 Proof.
 exact lt_S.
 Qed.
diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v
index c4e9a21a7..08a6d44a8 100644
--- a/theories/Numbers/Natural/Axioms/NOrder.v
+++ b/theories/Numbers/Natural/Axioms/NOrder.v
@@ -9,6 +9,8 @@ Parameter Inline le : N -> N -> bool.
 
 Notation "x < y" := (lt x y) : NatScope.
 Notation "x <= y" := (le x y) : NatScope.
+Notation "x > y" := (lt y x) (only parsing) : NatScope.
+Notation "x >= y" := (le y x) (only parsing) : NatScope.
 
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
@@ -62,7 +64,7 @@ Proof.
 induct n; [apply lt_n_Sn | intros x H; now apply lt_closed_S].
 Qed.
 
-Theorem lt_transitive : forall n m p, n < m -> m < p -> n < p.
+Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.
 Proof.
 intros n m p; induct m.
 intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption].
@@ -72,12 +74,31 @@ apply IH; [assumption | apply lt_S_lt; assumption].
 rewrite H1; apply lt_S_lt; assumption.
 Qed.
 
+Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+le_elim H2. le_intro1; now apply lt_trans with (m := m).
+le_intro1; now rewrite <- H2. now rewrite H1.
+Qed.
+
+Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H1.
+now apply lt_trans with (m := m). now rewrite H1.
+Qed.
+
+Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof.
+intros n m p H1 H2; le_elim H2.
+now apply lt_trans with (m := m). now rewrite <- H2.
+Qed.
+
 Theorem lt_positive : forall n m, n < m -> 0 < m.
 Proof.
 intros n m; induct n.
 trivial.
 intros x IH H.
-apply lt_transitive with (m := S x); [apply lt_0_Sn | apply H].
+apply lt_trans with (m := S x); [apply lt_0_Sn | apply H].
 Qed.
 
 Theorem lt_resp_S : forall n m, S n < S m <-> n < m.
@@ -90,7 +111,7 @@ induct m.
 intro H; false_hyp H lt_0.
 intros x IH H.
 apply -> lt_S in H; le_elim H.
-apply lt_transitive with (m := S x).
+apply lt_trans with (m := S x).
 apply IH; assumption.
 apply lt_n_Sn.
 rewrite H; apply lt_n_Sn.
@@ -109,7 +130,7 @@ split; intro H; [false_hyp H lt_0 |
 le_elim H; [false_hyp H lt_0 | false_hyp H S_0]].
 intros m; split; intro H.
 apply -> lt_S in H. le_elim H; [le_intro1; now apply <- lt_resp_S | le_intro2; now apply S_wd].
-le_elim H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] |
+le_elim H; [apply lt_trans with (m := S n); [apply lt_n_Sn | assumption] |
 apply S_inj in H; rewrite H; apply lt_n_Sn].
 Qed.
 
@@ -123,13 +144,20 @@ Proof.
 intros; le_intro1; now apply <- lt_le_S_l.
 Qed.
 
-Theorem lt_irreflexive : forall n, ~ (n < n).
+Theorem lt_irr : forall n, ~ (n < n).
 Proof.
 induct n.
 apply lt_0.
 intro x; unfold not; intros H1 H2; apply H1; now apply -> lt_resp_S.
 Qed.
 
+Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m.
+Proof.
+intros n m H1 H2; le_elim H1; le_elim H2.
+elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m).
+now symmetry. assumption. assumption.
+Qed.
+
 Theorem neq_0_lt : forall n, 0 # n -> 0 < n.
 Proof.
 induct n.
@@ -144,10 +172,10 @@ intro H; absurd_hyp H; [apply lt_0 | assumption].
 unfold not; intros; now apply S_0 with (n := n).
 Qed.
 
-Theorem lt_asymmetric : forall n m, ~ (n < m /\ m < n).
+Theorem lt_asymm : forall n m, ~ (n < m /\ m < n).
 Proof.
 unfold not; intros n m [H1 H2].
-now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|].
+now apply (lt_trans n m n) in H1; [false_hyp H1 lt_irr|].
 Qed.
 
 Theorem le_0_l: forall n, 0 <= n.
@@ -163,16 +191,30 @@ intros n IH. destruct IH as [H | H].
 assert (H1 : S n <= m); [now apply -> lt_le_S_l | apply -> le_lt in H1; tauto].
 destruct H as [H | H].
 right; right; rewrite H; apply lt_n_Sn.
-right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn].
+right; right; apply lt_trans with (m := n); [assumption | apply lt_n_Sn].
 Qed.
 
-Theorem lt_dichotomy : forall n m, n < m \/ ~ n < m.
+(** The law of excluded middle for < *)
+Theorem lt_em : forall n m, n < m \/ ~ n < m.
 Proof.
 intros n m; pose proof (lt_trichotomy n m) as H.
 destruct H as [H1 | H1]; [now left |].
 destruct H1 as [H2 | H2].
-right; rewrite H2; apply lt_irreflexive.
-right; intro; apply (lt_asymmetric n m); split; assumption.
+right; rewrite H2; apply lt_irr.
+right; intro; apply (lt_asymm n m); split; assumption.
+Qed.
+
+Theorem not_lt : forall n m, ~ (n < m) <-> n >= m.
+Proof.
+intros n m; split; intro H.
+destruct (lt_trichotomy n m) as [H1 | [H1 | H1]].
+false_hyp H1 H. rewrite H1; apply le_refl. now le_intro1.
+intro; now apply (le_lt_trans m n m) in H; [false_hyp H lt_irr |].
+Qed.
+
+Theorem lt_or_ge : forall n m, n < m \/ n >= m.
+Proof.
+intros n m; rewrite <- not_lt; apply lt_em.
 Qed.
 
 Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n.
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index 0ae12df97..d49794d28 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -112,6 +112,14 @@ intros n IH H. rewrite plus_Sn_m in H.
 absurd_hyp H; [|assumption]. unfold not; apply S_0.
 Qed.
 
+Theorem plus_eq_S :
+  forall n m p, n + m == S p -> (exists n', n == S n') \/ (exists m', m == S m').
+Proof.
+intros n m p; nondep_induct n.
+intro H; rewrite plus_0_l in H; right; now exists p.
+intros n _; left; now exists n.
+Qed.
+
 Theorem succ_plus_discr : forall n m, m # S (n + m).
 Proof.
 intro n; induct m.
@@ -197,4 +205,73 @@ rewrite plus_Sn_m in H. apply S_inj in H.
 apply plus_eq_0 in H; split; [apply S_wd | ]; tauto.
 Qed.
 
+(* One could define n <= m := exists p, p + n == m. Then we have
+dichotomy:
+
+forall n m, n <= m \/ m <= n,
+
+i.e.,
+
+forall n m, (exists p, p + n == m) \/ (exists p, 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 minus_plus from Minus.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 minus; it is enough to prove (1)
+here. *)
+
+Theorem plus_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
+Proof.
+intros n m; induct n.
+left; exists m; apply plus_0_r.
+intros n IH.
+(* destruct IH as [p H | p H]. does not print a goal in ProofGeneral *)
+destruct IH as [[p H] | [p H]].
+destruct (O_or_S p) as [H1 | [p' H1]]; rewrite H1 in H.
+rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_Sn_m; now rewrite plus_0_l.
+left; exists p'; rewrite plus_n_Sm; now rewrite plus_Sn_m in H.
+right; exists (S p). rewrite plus_Sn_m; now rewrite H.
+Qed.
+
+(* In proving the correctness of the definition of multiplication on
+integers constructed from pairs of natural numbers, we'll need the
+following fact about natural numbers:
+
+a * x + u == a * y + v -> x + y' == x' + y -> a * x' + u = a * y' + v  (2)
+
+Here x + y' == x' + y represents equality of integers (x, y) and
+(x', y'), since a pair of natural numbers represents their integer
+difference. On integers, the (2) could be proved by moving
+a * y to the left, factoring out a and replacing x - y by x' - y'.
+However, the whole point is that we are only in the process of
+constructing integers, so this has to be proved for natural numbers,
+where we cannot move terms from one side of an equation to the other.
+We first prove the special case of (2) where a == 1. *)
+
+Theorem plus_repl_pair : forall n m n' m' u v,
+  n + u == m + v -> n + m' == n' + m -> n' + u == m' + v.
+Proof.
+induct n.
+intros m n' m' u v H1 H2. rewrite plus_0_l in H1. rewrite plus_0_l in H2.
+rewrite H1; rewrite H2. now rewrite plus_assoc.
+intros n IH m n' m' u v H1 H2. rewrite plus_Sn_m in H1. rewrite plus_Sn_m in H2.
+assert (H : (exists m'', m == S m'') \/ ((exists v', v == S v') /\ (exists n'', n' == S n''))).
+symmetry in H1; symmetry in H2;
+destruct (plus_eq_S m v (n + u) H1); destruct (plus_eq_S n' m (n + m') H2).
+now left. now left. right; now split. now left.
+(* destruct H as [[m'' H] | [v' H3] [n'' H4]]. *)
+(* The command above produces a warning and the PG does not show a goal !!! *) 
+destruct H as [[m'' H] | [[v' H3] [n'' H4]]].
+rewrite H in H1, H2. rewrite plus_Sn_m in H1; rewrite plus_n_Sm in H2.
+apply S_inj in H1; apply S_inj in H2. now apply (IH m'').
+rewrite H3; rewrite H4; rewrite plus_Sn_m; rewrite plus_n_Sm; apply S_wd.
+rewrite H3 in H1; rewrite H4 in H2; rewrite plus_Sn_m in H2; rewrite plus_n_Sm in H1;
+apply S_inj in H1; apply S_inj in H2. now apply (IH m).
+Qed.
+
+(* The formula (2) will be proved in NTimes.v *)
+
 End NPlusProperties.
diff --git a/theories/Numbers/Natural/Axioms/NPlusOrder.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v
index fe43ff38d..d152a0368 100644
--- a/theories/Numbers/Natural/Axioms/NPlusOrder.v
+++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v
@@ -34,7 +34,7 @@ Qed.
 Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
 Proof.
 intros n m p q H1 H2.
-apply lt_transitive with (m := m + p);
+apply lt_trans with (m := m + p);
 [now apply plus_lt_compat_r | now apply plus_lt_compat_l].
 Qed.
 
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index 2dd052201..ed3498f1c 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -1,3 +1,4 @@
+Require Import Ring.
 Require Export NPlus.
 
 Module Type NTimesSignature.
@@ -160,4 +161,42 @@ apply plus_eq_0 in H; destruct H as [H1 H2];
 apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split.
 Qed.
 
+(* See the notes on the theorem plus_repl_pair in NPlus.v *)
+
+Theorem plus_mult_repl_pair : forall a n m n' m' u v,
+  a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v.
+Proof.
+induct a.
+intros; repeat rewrite times_0_n in *; now repeat rewrite plus_0_n in *.
+intros a IH n m n' m' u v H1 H2.
+repeat rewrite times_Sn_m in *.
+(*setoid_replace (n + a * n) with (a * n + n) in H1 by (apply plus_comm).
+setoid_replace (m + a * m) with (a * m + m) in H1 by (apply plus_comm).*)
+setoid_replace (n' + a * n') with (a * n' + n') by (apply plus_comm).
+setoid_replace (m' + a * m') with (a * m' + m') by (apply plus_comm).
+do 2 rewrite <- plus_assoc. apply IH with n m; [| assumption]. do 2 rewrite plus_assoc.
+setoid_replace ((a * n) + n') with (n' + a * n) by (apply plus_comm).
+setoid_replace (a * m + m') with (m' + a * m) by (apply plus_comm).
+do 2 rewrite <- plus_assoc. apply plus_repl_pair with n m; [| assumption].
+now do 2 rewrite plus_assoc.
+Qed.
+
+Theorem semi_ring : semi_ring_theory 0 (S 0) plus times E.
+Proof.
+constructor.
+exact plus_0_l.
+exact plus_comm.
+exact plus_assoc.
+exact mult_1_l.
+exact mult_0_l.
+exact mult_comm.
+exact mult_assoc.
+exact mult_plus_distr_r.
+Qed.
+
+Add Ring SR : semi_ring.
+Goal forall x y z : N, (x + y) * z == z * y + x * z.
+intros. Set Printing All. ring.
+
+
 End NTimesProperties.
diff --git a/theories/Numbers/Natural/Axioms/NTimesOrder.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v
index f6afd5999..89ddcc7d4 100644
--- a/theories/Numbers/Natural/Axioms/NTimesOrder.v
+++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v
@@ -55,7 +55,7 @@ intros n m p q; induct n.
 intros; rewrite times_0_n; apply mult_positive;
 [assumption | apply lt_positive with (n := p); assumption].
 intros x IH H1 H2.
-apply lt_transitive with (m := ((S x) * q)).
+apply lt_trans with (m := ((S x) * q)).
 now apply mult_S_lt_compat_l; assumption.
 now apply mult_lt_compat_r; [| apply lt_positive with (n := p)].
 Qed.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 9927bde0b..0e07cd260 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,3 +1,5 @@
+Require Import Minus.
+
 Require Export NDepRec.
 Require Export NTimesOrder.
 Require Export NMinus.
@@ -150,35 +152,96 @@ Qed.
 
 End NPeanoTimes.
 
-Module NPeanoLt <: NLtSignature.
+Module NPeanoOrder <: NOrderSignature.
 Module Export NatModule := PeanoNat.
 
 Definition lt := lt_bool.
+Definition le := le_bool.
 
 Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
 Proof.
 unfold E, eq_bool; congruence.
 Qed.
 
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+unfold E, eq_bool; congruence.
+Qed.
+
+Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y.
+Proof.
+exact le_lt.
+Qed.
+
 Theorem lt_0 : forall x, ~ (lt x 0).
 Proof.
 exact lt_bool_0.
 Qed.
 
-Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y.
+Theorem lt_S : forall x y, lt x (S y) <-> le x y.
 Proof.
 exact lt_bool_S.
 Qed.
 
-End NPeanoLt.
+End NPeanoOrder.
 
 Module NPeanoPred <: NPredSignature.
+Module Export NatModule := PeanoNat.
+
+Definition P (n : nat) :=
+match n with
+| 0 => 0
+| S n' => n'
+end.
+
+Add Morphism P with signature E ==> E as P_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem P_0 : P 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem P_S : forall n, P (S n) = n.
+Proof.
+now intro.
+Qed.
+
+End NPeanoPred.
+
+Module NPeanoMinus <: NMinusSignature.
+Module Export NPredModule := NPeanoPred.
+
+Definition minus := minus.
+
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+unfold E; congruence.
+Qed.
+
+Theorem minus_0_r : forall n, n - 0 = n.
+Proof.
+now destruct n.
+Qed.
+
+Theorem minus_S_r : forall n m, n - (S m) = P (n - m).
+Proof.
+induction n as [| n IH]; simpl.
+now intro.
+destruct m; simpl; [apply minus_0_r | apply IH].
+Qed.
+
+End NPeanoMinus.
 
 (* Obtaining properties for +, *, <, and their combinations *)
 
-Module Export NPeanoTimesLtProperties := NTimesLtProperties NPeanoTimes NPeanoLt.
+Module Export NPeanoTimesOrderProperties := NTimesOrderProperties NPeanoTimes NPeanoOrder.
 Module Export NPeanoDepRecTimesProperties :=
   NDepRecTimesProperties NPeanoDepRec NPeanoTimes.
+Module Export NPeanoMinusProperties :=
+  NMinusProperties NPeanoMinus NPeanoPlus NPeanoOrder.
 
 Module MiscFunctModule := MiscFunctFunctor PeanoNat.
 (* The instruction above adds about 0.5M to the size of the .vo file !!! *)