From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Arith/Arith.v          |   4 +-
 theories/Arith/Arith_base.v     |   4 +-
 theories/Arith/Between.v        |   4 +-
 theories/Arith/Bool_nat.v       |   6 +--
 theories/Arith/Compare.v        |   6 +--
 theories/Arith/Compare_dec.v    |  18 +++----
 theories/Arith/Div2.v           |   4 +-
 theories/Arith/EqNat.v          |   4 +-
 theories/Arith/Euclid.v         |  13 ++---
 theories/Arith/Even.v           |   4 +-
 theories/Arith/Factorial.v      |   8 ++-
 theories/Arith/Gt.v             |   4 +-
 theories/Arith/Le.v             |  11 ++--
 theories/Arith/Lt.v             |  11 ++--
 theories/Arith/Max.v            |  58 +++++++++++----------
 theories/Arith/Min.v            |  52 +++++++++---------
 theories/Arith/MinMax.v         | 113 ----------------------------------------
 theories/Arith/Minus.v          |   4 +-
 theories/Arith/Mult.v           |  19 +++----
 theories/Arith/NatOrderedType.v |  64 -----------------------
 theories/Arith/Peano_dec.v      |  26 +++++++--
 theories/Arith/Plus.v           |  31 +++--------
 theories/Arith/Wf_nat.v         |  23 ++------
 theories/Arith/vo.itarget       |   2 -
 24 files changed, 136 insertions(+), 357 deletions(-)
 delete mode 100644 theories/Arith/MinMax.v
 delete mode 100644 theories/Arith/NatOrderedType.v

(limited to 'theories/Arith')

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 2e9dc2de..6f3827a3 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index e9953e54..4f21dadf 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Le.
 Require Export Lt.
 Require Export Plus.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 65753e31..dd514653 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Between.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Le.
 Require Import Lt.
 
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index b3dcd8ec..f384e148 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Bool_nat.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Compare_dec.
 Require Export Peano_dec.
 Require Import Sumbool.
@@ -36,4 +34,4 @@ Definition nat_noteq_bool x y :=
   bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)).
 
 Definition zerop_bool x := bool_of_sumbool (zerop x).
-Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file
+Definition notzerop_bool x := bool_of_sumbool (notzerop x).
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 2fe5c0d9..c9e6d3cf 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Equality is decidable on [nat] *)
 
 Open Local Scope nat_scope.
@@ -52,4 +50,4 @@ Qed.
 
 Require Export Wf_nat.
 
-Require Export Min Max.
\ No newline at end of file
+Require Export Min Max.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 99c7415e..360d760a 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Le.
 Require Import Lt.
 Require Import Gt.
@@ -22,21 +20,21 @@ Proof.
   destruct n; auto with arith.
 Defined.
 
-Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}.
+Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
 Proof.
-  induction n; destruct m; auto with arith.
+  induction n in m |- *; destruct m; auto with arith.
   destruct (IHn m) as [H|H]; auto with arith.
   destruct H; auto with arith.
 Defined.
 
-Definition gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}.
+Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
 Proof.
   intros; apply lt_eq_lt_dec; assumption.
 Defined.
 
-Definition le_lt_dec : forall n m, {n <= m} + {m < n}.
+Definition le_lt_dec n m : {n <= m} + {m < n}.
 Proof.
-  induction n.
+  induction n in m |- *.
   auto with arith.
   destruct m.
   auto with arith.
@@ -200,7 +198,8 @@ Proof.
    apply -> nat_compare_lt; auto.
 Qed.
 
-Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y).
+Lemma nat_compare_spec :
+  forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y).
 Proof.
  intros.
  destruct (nat_compare x y) as [ ]_eqn; constructor.
@@ -209,7 +208,6 @@ Proof.
  apply <- nat_compare_gt; auto.
 Qed.
 
-
 (** Some projections of the above equivalences. *)
 
 Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 89620f5f..24cbc3f9 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Lt.
 Require Import Plus.
 Require Import Compare_dec.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 60575beb..94986278 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqNat.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Equality on natural numbers *)
 
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index f32e1ad4..513fd110 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -1,25 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Euclid.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Mult.
 Require Import Compare_dec.
 Require Import Wf_nat.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Implicit Types a b n q r : nat.
 
 Inductive diveucl a b : Set :=
   divex : forall q r, b > r -> a = q * b + r -> diveucl a b.
 
