Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

13 files changed, 203 insertions, 107 deletions

diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index b076de2a..fbdf2a41 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Arith_base.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
 Require Export Le.
 Require Export Lt.
@@ -18,3 +18,5 @@ Require Export Between.
 Require Export Peano_dec.
 Require Export Compare_dec.
 Require Export Factorial.
+Require Export EqNat.
+Require Export Wf_nat.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index b431fd05..e6cb5be4 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
+(*i $Id: Compare_dec.v 10295 2007-11-06 22:46:21Z letouzey $ i*)
 
 Require Import Le.
 Require Import Lt.
@@ -170,7 +170,7 @@ Proof.
   exact (lt_irrefl n).
   intros.
   apply not_gt.
-  swap H.
+  contradict H.
   destruct (nat_compare_gt n m); auto.
 Qed.  
 
@@ -184,7 +184,7 @@ Proof.
   exact (lt_irrefl m).
   intros.
   apply not_lt.
-  swap H.
+  contradict H.
   destruct (nat_compare_lt n m); auto.
 Qed.  
 
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
deleted file mode 100644
index 1dec34e2..00000000
--- a/theories/Arith/Div.v
+++ /dev/null
@@ -1,64 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id: Div.v 9245 2006-10-17 12:53:34Z notin $ i*)
-
-(** Euclidean division *)
-
-V7only [Import nat_scope.].
-Open Local Scope nat_scope.
-
-Require Le.
-Require Euclid_def.
-Require Compare_dec.
-
-Implicit Variables Type n,a,b,q,r:nat.
-
-Fixpoint inf_dec [n:nat] : nat->bool :=
-  [m:nat] Cases n m of
-            O     _     => true
-            | (S n')  O     => false
-            | (S n') (S m') => (inf_dec n' m')
-          end.
-
-Theorem div1 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-    [b,a]Cases a of
-           O     => (O,O)
-	   | (S n) =>
-             let (q,r) = (div1 b n) in
-               if (le_gt_dec b (S r)) then ((S q),O)
-		 else (q,(S r))
-	 end}.
-  Program_all.
-  Rewrite e.
-  Replace b with (S r).
-  Simpl.
-  Elim plus_n_O; Auto with arith.
-  Apply le_antisym; Auto with arith.
-  Elim plus_n_Sm; Auto with arith.
-Qed.
-
-Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b).
-  Realizer Fix div1 {div1/2: nat->nat->diveucl :=
-    [b,a]Cases a of
-           O     => (O,O)
-	   | (S n) =>
-             let (q,r) = (div1 b n) in
-               if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} }
-		 then ((S q),O)
-		 else (q,(S r))
-	 end}.
-  Program_all.
-  Rewrite e.
-  Replace b with (S r).
-  Simpl.
-  Elim plus_n_O; Auto with arith.
-  Apply le_antisym; Auto with arith.
-  Elim plus_n_Sm; Auto with arith.
-Qed.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index c32759b2..1216a545 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div2.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Div2.v 10625 2008-03-06 11:21:01Z notin $ i*)
 
 Require Import Lt.
 Require Import Plus.
@@ -169,12 +169,12 @@ Hint Resolve even_double double_even odd_double double_odd: arith.
 Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 Proof.
   intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
 
 Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 Proof.
   intros n H. exists (div2 n). auto with arith.
-Qed.
+Defined.
 
 (** Doubling before dividing by two brings back to the initial number. *)
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 82d05e2c..a9244455 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqNat.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: EqNat.v 9966 2007-07-10 23:54:53Z letouzey $ i*)
 
 (** Equality on natural numbers *)
 
@@ -89,3 +89,13 @@ Proof.
     intros n H1 H2. discriminate H2.
     intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
 Defined.
+
+Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.
+
+Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
+Proof.
+ induction x; destruct y; simpl; auto; intros; discriminate.
+Qed.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 83c0ce17..1484666b 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Even.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Even.v 10410 2007-12-31 13:11:55Z msozeau $ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
@@ -40,7 +40,7 @@ Proof.
   induction n.
     auto with arith.
     elim IHn; auto with arith.
-Qed.
+Defined.
 
 Lemma not_even_and_odd : forall n, even n -> odd n -> False.
 Proof.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index e0222e41..95af67f8 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Max.v 9883 2007-06-07 18:44:59Z letouzey $ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
