Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 96 insertions, 196 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 84836268..ab749bd1 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -6,101 +6,47 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: NSigNAxioms.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
 
-Require Import ZArith.
-Require Import Nnat.
-Require Import NAxioms.
-Require Import NSig.
+Require Import ZArith Nnat NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
-Module NSig_NAxioms (N:NType) <: NAxiomsSig.
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with N.t.
-Open Local Scope IntScope.
-Notation "[ x ]" := (N.to_Z x) : IntScope.
-Infix "=="  := N.eq (at level 70) : IntScope.
-Notation "0" := N.zero : IntScope.
-Infix "+" := N.add : IntScope.
-Infix "-" := N.sub : IntScope.
-Infix "*" := N.mul : IntScope.
-
-Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
-Module Export NZAxiomsMod <: NZAxiomsSig.
-
-Definition NZ := N.t.
-Definition NZeq := N.eq.
-Definition NZ0 := N.zero.
-Definition NZsucc := N.succ.
-Definition NZpred := N.pred.
-Definition NZadd := N.add.
-Definition NZsub := N.sub.
-Definition NZmul := N.mul.
-
-Theorem NZeq_equiv : equiv N.t N.eq.
-Proof.
-repeat split; repeat red; intros; auto; congruence.
-Qed.
+Module NTypeIsNAxioms (Import N : NType').
 
-Add Relation N.t N.eq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
- as NZeq_rel.
+Hint Rewrite
+ spec_0 spec_succ spec_add spec_mul spec_pred spec_sub
+ spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
+ spec_max spec_min spec_power_pos spec_power
+ : nsimpl.
+Ltac nsimpl := autorewrite with nsimpl.
+Ltac ncongruence := unfold eq; repeat red; intros; nsimpl; congruence.
+Ltac zify := unfold eq, lt, le in *; nsimpl.
 
-Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
-Proof.
-unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto.
-Qed.
+Local Obligation Tactic := ncongruence.
 
-Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
-Proof.
-unfold N.eq; intros.
-generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
-destruct N.eq_bool; rewrite N.spec_0; intros.
-rewrite 2 N.spec_pred0; congruence.
-rewrite 2 N.spec_pred; f_equal; auto; try omega.
-Qed.
+Instance eq_equiv : Equivalence eq.
+Proof. unfold eq. firstorder. Qed.
 
-Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
-Proof.
-unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
-Qed.
+Program Instance succ_wd : Proper (eq==>eq) succ.
+Program Instance pred_wd : Proper (eq==>eq) pred.
+Program Instance add_wd : Proper (eq==>eq==>eq) add.
+Program Instance sub_wd : Proper (eq==>eq==>eq) sub.
+Program Instance mul_wd : Proper (eq==>eq==>eq) mul.
 
-Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
+Theorem pred_succ : forall n, pred (succ n) == n.
 Proof.
-unfold N.eq; intros x x' Hx y y' Hy.
-destruct (Z_lt_le_dec [x] [y]).
-rewrite 2 N.spec_sub0; f_equal; congruence.
-rewrite 2 N.spec_sub; f_equal; congruence.
+intros. zify. generalize (spec_pos n); omega with *.
 Qed.
 
-Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
-Proof.
-unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
-Qed.
-
-Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
-Proof.
-unfold N.eq; intros.
-rewrite N.spec_pred; rewrite N.spec_succ.
-omega.
-generalize (N.spec_pos n); omega.
-Qed.
-
-Definition N_of_Z z := N.of_N (Zabs_N z).
+Definition N_of_Z z := of_N (Zabs_N z).
 
 Section Induction.
 
 Variable A : N.t -> Prop.
-Hypothesis A_wd : predicate_wd N.eq A.
+Hypothesis A_wd : Proper (eq==>iff) A.
 Hypothesis A0 : A 0.
-Hypothesis AS : forall n, A n <-> A (N.succ n). 
-
-Add Morphism A with signature N.eq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
+Hypothesis AS : forall n, A n <-> A (succ n).
 
 Let B (z : Z) := A (N_of_Z z).
 
@@ -108,17 +54,17 @@ Lemma B0 : B 0.
 Proof.
 unfold B, N_of_Z; simpl.
 rewrite <- (A_wd 0); auto.
-red; rewrite N.spec_0, N.spec_of_N; auto.
+red; rewrite spec_0, spec_of_N; auto.
 Qed.
 
 Lemma BS : forall z : Z, (0 <= z)%Z -> B z -> B (z + 1).
 Proof.
 intros z H1 H2.
 unfold B in *. apply -> AS in H2.
-setoid_replace (N_of_Z (z + 1)) with (N.succ (N_of_Z z)); auto.
-unfold N.eq. rewrite N.spec_succ.
+setoid_replace (N_of_Z (z + 1)) with (succ (N_of_Z z)); auto.
+unfold eq. rewrite spec_succ.
 unfold N_of_Z.
-rewrite 2 N.spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith.
+rewrite 2 spec_of_N, 2 Z_of_N_abs, 2 Zabs_eq; auto with zarith.
 Qed.
 
 Lemma B_holds : forall z : Z, (0 <= z)%Z -> B z.
@@ -126,193 +72,144 @@ Proof.
 exact (natlike_ind B B0 BS).
 Qed.
 
-Theorem NZinduction : forall n, A n.
+Theorem bi_induction : forall n, A n.
 Proof.
-intro n. setoid_replace n with (N_of_Z (N.to_Z n)).
-apply B_holds. apply N.spec_pos.
+intro n. setoid_replace n with (N_of_Z (to_Z n)).
+apply B_holds. apply spec_pos.
 red; unfold N_of_Z.
-rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
-apply N.spec_pos.
+rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+apply spec_pos.
 Qed.
 
 End Induction.
 
-Theorem NZadd_0_l : forall n, 0 + n == n.
+Theorem add_0_l : forall n, 0 + n == n.
 Proof.
-intros; red; rewrite N.spec_add, N.spec_0; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem NZadd_succ_l : forall n m, (N.succ n) + m == N.succ (n + m).
+Theorem add_succ_l : forall n m, (succ n) + m == succ (n + m).
 Proof.
-intros; red; rewrite N.spec_add, 2 N.spec_succ, N.spec_add; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem NZsub_0_r : forall n, n - 0 == n.
+Theorem sub_0_r : forall n, n - 0 == n.
 Proof.
-intros; red; rewrite N.spec_sub; rewrite N.spec_0; auto with zarith.
-apply N.spec_pos.
+intros. zify. generalize (spec_pos n); omega with *.
 Qed.
 
-Theorem NZsub_succ_r : forall n m, n - (N.succ m) == N.pred (n - m).
+Theorem sub_succ_r : forall n m, n - (succ m) == pred (n - m).
 Proof.
-intros; red.
-destruct (Z_lt_le_dec [n] [N.succ m]) as [H|H].
-rewrite N.spec_sub0; auto.
-rewrite N.spec_succ in H.
-rewrite N.spec_pred0; auto.
-destruct (Z_eq_dec [n] [m]).
-rewrite N.spec_sub; auto with zarith.
-rewrite N.spec_sub0; auto with zarith.
-
-rewrite N.spec_sub, N.spec_succ in *; auto.
-rewrite N.spec_pred, N.spec_sub; auto with zarith.
-rewrite N.spec_sub; auto with zarith.
+intros. zify. omega with *.
 Qed.
 
-Theorem NZmul_0_l : forall n, 0 * n == 0.
+Theorem mul_0_l : forall n, 0 * n == 0.
 Proof.
-intros; red.
-rewrite N.spec_mul, N.spec_0; auto with zarith.
+intros. zify. auto with zarith.
 Qed.
 
-Theorem NZmul_succ_l : forall n m, (N.succ n) * m == n * m + m.
+Theorem mul_succ_l : forall n m, (succ n) * m == n * m + m.
 Proof.
-intros; red.
-rewrite N.spec_add, 2 N.spec_mul, N.spec_succ; ring.
+intros. zify. ring.
 Qed.
 
-End NZAxiomsMod.
-
-Definition NZlt := N.lt.
-Definition NZle := N.le.
-Definition NZmin := N.min.
-Definition NZmax := N.max.
+(** Order *)
 
-Infix "<=" := N.le : IntScope.
-Infix "<" := N.lt : IntScope.
-
-Lemma spec_compare_alt : forall x y, N.compare x y = ([x] ?= [y])%Z.
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 Proof.
- intros; generalize (N.spec_compare x y).
- destruct (N.compare x y); auto.
- intros H; rewrite H; symmetry; apply Zcompare_refl.
+ intros. zify. destruct (Zcompare_spec [x] [y]); auto.
 Qed.
 
-Lemma spec_lt : forall x y, (x<y) <-> ([x]<[y])%Z.
-Proof.
- intros; unfold N.lt, Zlt; rewrite spec_compare_alt; intuition.
-Qed.
+Definition eqb := eq_bool.
 
-Lemma spec_le : forall x y, (x<=y) <-> ([x]<=[y])%Z.
+Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
 Proof.
- intros; unfold N.le, Zle; rewrite spec_compare_alt; intuition.
+ intros. zify. symmetry. apply Zeq_is_eq_bool.
 Qed.
 
-Lemma spec_min : forall x y, [N.min x y] = Zmin [x] [y].
+Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare.
 Proof.
- intros; unfold N.min, Zmin.
- rewrite spec_compare_alt; destruct Zcompare; auto.
+intros x x' Hx y y' Hy. rewrite 2 spec_compare, Hx, Hy; intuition.
 Qed.
 
-Lemma spec_max : forall x y, [N.max x y] = Zmax [x] [y].
+Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
 Proof.
- intros; unfold N.max, Zmax.
- rewrite spec_compare_alt; destruct Zcompare; auto.
-Qed.
-
-Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
-Proof. 
-intros x x' Hx y y' Hy.
-rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
+intros x x' Hx y y' Hy; unfold lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
+Theorem lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
 Proof.
-intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition.
+intros. zify. omega.
 Qed.
 
-Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
+Theorem lt_irrefl : forall n, ~ n < n.
 Proof.
-intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition.
+intros. zify. omega.
 Qed.
 
-Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
+Theorem lt_succ_r : forall n m, n < (succ m) <-> n <= m.
 Proof.
-intros; red; rewrite 2 spec_min; congruence.
+intros. zify. omega.
 Qed.
 
-Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
+Theorem min_l : forall n m, n <= m -> min n m == n.
 Proof.
-intros; red; rewrite 2 spec_max; congruence.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+Theorem min_r : forall n m, m <= n -> min n m == m.
 Proof.
-intros.
-unfold N.eq; rewrite spec_lt, spec_le; omega.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem NZlt_irrefl : forall n, ~ n < n.
+Theorem max_l : forall n m, m <= n -> max n m == n.
 Proof.
-intros; rewrite spec_lt; auto with zarith.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem NZlt_succ_r : forall n m, n < (N.succ m) <-> n <= m.
+Theorem max_r : forall n m, n <= m -> max n m == m.
 Proof.
-intros; rewrite spec_lt, spec_le, N.spec_succ; omega.
+intros n m. zify. omega with *.
 Qed.
 
-Theorem NZmin_l : forall n m, n <= m -> N.min n m == n.
-Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
-Qed.
+(** Properties specific to natural numbers, not integers. *)
 
-Theorem NZmin_r : forall n m, m <= n -> N.min n m == m.
+Theorem pred_0 : pred 0 == 0.
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_min.
-generalize (Zmin_spec [n] [m]); omega.
+zify. auto.
 Qed.
 
-Theorem NZmax_l : forall n m, m <= n -> N.max n m == n.
-Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
-Qed.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
-Theorem NZmax_r : forall n m, n <= m -> N.max n m == m.
+Theorem div_mod : forall a b, ~b==0 -> a == b*(div a b) + (modulo a b).
 Proof.
-intros n m; unfold N.eq; rewrite spec_le, spec_max.
-generalize (Zmax_spec [n] [m]); omega.
+intros a b. zify. intros. apply Z_div_mod_eq_full; auto.
 Qed.
 
-End NZOrdAxiomsMod.
-
-Theorem pred_0 : N.pred 0 == 0.
+Theorem mod_upper_bound : forall a b, ~b==0 -> modulo a b < b.
 Proof.
-red; rewrite N.spec_pred0; rewrite N.spec_0; auto.
+intros a b. zify. intros.
+destruct (Z_mod_lt [a] [b]); auto.
+generalize (spec_pos b); auto with zarith.
 Qed.
 
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
   Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
 Implicit Arguments recursion [A].
 
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
-      forall x x' : N.t, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-unfold fun2_wd, N.eq, fun2_eq.
-intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
+unfold eq.
+intros a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
 rewrite <- Exx'; clear x' Exx'.
 replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
 induction (Zabs_nat [x]).
 simpl; auto.
-rewrite N_of_S, 2 Nrect_step; auto.
+rewrite N_of_S, 2 Nrect_step; auto. apply Eff'; auto.
 destruct [x]; simpl; auto.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
@@ -326,11 +223,11 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
-    Aeq a a -> fun2_wd N.eq Aeq Aeq f ->
-      forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
+      forall n, Aeq (recursion a f (succ n)) (f n (recursion a f n)).
 Proof.
-unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
-replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)).
+unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n.
+replace (N.to_N (succ n)) with (Nsucc (N.to_N n)).
 rewrite Nrect_step.
 apply f_wd; auto.
 unfold N.to_N.
@@ -340,7 +237,6 @@ rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto.
 fold (recursion a f n).
 apply recursion_wd; auto.
 red; auto.
-red; auto.
 unfold N.to_N.
 
 rewrite N.spec_succ.
@@ -349,8 +245,12 @@ apply Z_of_N_eq_rev.
 rewrite Z_of_N_succ.
 rewrite 2 Z_of_N_abs.
 rewrite 2 Zabs_eq; auto.
-generalize (N.spec_pos n); auto with zarith.
-apply N.spec_pos; auto.
+generalize (spec_pos n); auto with zarith.
+apply spec_pos; auto.
 Qed.
 
-End NSig_NAxioms.
+End NTypeIsNAxioms.
+
+Module NType_NAxioms (N : NType)
+ <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ := N <+ NTypeIsNAxioms.