Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

21 files changed, 78 insertions, 61 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 114a60ee..59d9b2b1 100755..100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Arith.v,v 1.11.2.2 2004/08/03 17:42:42 herbelin Exp $ i*)
+(*i $Id: Arith.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Le.
 Require Export Lt.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 448ce002..7680997d 100755..100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Between.v,v 1.12.2.1 2004/07/16 19:30:59 herbelin Exp $ i*)
+(*i $Id: Between.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 55dfd47f..fed650ab 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Bool_nat.v,v 1.5.2.1 2004/07/16 19:30:59 herbelin Exp $ *)
+(* $Id: Bool_nat.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Compare_dec.
 Require Export Peano_dec.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 46827bae..b11f0517 100755..100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Compare.v,v 1.12.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Compare.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Equality is decidable on [nat] *)
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index ea21437d..3a87ee1a 100755..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,v 1.13.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Compare_dec.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v
index adb5593d..9011cee3 100755..100644
--- a/theories/Arith/Div.v
+++ b/theories/Arith/Div.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Div.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Div.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Euclidean division *)
 
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index c005f061..6e5d292f 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,v 1.15.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Div2.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 Require Import Lt.
 Require Import Plus.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 2e99e068..09df9464 100755..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,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: EqNat.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Equality on natural numbers *)
 
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index e50e3d70..23bc7cdb 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Euclid.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Euclid.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 Require Import Mult.
 Require Import Compare_dec.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index f7a2ad71..cdbc86df 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,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Even.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (** Here we define the predicates [even] and [odd] by mutual induction
     and we prove the decidability and the exclusion of those predicates.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 4db211e4..2767f9f0 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Factorial.v,v 1.5.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Factorial.v 6338 2004-11-22 09:10:51Z gregoire $ i*)
 
 Require Import Plus.
 Require Import Mult.
@@ -15,7 +15,7 @@ Open Local Scope nat_scope.
 
 (** Factorial *)
 
-Fixpoint fact (n:nat) : nat :=
+Boxed Fixpoint fact (n:nat) : nat :=
   match n with
   | O => 1
   | S n => S n * fact n
@@ -47,4 +47,4 @@ assumption.
 simpl (1 * fact n) in H0.
 rewrite <- plus_n_O in H0.
 assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index 299c664d..90f893a3 100755..100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Gt.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Gt.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Le.
 Require Import Lt.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index a5378cff..e95ef408 100755..100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Le.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Le.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Order on natural numbers *)
 Open Local Scope nat_scope.
@@ -62,15 +62,14 @@ 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 |- *.
-elim H; simpl in |- *; auto with arith.
+destruct H; simpl; auto with arith.
 Qed.
 Hint Immediate le_S_n: arith v62.
 
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
-induction n as [| n IHn]. simpl in |- *. auto with arith.
-destruct m as [| m]. simpl in |- *. intro H. inversion H.
-simpl in |- *. auto with arith.
+destruct n; simpl; auto with arith.
+destruct m; simpl; auto with arith.
 Qed.
 
 (** Comparison to 0 *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index e1b3e4b8..eeb4e35e 100755..100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lt.v,v 1.11.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Lt.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Le.
 Open Local Scope nat_scope.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 82673ed0..7f5c1148 100755..100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Max.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Arith.
 
@@ -69,17 +69,11 @@ induction n; induction m; simpl in |- *; auto with arith.
 elim (IHn m); intro H; elim H; auto.
 Qed.
 
-Lemma max_case : forall n m (P:nat -> Set), P n -> P m -> P (max n m).
-Proof.
-induction n; simpl in |- *; auto with arith.
-induction m; intros; simpl in |- *; auto with arith.
-pattern (max n m) in |- *; apply IHn; auto with arith.
-Qed.
-
-Lemma max_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (max n m).
+Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
 Proof.
 induction n; simpl in |- *; auto with arith.
 induction m; intros; simpl in |- *; auto with arith.
 pattern (max n m) in |- *; apply IHn; auto with arith.
 Qed.
 
+Notation max_case2 := max_case (only parsing).
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 912e7ba3..38351817 100755..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,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Min.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Arith.
 
@@ -68,16 +68,12 @@ induction n; induction m; simpl in |- *; auto with arith.
 elim (IHn m); intro H; elim H; auto.
 Qed.
 
-Lemma min_case : forall n m (P:nat -> Set), P n -> P m -> P (min n m).
+Lemma min_case : forall n m (P:nat -> Type), P n -> P m -> P (min n m).
 Proof.
 induction n; simpl in |- *; auto with arith.
 induction m; intros; simpl in |- *; auto with arith.
 pattern (min n m) in |- *; apply IHn; auto with arith.
 Qed.
 
-Lemma min_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (min n m).
-Proof.
-induction n; simpl in |- *; auto with arith.
-induction m; intros; simpl in |- *; auto with arith.
-pattern (min n m) in |- *; apply IHn; auto with arith.
-Qed.
\ No newline at end of file
+Notation min_case2 := min_case (only parsing).
+
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index ba9a46ad..dfecd7cf 100755..100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Minus.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Minus.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Subtraction (difference between two natural numbers) *)
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index abfade57..051f8645 100755..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,v 1.21.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Mult.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Plus.
 Require Export Minus.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 01204ee6..4aef7dc0 100755..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,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Peano_dec.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Decidable.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index e4ac631e..56e1c58a 100755..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,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+(*i $Id: Plus.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Properties of addition *)
 
