diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Arith.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Between.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Bool_nat.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Compare.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Compare_dec.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Div.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/EqNat.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Euclid.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 6 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Gt.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Le.v | 9 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Lt.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Max.v | 12 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Min.v | 12 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Minus.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Mult.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Peano_dec.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Plus.v | 29 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Arith/Wf_nat.v | 41 |
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. |