Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.

1 files changed, 114 insertions, 183 deletions

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 4f679fe2b..050b45ed9 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,16 +6,22 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Nota : this file is OBSOLETE, and left only for compatibility.
+    Please consider instead predicates [Nat.Even] and [Nat.Odd]
+    and Boolean functions [Nat.even] and [Nat.odd]. *)
+
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
     The main results about parity are proved in the module Div2. *)
 
+Require Import PeanoNat.
+
 Local Open Scope nat_scope.
 
 Implicit Types m n : nat.
 
 
-(** * Definition of [even] and [odd], and basic facts *)
+(** * Inductive definition of [even] and [odd] *)
 
 Inductive even : nat -> Prop :=
   | even_O : even 0
@@ -26,225 +32,150 @@ with odd : nat -> Prop :=
 Hint Constructors even: arith.
 Hint Constructors odd: arith.
 
-Lemma even_or_odd : forall n, even n \/ odd n.
+(** * Equivalence with predicates [Nat.Even] and [Nat.odd] *)
+
+Lemma even_equiv : forall n, even n <-> Nat.Even n.
+Proof.
+ fix 1.
+ destruct n as [|[|n]]; simpl.
+ - split; [now exists 0 | constructor].
+ - split.
+   + inversion_clear 1. inversion_clear H0.
+   + now rewrite <- Nat.even_spec.
+ - rewrite Nat.Even_succ_succ, <- even_equiv.
+   split.
+   + inversion_clear 1. now inversion_clear H0.
+   + now do 2 constructor.
+Qed.
+
+Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.
+Proof.
+ fix 1.
+ destruct n as [|[|n]]; simpl.
+ - split.
+   + inversion_clear 1.
+   + now rewrite <- Nat.odd_spec.
+ - split; [ now exists 0 | do 2 constructor ].
+ - rewrite Nat.Odd_succ_succ, <- odd_equiv.
+   split.
+   + inversion_clear 1. now inversion_clear H0.
+   + now do 2 constructor.
+Qed.
+
+(** Basic facts *)
+
+Lemma even_or_odd n : even n \/ odd n.
 Proof.
   induction n.
-    auto with arith.
-    elim IHn; auto with arith.
+  - auto with arith.
+  - elim IHn; auto with arith.
 Qed.
 
-Lemma even_odd_dec : forall n, {even n} + {odd n}.
+Lemma even_odd_dec n : {even n} + {odd n}.
 Proof.
   induction n.
-    auto with arith.
-    elim IHn; auto with arith.
+  - auto with arith.
+  - elim IHn; auto with arith.
 Defined.
 
-Lemma not_even_and_odd : forall n, even n -> odd n -> False.
+Lemma not_even_and_odd n : even n -> odd n -> False.
 Proof.
   induction n.
-    intros even_0 odd_0. inversion odd_0.
-    intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith.
+  - intros Ev Od. inversion Od.
+  - intros Ev Od. inversion Ev. inversion Od. auto with arith.
 Qed.
 
 
 (** * Facts about [even] & [odd] wrt. [plus] *)
 
-Lemma even_plus_split : forall n m,
-  (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
-with odd_plus_split : forall n m,
+Ltac parity2bool :=
+ rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec.
+
+Ltac parity_binop_spec :=
+ rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul.
+
+Ltac parity_binop :=
+ parity2bool; parity_binop_spec; unfold Nat.odd;
+ do 2 destruct Nat.even; simpl; tauto.
+
+
+Lemma even_plus_split n m :
+  even (n + m) -> even n /\ even m \/ odd n /\ odd m.
+Proof. parity_binop. Qed.
+
+Lemma odd_plus_split n m :
   odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
-Proof.
-intros. clear even_plus_split. destruct n; simpl in *.
- auto with arith.
- inversion_clear H;
-   apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
-intros. clear odd_plus_split. destruct n; simpl in *.
- auto with arith.
- inversion_clear H;
-   apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith.
-Qed.
+Proof. parity_binop. Qed.
 
-Lemma even_even_plus : forall n m, even n -> even m -> even (n + m)
-with odd_plus_l : forall n m, odd n -> even m -> odd (n + m).
-Proof.
-intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial.
-intros n m [] ?. apply odd_S, even_even_plus; trivial.
-Qed.
+Lemma even_even_plus n m : even n -> even m -> even (n + m).
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m)
-with odd_even_plus : forall n m, odd n -> odd m -> even (n + m).
-Proof.
-intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial.
-intros n m [] ?. apply even_S, odd_plus_r; trivial.
-Qed.
+Lemma odd_plus_l n m : odd n -> even m -> odd (n + m).
+Proof. parity_binop. Qed.
+
+Lemma odd_plus_r n m : even n -> odd m -> odd (n + m).
+Proof. parity_binop. Qed.
 