-
 Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n.
 Proof.
   intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
@@ -32,7 +29,7 @@ Proof.
   elim e; auto with arith.
   intros gtbn.
   apply divex with 0 n; simpl in |- *; auto with arith.
-Qed.
+Defined.
 
 Lemma quotient :
   forall n,
@@ -50,7 +47,7 @@ Proof.
   elim H1; auto with arith.
   intros gtbn.
   exists 0; exists n; simpl in |- *; auto with arith.
-Qed.
+Defined.
 
 Lemma modulo :
   forall n,
@@ -68,4 +65,4 @@ Proof.
   elim H1; auto with arith.
   intros gtbn.
   exists n; exists 0; simpl in |- *; auto with arith.
-Qed.
+Defined.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 5bab97c2..cd4dae98 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Even.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** 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. *)
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 3b434b96..146546dc 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Factorial.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Plus.
 Require Import Mult.
 Require Import Lt.
@@ -15,13 +13,13 @@ Open Local Scope nat_scope.
 
 (** Factorial *)
 
-Boxed Fixpoint fact (n:nat) : nat :=
+Fixpoint fact (n:nat) : nat :=
   match n with
     | O => 1
     | S n => S n * fact n
   end.
 
-Arguments Scope fact [nat_scope].
+Arguments fact n%nat.
 
 Lemma lt_O_fact : forall n:nat, 0 < fact n.
 Proof.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 43df01c0..32f453e5 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Gt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
 <<
 Definition gt (n m:nat) := m < n.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index b73959e7..f0ebf162 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Le.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
 <<
 Inductive le (n:nat) : nat -> Prop :=
@@ -84,8 +82,7 @@ Hint Immediate le_Sn_le: arith v62.
 
 Theorem le_S_n : forall n m, S n <= S m -> n <= m.
 Proof.
-  intros n m H; change (pred (S n) <= pred (S m)) in |- *.
-  destruct H; simpl; auto with arith.
+  exact Peano.le_S_n.
 Qed.
 Hint Immediate le_S_n: arith v62.
 
@@ -105,11 +102,9 @@ Hint Resolve le_pred_n: arith v62.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-  destruct n; simpl; auto with arith.
-  destruct m; simpl; auto with arith.
+  exact Peano.le_pred.
 Qed.
 
-
 (** * [le] is a order on [nat] *)
 (** Antisymmetry *)
 
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 004274fe..e07bba8d 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
 <<
 Definition lt (n m:nat) := S n <= m.
@@ -96,9 +94,9 @@ Proof.
 Qed.
 Hint Resolve lt_0_Sn: arith v62.
 
-Theorem lt_n_O : forall n, ~ n < 0.
-Proof le_Sn_O.
-Hint Resolve lt_n_O: arith v62.
+Theorem lt_n_0 : forall n, ~ n < 0.
+Proof le_Sn_0.
+Hint Resolve lt_n_0: arith v62.
 
 (** * Predecessor *)
 
@@ -192,4 +190,5 @@ Hint Immediate lt_0_neq: arith v62.
 Notation lt_O_Sn := lt_0_Sn (only parsing).
 Notation neq_O_lt := neq_0_lt (only parsing).
 Notation lt_O_neq := lt_0_neq (only parsing).
+Notation lt_n_O := lt_n_0 (only parsing).
 (* end hide *)
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index d1b1b269..77dfa508 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -1,44 +1,48 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
 
