summaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/Arith
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/Arith')
-rw-r--r--[-rwxr-xr-x]theories/Arith/Arith.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Between.v2
-rw-r--r--theories/Arith/Bool_nat.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Compare.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Compare_dec.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Div.v2
-rw-r--r--theories/Arith/Div2.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/EqNat.v2
-rw-r--r--theories/Arith/Euclid.v2
-rw-r--r--theories/Arith/Even.v2
-rw-r--r--theories/Arith/Factorial.v6
-rw-r--r--[-rwxr-xr-x]theories/Arith/Gt.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Le.v9
-rw-r--r--[-rwxr-xr-x]theories/Arith/Lt.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Max.v12
-rw-r--r--[-rwxr-xr-x]theories/Arith/Min.v12
-rw-r--r--[-rwxr-xr-x]theories/Arith/Minus.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Mult.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Peano_dec.v2
-rw-r--r--[-rwxr-xr-x]theories/Arith/Plus.v29
-rw-r--r--[-rwxr-xr-x]theories/Arith/Wf_nat.v41
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.