-Lemma even_plus_aux : forall n m,
+Lemma odd_even_plus n m : odd n -> odd m -> even (n + m).
+Proof. parity_binop. Qed.
+
+Lemma even_plus_aux n m :
     (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\
     (even (n + m) <-> even n /\ even m \/ odd n /\ odd m).
-Proof.
-split; split; auto using odd_plus_split, even_plus_split.
-intros [[]|[]]; auto using odd_plus_r, odd_plus_l.
-intros [[]|[]]; auto using even_even_plus, odd_even_plus.
-Qed.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma even_plus_even_inv_r n m : even (n + m) -> even n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma even_plus_even_inv_l n m : even (n + m) -> even m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma even_plus_odd_inv_r n m : even (n + m) -> odd n -> odd m.
+Proof. parity_binop. Qed.
 
-Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
-Proof.
-  intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
-Hint Resolve even_even_plus odd_even_plus: arith.
+Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma odd_plus_even_inv_l n m : odd (n + m) -> odd m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
+Lemma odd_plus_even_inv_r n m : odd (n + m) -> odd n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd m); auto.
-Qed.
+Lemma odd_plus_odd_inv_l n m : odd (n + m) -> even m -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
-Proof.
-  intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto.
-  intro; destruct (not_even_and_odd n); auto.
-Qed.
-Hint Resolve odd_plus_l odd_plus_r: arith.
+Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m.
+Proof. parity_binop. Qed.
 
 
 (** * Facts about [even] and [odd] wrt. [mult] *)
 
-Lemma even_mult_aux :
-  forall n m,
-    (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
-Proof.
-  intros n; elim n; simpl; auto with arith.
-  intros m; split; split; auto with arith.
-  intros H'; inversion H'.
-  intros H'; elim H'; auto.
-  intros n0 H' m; split; split; auto with arith.
-  intros H'0.
-  elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2;
-    case H'1; auto.
-  intros H'5; elim H'5; intros H'6 H'7; auto with arith.
-  split; auto with arith.
-  case (H' m).
-  intros H'8 H'9; case H'9.
-  intros H'10; case H'10; auto with arith.
-  intros H'11 H'12; case (not_even_and_odd m); auto with arith.
-  intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto.
-  case (H' m).
-  intros H'8 H'9; case H'9; auto.
-  intros H'0; elim H'0; intros H'1 H'2; clear H'0.
-  elim (even_plus_aux m (n0 * m)); auto.
-  intros H'0 H'3.
-  elim H'0.
-  intros H'4 H'5; apply H'5; auto.
-  left; split; auto with arith.
-  case (H' m).
-  intros H'6 H'7; elim H'7.
-  intros H'8 H'9; apply H'9.
-  left.
-  inversion H'1; auto.
-  intros H'0.
-  elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4.
-  intros H'1 H'2.
-  elim H'1; auto.
-  intros H; case H; auto.
-  intros H'5; elim H'5; intros H'6 H'7; auto with arith.
-  left.
-  case (H' m).
-  intros H'8; elim H'8.
-  intros H'9; elim H'9; auto with arith.
-  intros H'0; elim H'0; intros H'1.
-  case (even_or_odd m); intros H'2.
-  apply even_even_plus; auto.
-  case (H' m).
-  intros H H0; case H0; auto.
-  apply odd_even_plus; auto.
-  inversion H'1; case (H' m); auto.
-  intros H1; case H1; auto.
-  apply even_even_plus; auto.
-  case (H' m).
-  intros H H0; case H0; auto.
-Qed.
+Lemma even_mult_aux n m :
+  (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_l : forall n m, even n -> even (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); auto.
-  intros H H0; case H0; auto.
-Qed.
+Lemma even_mult_l n m : even n -> even (n * m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_r : forall n m, even m -> even (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); auto.
-  intros H H0; case H0; auto.
-Qed.
-Hint Resolve even_mult_l even_mult_r: arith.
+Lemma even_mult_r n m : even m -> even (n * m).
+Proof. parity_binop. Qed.
 
-Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m.
-Proof.
-  intros n m H' H'0.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'2.
-  intros H'3; elim H'3; auto.
-  intros H; case (not_even_and_odd n); auto.
-Qed.
+Lemma even_mult_inv_r n m : even (n * m) -> odd n -> even m.
+Proof. parity_binop. Qed.
 
-Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.
-Proof.
-  intros n m H' H'0.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'2.
-  intros H'3; elim H'3; auto.
-  intros H; case (not_even_and_odd m); auto.
-Qed.
+Lemma even_mult_inv_l n m : even (n * m) -> odd m -> even n.
+Proof. parity_binop. Qed.
 
-Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
-Proof.
-  intros n m; case (even_mult_aux n m); intros H; case H; auto.
-Qed.
-Hint Resolve even_mult_l even_mult_r odd_mult: arith.
+Lemma odd_mult n m : odd n -> odd m -> odd (n * m).
+Proof. parity_binop. Qed.
 
-Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.
-Proof.
-  intros n m H'.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'1.
-  intros H'3; elim H'3; auto.
-Qed.
+Lemma odd_mult_inv_l n m : odd (n * m) -> odd n.
+Proof. parity_binop. Qed.
 
-Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m.
-Proof.
-  intros n m H'.
-  case (even_mult_aux n m).
-  intros H'1 H'2; elim H'1.
-  intros H'3; elim H'3; auto.
-Qed.
+Lemma odd_mult_inv_r n m : odd (n * m) -> odd m.
+Proof. parity_binop. Qed.
+
+Hint Resolve
+ even_even_plus odd_even_plus odd_plus_l odd_plus_r
+ even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.