-(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
-
-Require Export MinMax.
+Require Import NPeano.
 
 Local Open Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation max := MinMax.max (only parsing).
-
-Definition max_0_l := max_0_l.
-Definition max_0_r := max_0_r.
-Definition succ_max_distr := succ_max_distr.
-Definition plus_max_distr_l := plus_max_distr_l.
-Definition plus_max_distr_r := plus_max_distr_r.
-Definition max_case_strong := max_case_strong.
-Definition max_spec := max_spec.
-Definition max_dec := max_dec.
-Definition max_case := max_case.
-Definition max_idempotent := max_id.
-Definition max_assoc := max_assoc.
-Definition max_comm := max_comm.
-Definition max_l := max_l.
-Definition max_r := max_r.
-Definition le_max_l := le_max_l.
-Definition le_max_r := le_max_r.
-Definition max_lub_l := max_lub_l.
-Definition max_lub_r := max_lub_r.
-Definition max_lub := max_lub.
+Notation max := Peano.max (only parsing).
+
+Definition max_0_l := Nat.max_0_l.
+Definition max_0_r := Nat.max_0_r.
+Definition succ_max_distr := Nat.succ_max_distr.
+Definition plus_max_distr_l := Nat.add_max_distr_l.
+Definition plus_max_distr_r := Nat.add_max_distr_r.
+Definition max_case_strong := Nat.max_case_strong.
+Definition max_spec := Nat.max_spec.
+Definition max_dec := Nat.max_dec.
+Definition max_case := Nat.max_case.
+Definition max_idempotent := Nat.max_id.
+Definition max_assoc := Nat.max_assoc.
+Definition max_comm := Nat.max_comm.
+Definition max_l := Nat.max_l.
+Definition max_r := Nat.max_r.
+Definition le_max_l := Nat.le_max_l.
+Definition le_max_r := Nat.le_max_r.
+Definition max_lub_l := Nat.max_lub_l.
+Definition max_lub_r := Nat.max_lub_r.
+Definition max_lub := Nat.max_lub.
 
 (* begin hide *)
 (* Compatibility *)
 Notation max_case2 := max_case (only parsing).
-Notation max_SS := succ_max_distr (only parsing).
+Notation max_SS := Nat.succ_max_distr (only parsing).
 (* end hide *)
+
+Hint Resolve
+ Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62.
+
+Hint Resolve
+ Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 0c8b5669..bcfbe0ef 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -1,44 +1,42 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Min.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *)
 