@@ -199,4 +199,29 @@ 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.
 intro m; rewrite <- IHn; simpl in |- *; auto.
-Qed.
\ No newline at end of file
+Qed.
+
+(** Discrimination *)
+
+Lemma succ_plus_discr : forall n m, n <> S (plus m n).
+Proof.
+intros n m; induction n as [|n IHn].
+ discriminate.
+ intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; 
+   reflexivity.
+Qed.
+
+Lemma n_SSn : forall n, n <> S (S n).
+Proof.
+intro n; exact (succ_plus_discr n 1).
+Qed.
+
+Lemma n_SSSn : forall n, n <> S (S (S n)).
+Proof.
+intro n; exact (succ_plus_discr n 2).
+Qed.
+
+Lemma n_SSSSn : forall n, n <> S (S (S (S n))).
+Proof.
+intro n; exact (succ_plus_discr n 3).
+Qed.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 8bf237b5..e1bbfad9 100755..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,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
+(*i $Id: Wf_nat.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Well-founded relations and natural numbers *)
 
@@ -36,10 +36,12 @@ apply Acc_intro.
 unfold ltof in |- *; intros b ltfafb.
 apply IHn.
 apply lt_le_trans with (f a); auto with arith.
-Qed.
+Defined.
 
 Theorem well_founded_gtof : well_founded gtof.
-Proof well_founded_ltof.
+Proof.
+exact well_founded_ltof.
+Defined.
 
 (** It is possible to directly prove the induction principle going
    back to primitive recursion on natural numbers ([induction_ltof1])
@@ -113,31 +115,30 @@ apply Acc_intro.
 intros b ltfafb.
 apply IHn.
 apply lt_le_trans with (f a); auto with arith.
-Qed.
+Defined.
 
 End Well_founded_Nat.
 
 Lemma lt_wf : well_founded lt.
-Proof well_founded_ltof nat (fun m => m).
+Proof.
+exact (well_founded_ltof nat (fun m => m)).
+Defined.
 
 Lemma lt_wf_rec1 :
  forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
 Proof.
-exact
- (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =>
-    induction_ltof1 nat (fun m => m) P F p).
+exact (fun p P F => induction_ltof1 nat (fun m => m) P F p).
 Defined.
 
 Lemma lt_wf_rec :
  forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
 Proof.
-exact
- (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) =>
-    induction_ltof2 nat (fun m => m) P F p).
+exact (fun p P F => induction_ltof2 nat (fun m => m) P F p).
 Defined.
 
 Lemma lt_wf_ind :
  forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n.
+Proof.
 intro p; intros; elim (lt_wf p); auto with arith.
 Qed.
 
@@ -154,8 +155,9 @@ Proof lt_wf_ind.
 Lemma lt_wf_double_rec :
  forall P:nat -> nat -> Set,
    (forall n m,
-      (forall p (q:nat), p < n -> P p q) ->
+      (forall p q, p < n -> P p q) ->
       (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
+Proof.
 intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
 intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
 Defined.
@@ -165,6 +167,7 @@ Lemma lt_wf_double_ind :
    (forall n m,
       (forall p (q:nat), p < n -> P p q) ->
       (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
+Proof.
 intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
 intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
 Qed.
@@ -178,29 +181,29 @@ Variable R : A -> A -> Prop.
 
 (* Relational form of inversion *)
 Variable F : A -> nat -> Prop.
-Definition inv_lt_rel x y :=
-   exists2 n : _, F x n & (forall m, F y m -> n < m).
+Definition inv_lt_rel x y := exists2 n, F x n & (forall m, F y m -> n < m).
 
 Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y.
-Remark acc_lt_rel : forall x:A, (exists n : _, F x n) -> Acc R x.
-intros x [n fxn]; generalize x fxn; clear x fxn.
+Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
+Proof.
+intros x [n fxn]; generalize dependent x.
 pattern n in |- *; apply lt_wf_ind; intros.
 constructor; intros.
-case (F_compat y x); trivial; intros.
+destruct (F_compat y x) as (x0,H1,H2); trivial.
 apply (H x0); auto.
 Qed.
 
 Theorem well_founded_inv_lt_rel_compat : well_founded R.
+Proof.
 constructor; intros.
 case (F_compat y a); trivial; intros.
 apply acc_lt_rel; trivial.
 exists x; trivial.
 Qed.
 
-
 End LT_WF_REL.
 
 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.
\ No newline at end of file
+Qed.