@@ -30,6 +30,13 @@ Proof.
   auto with arith.
 Qed.
 
+Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
+Proof.
+  induction m; destruct n; destruct p; trivial.
+  simpl.
+  auto using IHm.
+Qed.
+
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
   induction n; induction m; simpl in |- *; auto with arith.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index db14e74b..aa009963 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Min.v 9660 2007-02-19 11:36:30Z notin $ i*)
 
 Require Import Le.
 
@@ -25,11 +25,28 @@ Fixpoint min n m {struct n} : nat :=
 
 (** * Simplifications of [min] *)
 
+Lemma min_0_l : forall n : nat, min 0 n = 0.
+Proof.
+  trivial. 
+Qed.
+
+Lemma min_0_r : forall n : nat, min n 0 = 0.
+Proof.
+  destruct n; trivial.
+Qed.
+
 Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
 Proof.
   auto with arith.
 Qed.
 
+Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
+Proof.
+  induction m; destruct n; destruct p; trivial.
+  simpl.
+  auto using (IHm n p).
+Qed.
+
 Lemma min_comm : forall n m, min n m = min m n.
 Proof.
   induction n; induction m; simpl in |- *; auto with arith.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 2380c2de..b961886d 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Minus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Minus.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
 (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
 <<
 Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
-  | O, _ => 0
+  | O, _ => n
   | S k, O => S k
   | S k, S l => k - l
   end
@@ -51,11 +51,18 @@ Qed.
 
 (** * Diagonal *)
 
-Lemma minus_n_n : forall n, 0 = n - n.
+Lemma minus_diag : forall n, n - n = 0.
 Proof.
   induction n; simpl in |- *; auto with arith.
 Qed.
-Hint Resolve minus_n_n: arith v62.
+
+Lemma minus_diag_reverse : forall n, 0 = n - n.
+Proof.
+  auto using minus_diag.
+Qed.
+Hint Resolve minus_diag_reverse: arith v62.
+
+Notation minus_n_n := minus_diag_reverse.
 
 (** * Simplification *)
 
@@ -97,23 +104,39 @@ Hint Resolve le_plus_minus_r: arith v62.
 
 (** * Relation with order *)
 
-Theorem le_minus : forall n m, n - m <= n.
+Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
 Proof.
-  intros i h; pattern i, h in |- *; apply nat_double_ind;
-    [ auto
-      | auto
-      | intros m n H; simpl in |- *; apply le_trans with (m := m); auto ].
+  intros n m p; generalize n m; clear n m; induction p as [|p HI].
+    intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
+
+    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
+    intros q r H _. simpl. auto using HI.
+Qed.
+
+Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
+Proof.
+  intros n m p; generalize n m; clear n m; induction p as [|p HI].
+    trivial.
+
+    intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
+      intros q; destruct q; auto with arith.
+        simpl. 
+        apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
+          auto with arith.
+        
+      intros q r Hqr _. simpl. auto using HI.
+Qed.
+
+Corollary le_minus : forall n m, n - m <= n.
+Proof.
+  intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
 Qed.
 
 Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
   intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
-    auto with arith.
-  intros; absurd (0 < 0); auto with arith.
-  intros p q lepq Hp gtp.
-  elim (le_lt_or_eq 0 p); auto with arith.
-  auto with arith.
-  induction 1; elim minus_n_O; auto with arith.
+    auto using le_minus with arith.
+    intros; absurd (0 < 0); auto with arith.
 Qed.
 Hint Resolve lt_minus: arith v62.
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 2315e12c..a43579f9 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Mult.v 11015 2008-05-28 20:06:42Z herbelin $ i*)
 
 Require Export Plus.
 Require Export Minus.
@@ -104,6 +104,43 @@ Proof.
 Qed.
 Hint Resolve mult_assoc: arith v62.
 