-(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
-
-Require Export MinMax.
+Require Import NPeano.
 
 Open Local Scope nat_scope.
 Implicit Types m n p : nat.
 
-Notation min := MinMax.min (only parsing).
+Notation min := Peano.min (only parsing).
 
-Definition min_0_l := min_0_l.
-Definition min_0_r := min_0_r.
-Definition succ_min_distr := succ_min_distr.
-Definition plus_min_distr_l := plus_min_distr_l.
-Definition plus_min_distr_r := plus_min_distr_r.
-Definition min_case_strong := min_case_strong.
-Definition min_spec := min_spec.
-Definition min_dec := min_dec.
-Definition min_case := min_case.
-Definition min_idempotent := min_id.
-Definition min_assoc := min_assoc.
-Definition min_comm := min_comm.
-Definition min_l := min_l.
-Definition min_r := min_r.
-Definition le_min_l := le_min_l.
-Definition le_min_r := le_min_r.
-Definition min_glb_l := min_glb_l.
-Definition min_glb_r := min_glb_r.
-Definition min_glb := min_glb.
+Definition min_0_l := Nat.min_0_l.
+Definition min_0_r := Nat.min_0_r.
+Definition succ_min_distr := Nat.succ_min_distr.
+Definition plus_min_distr_l := Nat.add_min_distr_l.
+Definition plus_min_distr_r := Nat.add_min_distr_r.
+Definition min_case_strong := Nat.min_case_strong.
+Definition min_spec := Nat.min_spec.
+Definition min_dec := Nat.min_dec.
+Definition min_case := Nat.min_case.
+Definition min_idempotent := Nat.min_id.
+Definition min_assoc := Nat.min_assoc.
+Definition min_comm := Nat.min_comm.
+Definition min_l := Nat.min_l.
+Definition min_r := Nat.min_r.
+Definition le_min_l := Nat.le_min_l.
+Definition le_min_r := Nat.le_min_r.
+Definition min_glb_l := Nat.min_glb_l.
+Definition min_glb_r := Nat.min_glb_r.
+Definition min_glb := Nat.min_glb.
 
 (* begin hide *)
 (* Compatibility *)
 Notation min_case2 := min_case (only parsing).
-Notation min_SS := succ_min_distr (only parsing).
-(* end hide *)
\ No newline at end of file
+Notation min_SS := Nat.succ_min_distr (only parsing).
+(* end hide *)
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
deleted file mode 100644
index 8a23c8f6..00000000
--- a/theories/Arith/MinMax.v
+++ /dev/null
@@ -1,113 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Orders NatOrderedType GenericMinMax.
-
-(** * Maximum and Minimum of two natural numbers *)
-
-Fixpoint max n m : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
-
-Fixpoint min n m : nat :=
-  match n, m with
-    | O, _ => 0
-    | S n', O => 0
-    | S n', S m' => S (min n' m')
-  end.
-
-(** These functions implement indeed a maximum and a minimum *)
-
-Lemma max_l : forall x y, y<=x -> max x y = x.
-Proof.
- induction x; destruct y; simpl; auto with arith.
-Qed.
-
-Lemma max_r : forall x y, x<=y -> max x y = y.
-Proof.
- induction x; destruct y; simpl; auto with arith.
-Qed.
-
-Lemma min_l : forall x y, x<=y -> min x y = x.
-Proof.
- induction x; destruct y; simpl; auto with arith.
-Qed.
-
-Lemma min_r : forall x y, y<=x -> min x y = y.
-Proof.
- induction x; destruct y; simpl; auto with arith.
-Qed.
-
-
-Module NatHasMinMax <: HasMinMax Nat_as_OT.
- Definition max := max.
- Definition min := min.
- Definition max_l := max_l.
- Definition max_r := max_r.
- Definition min_l := min_l.
- Definition min_r := min_r.
-End NatHasMinMax.
-
-(** We obtain hence all the generic properties of [max] and [min],
-    see file [GenericMinMax] or use SearchAbout. *)
-
-Module Export MMP := UsualMinMaxProperties Nat_as_OT NatHasMinMax.
-
-
-(** * Properties specific to the [nat] domain *)
-
-(** Simplifications *)
-
-Lemma max_0_l : forall n, max 0 n = n.
-Proof. reflexivity. Qed.
-
-Lemma max_0_r : forall n, max n 0 = n.
-Proof. destruct n; auto. Qed.
-
-Lemma min_0_l : forall n, min 0 n = 0.
-Proof. reflexivity. Qed.
-
-Lemma min_0_r : forall n, min n 0 = 0.
-Proof. destruct n; auto. Qed.
-
-(** Compatibilities (consequences of monotonicity) *)
-
-Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
-Proof. auto. Qed.
-
-Lemma succ_min_distr : forall n m, S (min n m) = min (S n) (S m).
-Proof. auto. Qed.
-
-Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
-Proof.
-intros. apply max_monotone. repeat red; auto with arith.
-Qed.
-
-Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
-Proof.
-intros. apply max_monotone with (f:=fun x => x + p).
-repeat red; auto with arith.
-Qed.
-
-Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m.
-Proof.
-intros. apply min_monotone. repeat red; auto with arith.
-Qed.
-
-Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p.
-Proof.
-intros. apply min_monotone with (f:=fun x => x + p).
-repeat red; auto with arith.
-Qed.
-
-Hint Resolve
- max_l max_r le_max_l le_max_r
- min_l min_r le_min_l le_min_r : arith v62.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 1b36f236..ed215f54 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Minus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
 Fixpoint minus (n m:nat) : nat :=
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 5dd61d67..479138a9 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Mult.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Export Plus.
 Require Export Minus.
 Require Export Lt.
@@ -177,19 +175,22 @@ Qed.
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
 Proof.
   induction n; intros; simpl in *.
-    rewrite <- 2! plus_n_O; assumption.
+    rewrite <- 2 plus_n_O; assumption.
     auto using plus_lt_compat.
 Qed.
 
 Hint Resolve mult_S_lt_compat_l: arith.
 
+Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m.
+Proof.
+ intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
+ now apply mult_S_lt_compat_l.
+Qed.
+
 Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
 Proof.
-  intros m n p H H0.
-  induction p.
-  elim (lt_irrefl _ H0).
-  rewrite mult_comm.
-  replace (n * S p) with (S p * n); auto with arith.
+  intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp).
+  rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l.
 Qed.
 
 Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.
diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
deleted file mode 100644
index fb4bf233..00000000
--- a/theories/Arith/NatOrderedType.v
+++ /dev/null
@@ -1,64 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Lt Peano_dec Compare_dec EqNat
- Equalities Orders OrdersTac.
-
-
-(** * DecidableType structure for Peano numbers *)
-
-Module Nat_as_UBE <: UsualBoolEq.
- Definition t := nat.
- Definition eq := @eq nat.
- Definition eqb := beq_nat.
- Definition eqb_eq := beq_nat_true_iff.
-End Nat_as_UBE.
-
-Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE.
-
-(** Note that the last module fulfills by subtyping many other
-    interfaces, such as [DecidableType] or [EqualityType]. *)
-
-
-
-(** * OrderedType structure for Peano numbers *)
-
-Module Nat_as_OT <: OrderedTypeFull.
- Include Nat_as_DT.
- Definition lt := lt.
- Definition le := le.
- Definition compare := nat_compare.
-
- Instance lt_strorder : StrictOrder lt.
- Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
-
- Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
- Proof. repeat red; intros; subst; auto. Qed.
-
- Definition le_lteq := le_lt_or_eq_iff.
- Definition compare_spec := nat_compare_spec.
-
-End Nat_as_OT.
-
-(** Note that [Nat_as_OT] can also be seen as a [UsualOrderedType]
-   and a [OrderedType] (and also as a [DecidableType]). *)
-
-
-
-(** * An [order] tactic for Peano numbers *)
-
-Module NatOrder := OTF_to_OrderTac Nat_as_OT.
-Ltac nat_order := NatOrder.order.
-
-(** Note that [nat_order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
-
-Section Test.
-Let test : forall x y : nat, x<=y -> y<=x -> x=y.
-Proof. nat_order. Qed.
-End Test.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 5cceab8b..6eb667c1 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -1,15 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 Require Import Decidable.
-
+Require Eqdep_dec.
+Require Import Le Lt.
 Open Local Scope nat_scope.
 
 Implicit Types m n x y : nat.
@@ -32,3 +31,22 @@ Hint Resolve O_or_S eq_nat_dec: arith.
 Theorem dec_eq_nat : forall n m, decidable (n = m).
   intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
 Defined.
+
+Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec.
+
+Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
+Proof.
+fix 3.
+refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
+  with le_n => _ |le_S i H => _ end).
+refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, 
+  le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
+    |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl).
+rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
+subst m. destruct (Lt.lt_irrefl j H').
+refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
+  with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
+    with |le_n => _ |le_S j H2 => fun H' => _ end H).
+destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
+f_equal. apply le_unique.
+Qed.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 12f12300..02975d8f 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -1,13 +1,11 @@
-(************************************************************************)
+ (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Plus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
 Fixpoint plus (n m:nat) : nat :=
@@ -26,17 +24,10 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p q : nat.
 
-(** * Zero is neutral *)
-
-Lemma plus_0_l : forall n, 0 + n = n.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma plus_0_r : forall n, n + 0 = n.
-Proof.
-  intro; symmetry  in |- *; apply plus_n_O.
-Qed.
+(** * Zero is neutral 
+Deprecated : Already in Init/Peano.v *)
+Notation plus_0_l := plus_O_n (only parsing).
+Definition plus_0_r n := eq_sym (plus_n_O n).
 
 (** * Commutativity *)
 
@@ -49,14 +40,8 @@ Hint Immediate plus_comm: arith v62.
 
 (** * Associativity *)
 
-Lemma plus_Snm_nSm : forall n m, S n + m = n + S m.
-Proof.
-  intros.
-  simpl in |- *.
-  rewrite (plus_comm n m).
-  rewrite (plus_comm n (S m)).
-  trivial with arith.
-Qed.
+Definition plus_Snm_nSm : forall n m, S n + m = n + S m:=
+ plus_n_Sm.
 
 Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
 Proof.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 23419531..b4468dd1 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf_nat.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Well-founded relations and natural numbers *)
 
 Require Import Lt.
@@ -260,19 +258,6 @@ Qed.
 
 Unset Implicit Arguments.
 
-(** [n]th iteration of the function [f] *)
-
-Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A :=
-  match n with
-    | O => x
-    | S n' => f (iter_nat n' A f x)
-  end.
-
-Theorem iter_nat_plus :
-  forall (n m:nat) (A:Type) (f:A -> A) (x:A),
-    iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x).
-Proof.
-  simple induction n;
-    [ simpl in |- *; auto with arith
-      | intros; simpl in |- *; apply f_equal with (f := f); apply H ].
-Qed.
+Notation iter_nat := @nat_iter (only parsing).
+Notation iter_nat_plus := @nat_iter_plus (only parsing).
+Notation iter_nat_invariant := @nat_iter_invariant (only parsing).
diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget
index c3f29d21..0b6564e1 100644
--- a/theories/Arith/vo.itarget
+++ b/theories/Arith/vo.itarget
@@ -19,5 +19,3 @@ Mult.vo
 Peano_dec.vo
 Plus.vo
 Wf_nat.vo
-NatOrderedType.vo
-MinMax.vo
-- 
cgit v1.2.3