+(** ** Inversion lemmas *)
+
+Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+Proof.
+  destruct n as [| n]. 
+    intros; left; trivial.
+
+    simpl; intros m H; right. 
+    assert (H':m = 0 /\ n * m = 0) by apply (plus_is_O _ _ H).
+    destruct H'; trivial.
+Qed.
+
+Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.
+Proof.
+  destruct n as [|n].
+    simpl; intros m H; elim (O_S _ H).
+
+    simpl; intros m H.
+    destruct (plus_is_one _ _ H) as [[Hm Hnm] | [Hm Hnm]].
+      rewrite Hm in H; simpl in H; rewrite mult_0_r in H; elim (O_S _ H).
+      rewrite Hm in Hnm; rewrite mult_1_r in Hnm; auto. 
+Qed.
+
+(** ** Multiplication and successor *)
+
+Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
+Proof.
+  intros; simpl. rewrite plus_comm. reflexivity.
+Qed.
+
+Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.
+Proof.
+  induction n as [| p H]; intro m; simpl.
+  reflexivity.
+  rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity.
+Qed.
+
 (** * Compatibility with orders *)
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
@@ -223,4 +260,4 @@ Qed.
 
 Ltac tail_simpl :=
   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
-    simpl in |- *.
\ No newline at end of file
+    simpl in |- *.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9ae80d79..cc970ae4 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano_dec.v 9941 2007-07-05 12:42:35Z letouzey $ i*)
+(*i $Id: Peano_dec.v 9698 2007-03-12 17:11:32Z letouzey $ i*)
 
 Require Import Decidable.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 74d0dc93..6d510447 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Plus.v 9750 2007-04-06 00:58:14Z letouzey $ i*)
 
 (** Properties of addition. [add] is defined in [Init/Peano.v] as:
 <<
@@ -198,16 +198,14 @@ Qed.
     tail-recursive, whereas [plus] is not. This can be useful
     when extracting programs. *)
 
-Fixpoint plus_acc q n {struct n} : nat :=
+Fixpoint tail_plus n m {struct n} : nat :=
   match n with
-    | O => q
-    | S p => plus_acc (S q) p
+    | O => m
+    | S n => tail_plus n (S m)
   end.
 
-Definition tail_plus n m := plus_acc m n.
-
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
-unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto.
+induction n as [| n IHn]; simpl in |- *; auto.
 intro m; rewrite <- IHn; simpl in |- *; auto.
 Qed.
 
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 11fcd161..6ad640eb 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*)
+(*i $Id: Wf_nat.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
 (** Well-founded relations and natural numbers *)
 
@@ -50,10 +50,12 @@ Defined.
 
 the ML-like program for [induction_ltof1] is : 
 [[
-   let induction_ltof1 F a = indrec ((f a)+1) a 
-   where rec indrec = 
-        function 0    -> (function a -> error)
-               |(S m) -> (function a -> (F a (function y -> indrec y m)));;
+let induction_ltof1 f F a =
+  let rec indrec n k =
+    match n with
+    | O -> error
+    | S m -> F k (indrec m)
+  in indrec (f a + 1) a
 ]]
 
 the ML-like program for [induction_ltof2] is : 
@@ -210,3 +212,67 @@ Lemma well_founded_inv_rel_inv_lt_rel :
   forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F).
   intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial.
 Qed.
+
+(** A constructive proof that any non empty decidable subset of
+    natural numbers has a least element *)
+
+Set Implicit Arguments.
+
+Require Import Le.
+Require Import Compare_dec.
+Require Import Decidable.
+
+Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
+  exists! x, P x /\ forall x', P x' -> R x x'.
+
+Lemma dec_inh_nat_subset_has_unique_least_element :
+  forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
+    (exists n, P n) -> has_unique_least_element le P.
+Proof.
+  intros P Pdec (n0,HPn0).
+  assert
+    (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'')
+      \/(forall n', P n' -> n<=n')).
+  induction n.
+  right.
+  intros n' Hn'.
+  apply le_O_n.
+  destruct IHn.
+  left; destruct H as (n', (Hlt', HPn')).
+  exists n'; split.
+  apply lt_S; assumption.
+  assumption.
+  destruct (Pdec n).
+  left; exists n; split.
+  apply lt_n_Sn.
+  split; assumption.
+  right.
+  intros n' Hltn'.
+  destruct (le_lt_eq_dec n n') as [Hltn|Heqn].
+  apply H; assumption.
+  assumption.
+  destruct H0.
+  rewrite Heqn; assumption.
+  destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+    repeat split;
+      assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
+Qed.
+
+Unset Implicit Arguments.
+
+(** [n]th iteration of the function [f] *)
+
+Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : 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.