diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Arith.v | 14 | ||||
| -rw-r--r-- | theories/Arith/Arith_base.v | 20 | ||||
| -rw-r--r-- | theories/Arith/Between.v | 326 | ||||
| -rw-r--r-- | theories/Arith/Compare.v | 30 | ||||
| -rw-r--r-- | theories/Arith/Compare_dec.v | 116 | ||||
| -rw-r--r-- | theories/Arith/Div.v | 74 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 148 | ||||
| -rw-r--r-- | theories/Arith/EqNat.v | 70 | ||||
| -rw-r--r-- | theories/Arith/Euclid.v | 85 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 387 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 34 | ||||
| -rw-r--r-- | theories/Arith/Gt.v | 22 | ||||
| -rw-r--r-- | theories/Arith/Le.v | 110 | ||||
| -rw-r--r-- | theories/Arith/Lt.v | 77 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 42 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 44 | ||||
| -rw-r--r-- | theories/Arith/Minus.v | 98 | ||||
| -rw-r--r-- | theories/Arith/Mult.v | 189 | ||||
| -rw-r--r-- | theories/Arith/Peano_dec.v | 14 | ||||
| -rw-r--r-- | theories/Arith/Plus.v | 102 | ||||
| -rw-r--r-- | theories/Arith/Wf_nat.v | 185 |
21 files changed, 1148 insertions, 1039 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 59d9b2b1..be065f1d 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -6,15 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Arith.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Arith.v 9302 2006-10-27 21:21:17Z barras $ i*) -Require Export Le. -Require Export Lt. -Require Export Plus. -Require Export Gt. -Require Export Minus. -Require Export Mult. -Require Export Between. -Require Export Peano_dec. -Require Export Compare_dec. -Require Export Factorial. +Require Export Arith_base. +Require Export ArithRing. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v new file mode 100644 index 00000000..b076de2a --- /dev/null +++ b/theories/Arith/Arith_base.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* 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$ i*) + +Require Export Le. +Require Export Lt. +Require Export Plus. +Require Export Gt. +Require Export Minus. +Require Export Mult. +Require Export Between. +Require Export Peano_dec. +Require Export Compare_dec. +Require Export Factorial. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 7680997d..2e9472c4 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Between.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Le. Require Import Lt. @@ -16,174 +16,174 @@ Open Local Scope nat_scope. Implicit Types k l p q r : nat. Section Between. -Variables P Q : nat -> Prop. - -Inductive between k : nat -> Prop := - | bet_emp : between k k - | bet_S : forall l, between k l -> P l -> between k (S l). - -Hint Constructors between: arith v62. - -Lemma bet_eq : forall k l, l = k -> between k l. -Proof. -induction 1; auto with arith. -Qed. - -Hint Resolve bet_eq: arith v62. - -Lemma between_le : forall k l, between k l -> k <= l. -Proof. -induction 1; auto with arith. -Qed. -Hint Immediate between_le: arith v62. - -Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. -Proof. -induction 1. -intros; absurd (S k <= k); auto with arith. -destruct H; auto with arith. -Qed. -Hint Resolve between_Sk_l: arith v62. - -Lemma between_restr : - forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m. -Proof. -induction 1; auto with arith. -Qed. - -Inductive exists_between k : nat -> Prop := - | exists_S : forall l, exists_between k l -> exists_between k (S l) - | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). - -Hint Constructors exists_between: arith v62. - -Lemma exists_le_S : forall k l, exists_between k l -> S k <= l. -Proof. -induction 1; auto with arith. -Qed. - -Lemma exists_lt : forall k l, exists_between k l -> k < l. -Proof exists_le_S. -Hint Immediate exists_le_S exists_lt: arith v62. - -Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. -Proof. -intros; apply le_S_n; auto with arith. -Qed. -Hint Immediate exists_S_le: arith v62. - -Definition in_int p q r := p <= r /\ r < q. - -Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. -Proof. -red in |- *; auto with arith. -Qed. -Hint Resolve in_int_intro: arith v62. - -Lemma in_int_lt : forall p q r, in_int p q r -> p < q. -Proof. -induction 1; intros. -apply le_lt_trans with r; auto with arith. -Qed. - -Lemma in_int_p_Sq : - forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. -Proof. -induction 1; intros. -elim (le_lt_or_eq r q); auto with arith. -Qed. - -Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. -Proof. -induction 1; auto with arith. -Qed. -Hint Resolve in_int_S: arith v62. - -Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. -Proof. -induction 1; auto with arith. -Qed. -Hint Immediate in_int_Sp_q: arith v62. - -Lemma between_in_int : - forall k l, between k l -> forall r, in_int k l r -> P r. -Proof. -induction 1; intros. -absurd (k < k); auto with arith. -apply in_int_lt with r; auto with arith. -elim (in_int_p_Sq k l r); intros; auto with arith. -rewrite H2; trivial with arith. -Qed. - -Lemma in_int_between : - forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l. -Proof. -induction 1; auto with arith. -Qed. - -Lemma exists_in_int : - forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. -Proof. -induction 1. -case IHexists_between; intros p inp Qp; exists p; auto with arith. -exists l; auto with arith. -Qed. - -Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. -Proof. -destruct 1; intros. -elim H0; auto with arith. -Qed. - -Lemma between_or_exists : - forall k l, - k <= l -> - (forall n:nat, in_int k l n -> P n \/ Q n) -> - between k l \/ exists_between k l. -Proof. -induction 1; intros; auto with arith. -elim IHle; intro; auto with arith. -elim (H0 m); auto with arith. -Qed. - -Lemma between_not_exists : - forall k l, - between k l -> - (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. -Proof. -induction 1; red in |- *; intros. -absurd (k < k); auto with arith. -absurd (Q l); auto with arith. -elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. -replace l with l'; auto with arith. -elim inl'; intros. -elim (le_lt_or_eq l' l); auto with arith; intros. -absurd (exists_between k l); auto with arith. -apply in_int_exists with l'; auto with arith. -Qed. - -Inductive P_nth (init:nat) : nat -> nat -> Prop := - | nth_O : P_nth init init 0 - | nth_S : + Variables P Q : nat -> Prop. + + Inductive between k : nat -> Prop := + | bet_emp : between k k + | bet_S : forall l, between k l -> P l -> between k (S l). + + Hint Constructors between: arith v62. + + Lemma bet_eq : forall k l, l = k -> between k l. + Proof. + induction 1; auto with arith. + Qed. + + Hint Resolve bet_eq: arith v62. + + Lemma between_le : forall k l, between k l -> k <= l. + Proof. + induction 1; auto with arith. + Qed. + Hint Immediate between_le: arith v62. + + Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. + Proof. + intros k l H; induction H as [|l H]. + intros; absurd (S k <= k); auto with arith. + destruct H; auto with arith. + Qed. + Hint Resolve between_Sk_l: arith v62. + + Lemma between_restr : + forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m. + Proof. + induction 1; auto with arith. + Qed. + + Inductive exists_between k : nat -> Prop := + | exists_S : forall l, exists_between k l -> exists_between k (S l) + | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). + + Hint Constructors exists_between: arith v62. + + Lemma exists_le_S : forall k l, exists_between k l -> S k <= l. + Proof. + induction 1; auto with arith. + Qed. + + Lemma exists_lt : forall k l, exists_between k l -> k < l. + Proof exists_le_S. + Hint Immediate exists_le_S exists_lt: arith v62. + + Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. + Proof. + intros; apply le_S_n; auto with arith. + Qed. + Hint Immediate exists_S_le: arith v62. + + Definition in_int p q r := p <= r /\ r < q. + + Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. + Proof. + red in |- *; auto with arith. + Qed. + Hint Resolve in_int_intro: arith v62. + + Lemma in_int_lt : forall p q r, in_int p q r -> p < q. + Proof. + induction 1; intros. + apply le_lt_trans with r; auto with arith. + Qed. + + Lemma in_int_p_Sq : + forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. + Proof. + induction 1; intros. + elim (le_lt_or_eq r q); auto with arith. + Qed. + + Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. + Proof. + induction 1; auto with arith. + Qed. + Hint Resolve in_int_S: arith v62. + + Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. + Proof. + induction 1; auto with arith. + Qed. + Hint Immediate in_int_Sp_q: arith v62. + + Lemma between_in_int : + forall k l, between k l -> forall r, in_int k l r -> P r. + Proof. + induction 1; intros. + absurd (k < k); auto with arith. + apply in_int_lt with r; auto with arith. + elim (in_int_p_Sq k l r); intros; auto with arith. + rewrite H2; trivial with arith. + Qed. + + Lemma in_int_between : + forall k l, k <= l -> (forall r, in_int k l r -> P r) -> between k l. + Proof. + induction 1; auto with arith. + Qed. + + Lemma exists_in_int : + forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. + Proof. + induction 1. + case IHexists_between; intros p inp Qp; exists p; auto with arith. + exists l; auto with arith. + Qed. + + Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. + Proof. + destruct 1; intros. + elim H0; auto with arith. + Qed. + + Lemma between_or_exists : + forall k l, + k <= l -> + (forall n:nat, in_int k l n -> P n \/ Q n) -> + between k l \/ exists_between k l. + Proof. + induction 1; intros; auto with arith. + elim IHle; intro; auto with arith. + elim (H0 m); auto with arith. + Qed. + + Lemma between_not_exists : + forall k l, + between k l -> + (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. + Proof. + induction 1; red in |- *; intros. + absurd (k < k); auto with arith. + absurd (Q l); auto with arith. + elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. + replace l with l'; auto with arith. + elim inl'; intros. + elim (le_lt_or_eq l' l); auto with arith; intros. + absurd (exists_between k l); auto with arith. + apply in_int_exists with l'; auto with arith. + Qed. + + Inductive P_nth (init:nat) : nat -> nat -> Prop := + | nth_O : P_nth init init 0 + | nth_S : forall k l (n:nat), - P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n). + P_nth init k n -> between (S k) l -> Q l -> P_nth init l (S n). -Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. -Proof. -induction 1; intros; auto with arith. -apply le_trans with (S k); auto with arith. -Qed. + Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. + Proof. + induction 1; intros; auto with arith. + apply le_trans with (S k); auto with arith. + Qed. -Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. + Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. -Lemma event_O : eventually 0 -> Q 0. -Proof. -induction 1; intros. -replace 0 with x; auto with arith. -Qed. + Lemma event_O : eventually 0 -> Q 0. + Proof. + induction 1; intros. + replace 0 with x; auto with arith. + Qed. End Between. Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le in_int_S in_int_intro: arith v62. -Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
\ No newline at end of file +Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index b11f0517..06898658 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -6,21 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Compare.v 9302 2006-10-27 21:21:17Z barras $ i*) (** Equality is decidable on [nat] *) + Open Local Scope nat_scope. -(* -Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p). -Proof sym_not_eq. -Hints Immediate not_eq_sym : arith. -*) Notation not_eq_sym := sym_not_eq. Implicit Types m n p q : nat. -Require Import Arith. +Require Import Arith_base. Require Import Peano_dec. Require Import Compare_dec. @@ -41,17 +37,17 @@ Proof le_lt_or_eq. (* By special request of G. Kahn - Used in Group Theory *) Lemma discrete_nat : - forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))). + forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))). Proof. -intros m n H. -lapply (lt_le_S m n); auto with arith. -intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. -induction 1; auto with arith. -right; exists (n - S (S m)); simpl in |- *. -rewrite (plus_comm m (n - S (S m))). -rewrite (plus_n_Sm (n - S (S m)) m). -rewrite (plus_n_Sm (n - S (S m)) (S m)). -rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. + intros m n H. + lapply (lt_le_S m n); auto with arith. + intro H'; lapply (le_lt_or_eq (S m) n); auto with arith. + induction 1; auto with arith. + right; exists (n - S (S m)); simpl in |- *. + rewrite (plus_comm m (n - S (S m))). + rewrite (plus_n_Sm (n - S (S m)) m). + rewrite (plus_n_Sm (n - S (S m)) (S m)). + rewrite (plus_comm (n - S (S m)) (S (S m))); auto with arith. Qed. Require Export Wf_nat. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index d2eead86..e6dc7c46 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 8733 2006-04-25 22:52:18Z letouzey $ i*) +(*i $Id: Compare_dec.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Le. Require Import Lt. @@ -17,109 +17,113 @@ Open Local Scope nat_scope. Implicit Types m n x y : nat. -Definition zerop : forall n, {n = 0} + {0 < n}. -destruct n; auto with arith. +Definition zerop n : {n = 0} + {0 < n}. + destruct n; auto with arith. Defined. -Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}. -Proof. -induction n; simple destruct m; auto with arith. -intros m0; elim (IHn m0); auto with arith. -induction 1; auto with arith. +Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. + induction n; simple destruct m; auto with arith. + intros m0; elim (IHn m0); auto with arith. + induction 1; auto with arith. Defined. -Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}. -Proof lt_eq_lt_dec. +Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. + exact lt_eq_lt_dec. +Defined. -Lemma le_lt_dec : forall n m, {n <= m} + {m < n}. -Proof. -induction n. -auto with arith. -induction m. -auto with arith. -elim (IHn m); auto with arith. +Definition le_lt_dec n m : {n <= m} + {m < n}. + induction n. + auto with arith. + induction m. + auto with arith. + elim (IHn m); auto with arith. Defined. -Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}. -Proof. -exact le_lt_dec. +Definition le_le_S_dec n m : {n <= m} + {S m <= n}. + exact le_lt_dec. Defined. -Definition le_ge_dec : forall n m, {n <= m} + {n >= m}. -Proof. -intros; elim (le_lt_dec n m); auto with arith. +Definition le_ge_dec n m : {n <= m} + {n >= m}. + intros; elim (le_lt_dec n m); auto with arith. Defined. -Definition le_gt_dec : forall n m, {n <= m} + {n > m}. -Proof. -exact le_lt_dec. +Definition le_gt_dec n m : {n <= m} + {n > m}. + exact le_lt_dec. Defined. -Definition le_lt_eq_dec : forall n m, n <= m -> {n < m} + {n = m}. -Proof. -intros; elim (lt_eq_lt_dec n m); auto with arith. -intros; absurd (m < n); auto with arith. +Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}. + intros; elim (lt_eq_lt_dec n m); auto with arith. + intros; absurd (m < n); auto with arith. Defined. (** Proofs of decidability *) Theorem dec_le : forall n m, decidable (n <= m). -intros x y; unfold decidable in |- *; elim (le_gt_dec x y); - [ auto with arith | intro; right; apply gt_not_le; assumption ]. +Proof. + intros x y; unfold decidable in |- *; elim (le_gt_dec x y); + [ auto with arith | intro; right; apply gt_not_le; assumption ]. Qed. Theorem dec_lt : forall n m, decidable (n < m). -intros x y; unfold lt in |- *; apply dec_le. +Proof. + intros x y; unfold lt in |- *; apply dec_le. Qed. Theorem dec_gt : forall n m, decidable (n > m). -intros x y; unfold gt in |- *; apply dec_lt. +Proof. + intros x y; unfold gt in |- *; apply dec_lt. Qed. Theorem dec_ge : forall n m, decidable (n >= m). -intros x y; unfold ge in |- *; apply dec_le. +Proof. + intros x y; unfold ge in |- *; apply dec_le. Qed. Theorem not_eq : forall n m, n <> m -> n < m \/ m < n. -intros x y H; elim (lt_eq_lt_dec x y); - [ intros H1; elim H1; - [ auto with arith | intros H2; absurd (x = y); assumption ] - | auto with arith ]. +Proof. + intros x y H; elim (lt_eq_lt_dec x y); + [ intros H1; elim H1; + [ auto with arith | intros H2; absurd (x = y); assumption ] + | auto with arith ]. Qed. Theorem not_le : forall n m, ~ n <= m -> n > m. -intros x y H; elim (le_gt_dec x y); - [ intros H1; absurd (x <= y); assumption | trivial with arith ]. +Proof. + intros x y H; elim (le_gt_dec x y); + [ intros H1; absurd (x <= y); assumption | trivial with arith ]. Qed. Theorem not_gt : forall n m, ~ n > m -> n <= m. -intros x y H; elim (le_gt_dec x y); - [ trivial with arith | intros H1; absurd (x > y); assumption ]. +Proof. + intros x y H; elim (le_gt_dec x y); + [ trivial with arith | intros H1; absurd (x > y); assumption ]. Qed. Theorem not_ge : forall n m, ~ n >= m -> n < m. -intros x y H; exact (not_le y x H). +Proof. + intros x y H; exact (not_le y x H). Qed. Theorem not_lt : forall n m, ~ n < m -> n >= m. -intros x y H; exact (not_gt y x H). +Proof. + intros x y H; exact (not_gt y x H). Qed. (** A ternary comparison function in the spirit of [Zcompare]. *) Definition nat_compare (n m:nat) := - match lt_eq_lt_dec n m with - | inleft (left _) => Lt - | inleft (right _) => Eq - | inright _ => Gt - end. + match lt_eq_lt_dec n m with + | inleft (left _) => Lt + | inleft (right _) => Eq + | inright _ => Gt + end. Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m. Proof. - unfold nat_compare; intros. - simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto. + unfold nat_compare; intros. + simpl; destruct (lt_eq_lt_dec n m) as [[H|H]|H]; simpl; auto. Qed. Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m. @@ -188,11 +192,11 @@ Qed. Fixpoint leb (m:nat) : nat -> bool := match m with - | O => fun _:nat => true - | S m' => + | O => fun _:nat => true + | S m' => fun n:nat => match n with - | O => false - | S n' => leb m' n' + | O => false + | S n' => leb m' n' end end. diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index 9011cee3..1dec34e2 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Div.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Euclidean division *) @@ -20,45 +20,45 @@ 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. + [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. + 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. + 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 ca1f39af..c32759b2 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 8733 2006-04-25 22:52:18Z letouzey $ i*) +(*i $Id: Div2.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Lt. Require Import Plus. @@ -30,28 +30,30 @@ Fixpoint div2 n : nat := useful to prove the corresponding induction principle *) Lemma ind_0_1_SS : - forall P:nat -> Prop, - P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. + forall P:nat -> Prop, + P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. -intros. -cut (forall n, P n /\ P (S n)). -intros. elim (H2 n). auto with arith. - -induction n0. auto with arith. -intros. elim IHn0; auto with arith. + intros P H0 H1 Hn. + cut (forall n, P n /\ P (S n)). + intros H'n n. elim (H'n n). auto with arith. + + induction n. auto with arith. + intros. elim IHn; auto with arith. Qed. (** [0 <n => n/2 < n] *) Lemma lt_div2 : forall n, 0 < n -> div2 n < n. Proof. -intro n. pattern n in |- *. apply ind_0_1_SS. -intro. inversion H. -auto with arith. -intros. simpl in |- *. -case (zerop n0). -intro. rewrite e. auto with arith. -auto with arith. + intro n. pattern n in |- *. apply ind_0_1_SS. + (* n = 0 *) + inversion 1. + (* n=1 *) + simpl; trivial. + (* n=S S n' *) + intro n'; case (zerop n'). + intro n'_eq_0. rewrite n'_eq_0. auto with arith. + auto with arith. Qed. Hint Resolve lt_div2: arith. @@ -59,27 +61,27 @@ Hint Resolve lt_div2: arith. (** Properties related to the parity *) Lemma even_odd_div2 : - forall n, - (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)). + forall n, + (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)). Proof. -intro n. pattern n in |- *. apply ind_0_1_SS. -(* n = 0 *) -split. split; auto with arith. -split. intro H. inversion H. -intro H. absurd (S (div2 0) = div2 1); auto with arith. -(* n = 1 *) -split. split. intro. inversion H. inversion H1. -intro H. absurd (div2 1 = div2 2). -simpl in |- *. discriminate. assumption. -split; auto with arith. -(* n = (S (S n')) *) -intros. decompose [and] H. unfold iff in H0, H1. -decompose [and] H0. decompose [and] H1. clear H H0 H1. -split; split; auto with arith. -intro H. inversion H. inversion H1. -change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith. -intro H. inversion H. inversion H1. -change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith. + intro n. pattern n in |- *. apply ind_0_1_SS. + (* n = 0 *) + split. split; auto with arith. + split. intro H. inversion H. + intro H. absurd (S (div2 0) = div2 1); auto with arith. + (* n = 1 *) + split. split. intro. inversion H. inversion H1. + intro H. absurd (div2 1 = div2 2). + simpl in |- *. discriminate. assumption. + split; auto with arith. + (* n = (S (S n')) *) + intros. decompose [and] H. unfold iff in H0, H1. + decompose [and] H0. decompose [and] H1. clear H H0 H1. + split; split; auto with arith. + intro H. inversion H. inversion H1. + change (S (div2 n0) = S (div2 (S n0))) in |- *. auto with arith. + intro H. inversion H. inversion H1. + change (S (S (div2 n0)) = S (div2 (S n0))) in |- *. auto with arith. Qed. (** Specializations *) @@ -106,39 +108,39 @@ Hint Unfold double: arith. Lemma double_S : forall n, double (S n) = S (S (double n)). Proof. -intro. unfold double in |- *. simpl in |- *. auto with arith. + intro. unfold double in |- *. simpl in |- *. auto with arith. Qed. Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m. Proof. -intros m n. unfold double in |- *. -do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). -reflexivity. + intros m n. unfold double in |- *. + do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). + reflexivity. Qed. Hint Resolve double_S: arith. Lemma even_odd_double : - forall n, - (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). + forall n, + (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. -intro n. pattern n in |- *. apply ind_0_1_SS. -(* n = 0 *) -split; split; auto with arith. -intro H. inversion H. -(* n = 1 *) -split; split; auto with arith. -intro H. inversion H. inversion H1. -(* n = (S (S n')) *) -intros. decompose [and] H. unfold iff in H0, H1. -decompose [and] H0. decompose [and] H1. clear H H0 H1. -split; split. -intro H. inversion H. inversion H1. -simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. -simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. -intro H. inversion H. inversion H1. -simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. -simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. + intro n. pattern n in |- *. apply ind_0_1_SS. + (* n = 0 *) + split; split; auto with arith. + intro H. inversion H. + (* n = 1 *) + split; split; auto with arith. + intro H. inversion H. inversion H1. + (* n = (S (S n')) *) + intros. decompose [and] H. unfold iff in H0, H1. + decompose [and] H0. decompose [and] H1. clear H H0 H1. + split; split. + intro H. inversion H. inversion H1. + simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. + simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. + intro H. inversion H. inversion H1. + simpl in |- *. rewrite (double_S (div2 n0)). auto with arith. + simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. Qed. @@ -166,32 +168,32 @@ 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. + intros n H. exists (div2 n). auto with arith. Qed. Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}. Proof. -intros n H. exists (div2 n). auto with arith. + intros n H. exists (div2 n). auto with arith. Qed. (** Doubling before dividing by two brings back to the initial number. *) Lemma div2_double : forall n:nat, div2 (2*n) = n. Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. + induction n. + simpl; auto. + simpl. + replace (n+S(n+0)) with (S (2*n)). + f_equal; auto. + simpl; auto with arith. Qed. Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n. Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. + induction n. + simpl; auto. + simpl. + replace (n+S(n+0)) with (S (2*n)). + f_equal; auto. + simpl; auto with arith. Qed. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 09df9464..82d05e2c 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: EqNat.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Equality on natural numbers *) @@ -14,52 +14,66 @@ Open Local Scope nat_scope. Implicit Types m n x y : nat. +(** * Propositional equality *) + Fixpoint eq_nat n m {struct n} : Prop := match n, m with - | O, O => True - | O, S _ => False - | S _, O => False - | S n1, S m1 => eq_nat n1 m1 + | O, O => True + | O, S _ => False + | S _, O => False + | S n1, S m1 => eq_nat n1 m1 end. Theorem eq_nat_refl : forall n, eq_nat n n. -induction n; simpl in |- *; auto. + induction n; simpl in |- *; auto. Qed. Hint Resolve eq_nat_refl: arith v62. -Theorem eq_eq_nat : forall n m, n = m -> eq_nat n m. -induction 1; trivial with arith. +(** [eq] restricted to [nat] and [eq_nat] are equivalent *) + +Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m. + induction 1; trivial with arith. Qed. Hint Immediate eq_eq_nat: arith v62. -Theorem eq_nat_eq : forall n m, eq_nat n m -> n = m. -induction n; induction m; simpl in |- *; contradiction || auto with arith. +Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m. + induction n; induction m; simpl in |- *; contradiction || auto with arith. Qed. Hint Immediate eq_nat_eq: arith v62. +Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m. +Proof. + split; auto with arith. +Qed. + Theorem eq_nat_elim : - forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. -intros; replace m with n; auto with arith. + forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. +Proof. + intros; replace m with n; auto with arith. Qed. Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. -induction n. -destruct m as [| n]. -auto with arith. -intros; right; red in |- *; trivial with arith. -destruct m as [| n0]. -right; red in |- *; auto with arith. -intros. -simpl in |- *. -apply IHn. +Proof. + induction n. + destruct m as [| n]. + auto with arith. + intros; right; red in |- *; trivial with arith. + destruct m as [| n0]. + right; red in |- *; auto with arith. + intros. + simpl in |- *. + apply IHn. Defined. + +(** * Boolean equality on [nat] *) + Fixpoint beq_nat n m {struct n} : bool := match n, m with - | O, O => true - | O, S _ => false - | S _, O => false - | S n1, S m1 => beq_nat n1 m1 + | O, O => true + | O, S _ => false + | S _, O => false + | S n1, S m1 => beq_nat n1 m1 end. Lemma beq_nat_refl : forall n, true = beq_nat n n. @@ -71,7 +85,7 @@ Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y. Proof. double induction x y; simpl in |- *. reflexivity. - intros; discriminate H0. - intros; discriminate H0. - intros; case (H0 _ H1); reflexivity. + intros n H1 H2. discriminate H2. + intros n H1 H2. discriminate H2. + intros n H1 z H2 H3. case (H2 _ H3). reflexivity. Defined. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 23bc7cdb..3d6f1af5 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 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Euclid.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Mult. Require Import Compare_dec. @@ -17,52 +17,55 @@ Open Local 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. + 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. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros q r g e. -apply divex with (S q) r; simpl in |- *; auto with arith. -elim plus_assoc. -elim e; auto with arith. -intros gtbn. -apply divex with 0 n; simpl in |- *; auto with arith. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros q r g e. + apply divex with (S q) r; simpl in |- *; auto with arith. + elim plus_assoc. + elim e; auto with arith. + intros gtbn. + apply divex with 0 n; simpl in |- *; auto with arith. Qed. Lemma quotient : - forall n, - n > 0 -> - forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros q Hq; exists (S q). -elim Hq; intros r Hr. -exists r; simpl in |- *; elim Hr; intros. -elim plus_assoc. -elim H1; auto with arith. -intros gtbn. -exists 0; exists n; simpl in |- *; auto with arith. + forall n, + n > 0 -> + forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros q Hq; exists (S q). + elim Hq; intros r Hr. + exists r; simpl in |- *; elim Hr; intros. + elim plus_assoc. + elim H1; auto with arith. + intros gtbn. + exists 0; exists n; simpl in |- *; auto with arith. Qed. Lemma modulo : - forall n, - n > 0 -> - forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros r Hr; exists r. -elim Hr; intros q Hq. -elim Hq; intros; exists (S q); simpl in |- *. -elim plus_assoc. -elim H1; auto with arith. -intros gtbn. -exists n; exists 0; simpl in |- *; auto with arith. -Qed.
\ No newline at end of file + forall n, + n > 0 -> + forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros r Hr; exists r. + elim Hr; intros q Hq. + elim Hq; intros; exists (S q); simpl in |- *. + elim plus_assoc. + elim H1; auto with arith. + intros gtbn. + exists n; exists 0; simpl in |- *; auto with arith. +Qed. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index cdbc86df..83c0ce17 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 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Even.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. @@ -16,6 +16,9 @@ Open Local Scope nat_scope. Implicit Types m n : nat. + +(** * Definition of [even] and [odd], and basic facts *) + Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) @@ -27,279 +30,285 @@ Hint Constructors odd: arith. Lemma even_or_odd : forall n, even n \/ odd n. Proof. -induction n. -auto with arith. -elim IHn; auto with arith. + induction n. + auto with arith. + elim IHn; auto with arith. Qed. Lemma even_odd_dec : forall n, {even n} + {odd n}. Proof. -induction n. -auto with arith. -elim IHn; auto with arith. + induction n. + auto with arith. + elim IHn; auto with arith. Qed. Lemma not_even_and_odd : forall n, even n -> odd n -> False. Proof. -induction n. -intros. inversion H0. -intros. inversion H. inversion H0. auto with arith. + induction n. + intros even_0 odd_0. inversion odd_0. + intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith. Qed. + +(** * Facts about [even] & [odd] wrt. [plus] *) + Lemma even_plus_aux : - forall n m, - (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ - (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). + forall n m, + (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ + (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). Proof. -intros n; elim n; simpl in |- *; auto with arith. -intros m; split; auto. -split. -intros H; right; split; auto with arith. -intros H'; case H'; auto with arith. -intros H'0; elim H'0; intros H'1 H'2; inversion H'1. -intros H; elim H; auto. -split; auto with arith. -intros H'; elim H'; auto with arith. -intros H; elim H; auto. -intros H'0; elim H'0; intros H'1 H'2; inversion H'1. -intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2; - intros E3 E4; clear H'1 H'2. -split; split. -intros H'0; case E3. -inversion H'0; auto. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H'0; case H'0; intros C0; case C0; intros C1 C2. -apply odd_S. -apply E4; left; split; auto with arith. -inversion C1; auto. -apply odd_S. -apply E4; right; split; auto with arith. -inversion C1; auto. -intros H'0. -case E1. -inversion H'0; auto. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H; elim H; intros H0 H1; clear H; auto with arith. -intros H'0; case H'0; intros C0; case C0; intros C1 C2. -apply even_S. -apply E2; left; split; auto with arith. -inversion C1; auto. -apply even_S. -apply E2; right; split; auto with arith. -inversion C1; auto. + intros n; elim n; simpl in |- *; auto with arith. + intros m; split; auto. + split. + intros H; right; split; auto with arith. + intros H'; case H'; auto with arith. + intros H'0; elim H'0; intros H'1 H'2; inversion H'1. + intros H; elim H; auto. + split; auto with arith. + intros H'; elim H'; auto with arith. + intros H; elim H; auto. + intros H'0; elim H'0; intros H'1 H'2; inversion H'1. + intros n0 H' m; elim (H' m); intros H'1 H'2; elim H'1; intros E1 E2; elim H'2; + intros E3 E4; clear H'1 H'2. + split; split. + intros H'0; case E3. + inversion H'0; auto. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H'0; case H'0; intros C0; case C0; intros C1 C2. + apply odd_S. + apply E4; left; split; auto with arith. + inversion C1; auto. + apply odd_S. + apply E4; right; split; auto with arith. + inversion C1; auto. + intros H'0. + case E1. + inversion H'0; auto. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H; elim H; intros H0 H1; clear H; auto with arith. + intros H'0; case H'0; intros C0; case C0; intros C1 C2. + apply even_S. + apply E2; left; split; auto with arith. + inversion C1; auto. + apply even_S. + apply E2; right; split; auto with arith. + inversion C1; auto. Qed. Lemma even_even_plus : forall n m, even n -> even m -> even (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H H0; case H0; auto. + intros n m; case (even_plus_aux n m). + intros H H0; case H0; auto. Qed. Lemma odd_even_plus : forall n m, odd n -> odd m -> even (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H H0; case H0; auto. + intros n m; case (even_plus_aux n m). + intros H H0; case H0; auto. Qed. - + Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0; elim H0; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0; elim H0; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. Qed. Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0; elim H0; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0; elim H0; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. Qed. - + Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. + intros H0; case H0; auto. Qed. - + Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'0. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'0. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Hint Resolve even_even_plus odd_even_plus: arith. - + Lemma odd_plus_l : forall n m, odd n -> even m -> odd (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H; case H; auto. + intros n m; case (even_plus_aux n m). + intros H; case H; auto. Qed. Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m). Proof. -intros n m; case (even_plus_aux n m). -intros H; case H; auto. + intros n m; case (even_plus_aux n m). + intros H; case H; auto. Qed. Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0; case H0; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0; case H0; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. Qed. Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0; case H0; auto. -intros H0 H1 H2; case (not_even_and_odd m); auto. -case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0; case H0; auto. + intros H0 H1 H2; case (not_even_and_odd m); auto. + case H0; auto. Qed. - + Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m. Proof. -intros n m H; case (even_plus_aux n m). -intros H' H'0; elim H'. -intros H'1; case H'1; auto. -intros H0 H1 H2; case (not_even_and_odd n); auto. -case H0; auto. -intros H0; case H0; auto. + intros n m H; case (even_plus_aux n m). + intros H' H'0; elim H'. + intros H'1; case H'1; auto. + intros H0 H1 H2; case (not_even_and_odd n); auto. + case H0; auto. + intros H0; case H0; auto. Qed. Hint Resolve odd_plus_l odd_plus_r: arith. - + + +(** * Facts about [even] and [odd] wrt. [mult] *) + Lemma even_mult_aux : - forall n m, - (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). + forall n m, + (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). Proof. -intros n; elim n; simpl in |- *; auto with arith. -intros m; split; split; auto with arith. -intros H'; inversion H'. -intros H'; elim H'; auto. -intros n0 H' m; split; split; auto with arith. -intros H'0. -elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; - case H'1; auto. -intros H'5; elim H'5; intros H'6 H'7; auto with arith. -split; auto with arith. -case (H' m). -intros H'8 H'9; case H'9. -intros H'10; case H'10; auto with arith. -intros H'11 H'12; case (not_even_and_odd m); auto with arith. -intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. -case (H' m). -intros H'8 H'9; case H'9; auto. -intros H'0; elim H'0; intros H'1 H'2; clear H'0. -elim (even_plus_aux m (n0 * m)); auto. -intros H'0 H'3. -elim H'0. -intros H'4 H'5; apply H'5; auto. -left; split; auto with arith. -case (H' m). -intros H'6 H'7; elim H'7. -intros H'8 H'9; apply H'9. -left. -inversion H'1; auto. -intros H'0. -elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. -intros H'1 H'2. -elim H'1; auto. -intros H; case H; auto. -intros H'5; elim H'5; intros H'6 H'7; auto with arith. -left. -case (H' m). -intros H'8; elim H'8. -intros H'9; elim H'9; auto with arith. -intros H'0; elim H'0; intros H'1. -case (even_or_odd m); intros H'2. -apply even_even_plus; auto. -case (H' m). -intros H H0; case H0; auto. -apply odd_even_plus; auto. -inversion H'1; case (H' m); auto. -intros H1; case H1; auto. -apply even_even_plus; auto. -case (H' m). -intros H H0; case H0; auto. + intros n; elim n; simpl in |- *; auto with arith. + intros m; split; split; auto with arith. + intros H'; inversion H'. + intros H'; elim H'; auto. + intros n0 H' m; split; split; auto with arith. + intros H'0. + elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; + case H'1; auto. + intros H'5; elim H'5; intros H'6 H'7; auto with arith. + split; auto with arith. + case (H' m). + intros H'8 H'9; case H'9. + intros H'10; case H'10; auto with arith. + intros H'11 H'12; case (not_even_and_odd m); auto with arith. + intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. + case (H' m). + intros H'8 H'9; case H'9; auto. + intros H'0; elim H'0; intros H'1 H'2; clear H'0. + elim (even_plus_aux m (n0 * m)); auto. + intros H'0 H'3. + elim H'0. + intros H'4 H'5; apply H'5; auto. + left; split; auto with arith. + case (H' m). + intros H'6 H'7; elim H'7. + intros H'8 H'9; apply H'9. + left. + inversion H'1; auto. + intros H'0. + elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. + intros H'1 H'2. + elim H'1; auto. + intros H; case H; auto. + intros H'5; elim H'5; intros H'6 H'7; auto with arith. + left. + case (H' m). + intros H'8; elim H'8. + intros H'9; elim H'9; auto with arith. + intros H'0; elim H'0; intros H'1. + case (even_or_odd m); intros H'2. + apply even_even_plus; auto. + case (H' m). + intros H H0; case H0; auto. + apply odd_even_plus; auto. + inversion H'1; case (H' m); auto. + intros H1; case H1; auto. + apply even_even_plus; auto. + case (H' m). + intros H H0; case H0; auto. Qed. - + Lemma even_mult_l : forall n m, even n -> even (n * m). Proof. -intros n m; case (even_mult_aux n m); auto. -intros H H0; case H0; auto. + intros n m; case (even_mult_aux n m); auto. + intros H H0; case H0; auto. Qed. Lemma even_mult_r : forall n m, even m -> even (n * m). Proof. -intros n m; case (even_mult_aux n m); auto. -intros H H0; case H0; auto. + intros n m; case (even_mult_aux n m); auto. + intros H H0; case H0; auto. Qed. Hint Resolve even_mult_l even_mult_r: arith. - + Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m. Proof. -intros n m H' H'0. -case (even_mult_aux n m). -intros H'1 H'2; elim H'2. -intros H'3; elim H'3; auto. -intros H; case (not_even_and_odd n); auto. + intros n m H' H'0. + case (even_mult_aux n m). + intros H'1 H'2; elim H'2. + intros H'3; elim H'3; auto. + intros H; case (not_even_and_odd n); auto. Qed. Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n. Proof. -intros n m H' H'0. -case (even_mult_aux n m). -intros H'1 H'2; elim H'2. -intros H'3; elim H'3; auto. -intros H; case (not_even_and_odd m); auto. + intros n m H' H'0. + case (even_mult_aux n m). + intros H'1 H'2; elim H'2. + intros H'3; elim H'3; auto. + intros H; case (not_even_and_odd m); auto. Qed. Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m). Proof. -intros n m; case (even_mult_aux n m); intros H; case H; auto. + intros n m; case (even_mult_aux n m); intros H; case H; auto. Qed. Hint Resolve even_mult_l even_mult_r odd_mult: arith. Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n. Proof. -intros n m H'. -case (even_mult_aux n m). -intros H'1 H'2; elim H'1. -intros H'3; elim H'3; auto. + intros n m H'. + case (even_mult_aux n m). + intros H'1 H'2; elim H'1. + intros H'3; elim H'3; auto. Qed. - + Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m. Proof. -intros n m H'. -case (even_mult_aux n m). -intros H'1 H'2; elim H'1. -intros H'3; elim H'3; auto. + intros n m H'. + case (even_mult_aux n m). + intros H'1 H'2; elim H'1. + intros H'3; elim H'3; auto. Qed. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 2767f9f0..5e2f491a 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 6338 2004-11-22 09:10:51Z gregoire $ i*) +(*i $Id: Factorial.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Plus. Require Import Mult. @@ -17,34 +17,34 @@ Open Local Scope nat_scope. Boxed Fixpoint fact (n:nat) : nat := match n with - | O => 1 - | S n => S n * fact n + | O => 1 + | S n => S n * fact n end. Arguments Scope fact [nat_scope]. Lemma lt_O_fact : forall n:nat, 0 < fact n. Proof. -simple induction n; unfold lt in |- *; simpl in |- *; auto with arith. + simple induction n; unfold lt in |- *; simpl in |- *; auto with arith. Qed. Lemma fact_neq_0 : forall n:nat, fact n <> 0. Proof. -intro. -apply sym_not_eq. -apply lt_O_neq. -apply lt_O_fact. + intro. + apply sym_not_eq. + apply lt_O_neq. + apply lt_O_fact. Qed. Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. Proof. -induction 1. -apply le_n. -assert (1 * fact n <= S m * fact m). -apply mult_le_compat. -apply lt_le_S; apply lt_O_Sn. -assumption. -simpl (1 * fact n) in H0. -rewrite <- plus_n_O in H0. -assumption. + induction 1. + apply le_n. + assert (1 * fact n <= S m * fact m). + apply mult_le_compat. + apply lt_le_S; apply lt_O_Sn. + assumption. + simpl (1 * fact n) in H0. + rewrite <- plus_n_O in H0. + assumption. Qed. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 90f893a3..5b1ee1b2 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,7 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Gt.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Gt.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: +<< +Definition gt (n m:nat) := m < n. +>> +*) Require Import Le. Require Import Lt. @@ -15,7 +21,7 @@ Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Order and successor *) +(** * Order and successor *) Theorem gt_Sn_O : forall n, S n > 0. Proof. @@ -52,20 +58,20 @@ Proof. Qed. Hint Immediate gt_pred: arith v62. -(** Irreflexivity *) +(** * Irreflexivity *) Lemma gt_irrefl : forall n, ~ n > n. Proof lt_irrefl. Hint Resolve gt_irrefl: arith v62. -(** Asymmetry *) +(** * Asymmetry *) Lemma gt_asym : forall n m, n > m -> ~ m > n. Proof fun n m => lt_asym m n. Hint Resolve gt_asym: arith v62. -(** Relating strict and large orders *) +(** * Relating strict and large orders *) Lemma le_not_gt : forall n m, n <= m -> ~ n > m. Proof le_not_lt. @@ -102,7 +108,7 @@ Proof. Qed. Hint Resolve le_gt_S: arith v62. -(** Transitivity *) +(** * Transitivity *) Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. Proof. @@ -127,14 +133,14 @@ Qed. Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. -(** Comparison to 0 *) +(** * Comparison to 0 *) Theorem gt_O_eq : forall n, n > 0 \/ 0 = n. Proof. intro n; apply gt_S; auto with arith. Qed. -(** Simplification and compatibility *) +(** * Simplification and compatibility *) Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. Proof. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index e95ef408..e8b9e6be 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,108 +6,124 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Le.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Le.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** Order on natural numbers. [le] is defined in [Init/Peano.v] as: +<< +Inductive le (n:nat) : nat -> Prop := + | le_n : n <= n + | le_S : forall m:nat, n <= m -> n <= S m + +where "n <= m" := (le n m) : nat_scope. +>> + *) -(** Order on natural numbers *) Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Reflexivity *) +(** * [le] is a pre-order *) +(** Reflexivity *) Theorem le_refl : forall n, n <= n. Proof. -exact le_n. + exact le_n. Qed. (** Transitivity *) - Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. Proof. induction 2; auto. Qed. Hint Resolve le_trans: arith v62. -(** Order, successor and predecessor *) +(** * Properties of [le] w.r.t. successor, predecessor and 0 *) -Theorem le_n_S : forall n m, n <= m -> S n <= S m. +(** Comparison to 0 *) + +Theorem le_O_n : forall n, 0 <= n. Proof. - induction 1; auto. + induction n; auto. Qed. -Theorem le_n_Sn : forall n, n <= S n. +Theorem le_Sn_O : forall n, ~ S n <= 0. Proof. - auto. + red in |- *; intros n H. + change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. Qed. -Theorem le_O_n : forall n, 0 <= n. +Hint Resolve le_O_n le_Sn_O: arith v62. + +Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. Proof. - induction n; auto. + induction n; auto with arith. + intro; contradiction le_Sn_O with n. Qed. +Hint Immediate le_n_O_eq: arith v62. -Hint Resolve le_n_S le_n_Sn le_O_n le_n_S: arith v62. -Theorem le_pred_n : forall n, pred n <= n. +(** [le] and successor *) + +Theorem le_n_S : forall n m, n <= m -> S n <= S m. Proof. -induction n; auto with arith. + induction 1; auto. Qed. -Hint Resolve le_pred_n: arith v62. + +Theorem le_n_Sn : forall n, n <= S n. +Proof. + auto. +Qed. + +Hint Resolve le_n_S le_n_Sn : arith v62. Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof. -intros n m H; apply le_trans with (S n); auto with arith. + intros n m H; apply le_trans with (S n); auto with arith. Qed. 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. + intros n m H; change (pred (S n) <= pred (S m)) in |- *. + 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. +Theorem le_Sn_n : forall n, ~ S n <= n. Proof. -destruct n; simpl; auto with arith. -destruct m; simpl; auto with arith. + induction n; auto with arith. Qed. +Hint Resolve le_Sn_n: arith v62. -(** Comparison to 0 *) +(** [le] and predecessor *) -Theorem le_Sn_O : forall n, ~ S n <= 0. +Theorem le_pred_n : forall n, pred n <= n. Proof. -red in |- *; intros n H. -change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. + induction n; auto with arith. Qed. -Hint Resolve le_Sn_O: arith v62. +Hint Resolve le_pred_n: arith v62. -Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. +Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. -induction n; auto with arith. -intro; contradiction le_Sn_O with n. + destruct n; simpl; auto with arith. + destruct m; simpl; auto with arith. Qed. -Hint Immediate le_n_O_eq: arith v62. -(** Negative properties *) - -Theorem le_Sn_n : forall n, ~ S n <= n. -Proof. -induction n; auto with arith. -Qed. -Hint Resolve le_Sn_n: arith v62. +(** * [le] is a order on [nat] *) (** Antisymmetry *) Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m. Proof. -intros n m h; destruct h as [| m0 H]; auto with arith. -intros H1. -absurd (S m0 <= m0); auto with arith. -apply le_trans with n; auto with arith. + intros n m H; destruct H as [|m' H]; auto with arith. + intros H1. + absurd (S m' <= m'); auto with arith. + apply le_trans with n; auto with arith. Qed. Hint Immediate le_antisym: arith v62. -(** A different elimination principle for the order on natural numbers *) + +(** * A different elimination principle for the order on natural numbers *) Lemma le_elim_rel : forall P:nat -> nat -> Prop, @@ -115,7 +131,7 @@ Lemma le_elim_rel : (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. Proof. -induction n; auto with arith. -intros m Le. -elim Le; auto with arith. -Qed.
\ No newline at end of file + induction n; auto with arith. + intros m Le. + elim Le; auto with arith. +Qed. diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index eeb4e35e..94cf3793 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,86 +6,93 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lt.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Lt.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: +<< +Definition lt (n m:nat) := S n <= m. +Infix "<" := lt : nat_scope. +>> +*) Require Import Le. Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Irreflexivity *) +(** * Irreflexivity *) Theorem lt_irrefl : forall n, ~ n < n. Proof le_Sn_n. Hint Resolve lt_irrefl: arith v62. -(** Relationship between [le] and [lt] *) +(** * Relationship between [le] and [lt] *) Theorem lt_le_S : forall n m, n < m -> S n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_le_S: arith v62. Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_n_Sm_le: arith v62. Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate le_lt_n_Sm: arith v62. Theorem le_not_lt : forall n m, n <= m -> ~ m < n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Theorem lt_not_le : forall n m, n < m -> ~ m <= n. Proof. -red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt). + red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt). Qed. Hint Immediate le_not_lt lt_not_le: arith v62. -(** Asymmetry *) +(** * Asymmetry *) Theorem lt_asym : forall n m, n < m -> ~ m < n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. -(** Order and successor *) +(** * Order and successor *) Theorem lt_n_Sn : forall n, n < S n. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_n_Sn: arith v62. Theorem lt_S : forall n m, n < m -> n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_S: arith v62. Theorem lt_n_S : forall n m, n < m -> S n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_n_S: arith v62. Theorem lt_S_n : forall n m, S n < S m -> n < m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_S_n: arith v62. Theorem lt_O_Sn : forall n, 0 < S n. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_O_Sn: arith v62. @@ -93,7 +100,7 @@ Theorem lt_n_O : forall n, ~ n < 0. Proof le_Sn_O. Hint Resolve lt_n_O: arith v62. -(** Predecessor *) +(** * Predecessor *) Lemma S_pred : forall n m, m < n -> n = S (pred n). Proof. @@ -111,65 +118,65 @@ destruct 1; simpl in |- *; auto with arith. Qed. Hint Resolve lt_pred_n_n: arith v62. -(** Transitivity properties *) +(** * Transitivity properties *) Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. -(** Large = strict or equal *) +(** * Large = strict or equal *) Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Theorem lt_le_weak : forall n m, n < m -> n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_le_weak: arith v62. -(** Dichotomy *) +(** * Dichotomy *) Theorem le_or_lt : forall n m, n <= m \/ m < n. Proof. -intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith. -induction 1; auto with arith. + intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith. + induction 1; auto with arith. Qed. Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n. Proof. -intros m n diff. -elim (le_or_lt n m); [ intro H'0 | auto with arith ]. -elim (le_lt_or_eq n m); auto with arith. -intro H'; elim diff; auto with arith. + intros m n diff. + elim (le_or_lt n m); [ intro H'0 | auto with arith ]. + elim (le_lt_or_eq n m); auto with arith. + intro H'; elim diff; auto with arith. Qed. -(** Comparison to 0 *) +(** * Comparison to 0 *) Theorem neq_O_lt : forall n, 0 <> n -> 0 < n. Proof. -induction n; auto with arith. -intros; absurd (0 = 0); trivial with arith. + induction n; auto with arith. + intros; absurd (0 = 0); trivial with arith. Qed. Hint Immediate neq_O_lt: arith v62. Theorem lt_O_neq : forall n, 0 < n -> 0 <> n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 7f5c1148..e0222e41 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Arith. @@ -14,66 +14,66 @@ Open Local Scope nat_scope. Implicit Types m n : nat. -(** maximum of two natural numbers *) +(** * maximum of two natural numbers *) Fixpoint max n m {struct n} : nat := match n, m with - | O, _ => m - | S n', O => n - | S n', S m' => S (max n' m') + | O, _ => m + | S n', O => n + | S n', S m' => S (max n' m') end. -(** Simplifications of [max] *) +(** * Simplifications of [max] *) Lemma max_SS : forall n m, S (max n m) = max (S n) (S m). Proof. -auto with arith. + auto with arith. Qed. Lemma max_comm : forall n m, max n m = max m n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. -(** [max] and [le] *) +(** * [max] and [le] *) Lemma max_l : forall n m, m <= n -> max n m = n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. Lemma max_r : forall n m, n <= m -> max n m = m. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. Lemma le_max_l : forall n m, n <= max n m. Proof. -induction n; intros; simpl in |- *; auto with arith. -elim m; intros; simpl in |- *; auto with arith. + induction n; intros; simpl in |- *; auto with arith. + elim m; intros; simpl in |- *; auto with arith. Qed. Lemma le_max_r : forall n m, m <= max n m. Proof. -induction n; simpl in |- *; auto with arith. -induction m; simpl in |- *; auto with arith. + induction n; simpl in |- *; auto with arith. + induction m; simpl in |- *; auto with arith. Qed. Hint Resolve max_r max_l le_max_l le_max_r: arith v62. -(** [max n m] is equal to [n] or [m] *) +(** * [max n m] is equal to [n] or [m] *) Lemma max_dec : forall n m, {max n m = n} + {max n m = m}. Proof. -induction n; induction m; simpl in |- *; auto with arith. -elim (IHn m); intro H; elim H; auto. + 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 -> 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. + 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 38351817..db14e74b 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,73 +6,73 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Min.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*) -Require Import Arith. +Require Import Le. Open Local Scope nat_scope. Implicit Types m n : nat. -(** minimum of two natural numbers *) +(** * minimum of two natural numbers *) Fixpoint min n m {struct n} : nat := match n, m with - | O, _ => 0 - | S n', O => 0 - | S n', S m' => S (min n' m') + | O, _ => 0 + | S n', O => 0 + | S n', S m' => S (min n' m') end. -(** Simplifications of [min] *) +(** * Simplifications of [min] *) Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). Proof. -auto with arith. + auto with arith. Qed. Lemma min_comm : forall n m, min n m = min m n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. -(** [min] and [le] *) +(** * [min] and [le] *) Lemma min_l : forall n m, n <= m -> min n m = n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. Lemma min_r : forall n m, m <= n -> min n m = m. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. Lemma le_min_l : forall n m, min n m <= n. Proof. -induction n; intros; simpl in |- *; auto with arith. -elim m; intros; simpl in |- *; auto with arith. + induction n; intros; simpl in |- *; auto with arith. + elim m; intros; simpl in |- *; auto with arith. Qed. Lemma le_min_r : forall n m, min n m <= m. Proof. -induction n; simpl in |- *; auto with arith. -induction m; simpl in |- *; auto with arith. + induction n; simpl in |- *; auto with arith. + induction m; simpl in |- *; auto with arith. Qed. Hint Resolve min_l min_r le_min_l le_min_r: arith v62. -(** [min n m] is equal to [n] or [m] *) +(** * [min n m] is equal to [n] or [m] *) Lemma min_dec : forall n m, {min n m = n} + {min n m = m}. Proof. -induction n; induction m; simpl in |- *; auto with arith. -elim (IHn m); intro H; elim H; auto. + 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 -> 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. + 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. Notation min_case2 := min_case (only parsing). diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index dfecd7cf..2380c2de 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,9 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Minus.v 8642 2006-03-17 10:09:02Z notin $ i*) - -(** Subtraction (difference between two natural numbers) *) +(*i $Id: Minus.v 9245 2006-10-17 12:53:34Z notin $ 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 + | S k, O => S k + | S k, S l => k - l + end +where "n - m" := (minus n m) : nat_scope. +>> +*) Require Import Lt. Require Import Le. @@ -17,36 +27,37 @@ Open Local Scope nat_scope. Implicit Types m n p : nat. -(** 0 is right neutral *) +(** * 0 is right neutral *) Lemma minus_n_O : forall n, n = n - 0. Proof. -induction n; simpl in |- *; auto with arith. + induction n; simpl in |- *; auto with arith. Qed. Hint Resolve minus_n_O: arith v62. -(** Permutation with successor *) +(** * Permutation with successor *) Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m. Proof. -intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *; - auto with arith. + intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *; + auto with arith. Qed. Hint Resolve minus_Sn_m: arith v62. Theorem pred_of_minus : forall n, pred n = n - 1. -intro x; induction x; simpl in |- *; auto with arith. +Proof. + intro x; induction x; simpl in |- *; auto with arith. Qed. -(** Diagonal *) +(** * Diagonal *) Lemma minus_n_n : forall n, 0 = n - n. Proof. -induction n; simpl in |- *; auto with arith. + induction n; simpl in |- *; auto with arith. Qed. Hint Resolve minus_n_n: arith v62. -(** Simplification *) +(** * Simplification *) Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). Proof. @@ -54,70 +65,71 @@ Proof. Qed. Hint Resolve minus_plus_simpl_l_reverse: arith v62. -(** Relation with plus *) +(** * Relation with plus *) Lemma plus_minus : forall n m p, n = m + p -> p = n - m. Proof. -intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *; - intros. -replace (n0 - 0) with n0; auto with arith. -absurd (0 = S (n0 + p)); auto with arith. -auto with arith. + intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *; + intros. + replace (n0 - 0) with n0; auto with arith. + absurd (0 = S (n0 + p)); auto with arith. + auto with arith. Qed. Hint Immediate plus_minus: arith v62. Lemma minus_plus : forall n m, n + m - n = m. -symmetry in |- *; auto with arith. + symmetry in |- *; auto with arith. Qed. Hint Resolve minus_plus: arith v62. Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n). Proof. -intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *; - auto with arith. + intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *; + auto with arith. Qed. Hint Resolve le_plus_minus: arith v62. Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m. Proof. -symmetry in |- *; auto with arith. + symmetry in |- *; auto with arith. Qed. Hint Resolve le_plus_minus_r: arith v62. -(** Relation with order *) +(** * Relation with order *) Theorem le_minus : forall n m, n - m <= n. 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 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 ]. 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. + 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. Qed. Hint Resolve lt_minus: arith v62. Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n. Proof. -intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; - auto with arith. -intros; absurd (0 < 0); trivial with arith. + intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; + auto with arith. + intros; absurd (0 < 0); trivial with arith. Qed. Hint Immediate lt_O_minus_lt: arith v62. Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0. -intros y x; pattern y, x in |- *; apply nat_double_ind; - [ simpl in |- *; trivial with arith - | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ] - | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3; - apply H2; apply le_n_S; assumption ]. -Qed.
\ No newline at end of file +Proof. + intros y x; pattern y, x in |- *; apply nat_double_ind; + [ simpl in |- *; trivial with arith + | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ] + | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3; + apply H2; apply le_n_S; assumption ]. +Qed. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 051f8645..2315e12c 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Mult.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Export Plus. Require Export Minus. @@ -17,86 +17,98 @@ Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Zero property *) +(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *) + +(** * [nat] is a semi-ring *) + +(** ** Zero property *) Lemma mult_0_r : forall n, n * 0 = 0. Proof. -intro; symmetry in |- *; apply mult_n_O. + intro; symmetry in |- *; apply mult_n_O. Qed. Lemma mult_0_l : forall n, 0 * n = 0. Proof. -reflexivity. + reflexivity. Qed. -(** Distributivity *) +(** ** 1 is neutral *) -Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. +Lemma mult_1_l : forall n, 1 * n = n. Proof. -intros; elim n; simpl in |- *; intros; auto with arith. -elim plus_assoc; elim H; auto with arith. + simpl in |- *; auto with arith. Qed. -Hint Resolve mult_plus_distr_r: arith v62. +Hint Resolve mult_1_l: arith v62. -Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. +Lemma mult_1_r : forall n, n * 1 = n. Proof. - induction n. trivial. - intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. + induction n; [ trivial | + simpl; rewrite IHn; reflexivity]. Qed. +Hint Resolve mult_1_r: arith v62. -Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. +(** ** Commutativity *) + +Lemma mult_comm : forall n m, n * m = m * n. Proof. -intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros; - auto with arith. -elim minus_plus_simpl_l_reverse; auto with arith. +intros; elim n; intros; simpl in |- *; auto with arith. +elim mult_n_Sm. +elim H; apply plus_comm. Qed. -Hint Resolve mult_minus_distr_r: arith v62. +Hint Resolve mult_comm: arith v62. -(** Associativity *) +(** ** Distributivity *) -Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). +Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. Proof. -intros; elim n; intros; simpl in |- *; auto with arith. -rewrite mult_plus_distr_r. -elim H; auto with arith. + intros; elim n; simpl in |- *; intros; auto with arith. + elim plus_assoc; elim H; auto with arith. Qed. -Hint Resolve mult_assoc_reverse: arith v62. +Hint Resolve mult_plus_distr_r: arith v62. -Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. +Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Proof. -auto with arith. + induction n. trivial. + intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. Qed. -Hint Resolve mult_assoc: arith v62. -(** Commutativity *) +Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. +Proof. + intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros; + auto with arith. + elim minus_plus_simpl_l_reverse; auto with arith. +Qed. +Hint Resolve mult_minus_distr_r: arith v62. -Lemma mult_comm : forall n m, n * m = m * n. +Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p. Proof. -intros; elim n; intros; simpl in |- *; auto with arith. -elim mult_n_Sm. -elim H; apply plus_comm. + intros n m p. rewrite mult_comm. rewrite mult_minus_distr_r. + rewrite (mult_comm m n); rewrite (mult_comm p n); reflexivity. Qed. -Hint Resolve mult_comm: arith v62. +Hint Resolve mult_minus_distr_l: arith v62. -(** 1 is neutral *) +(** ** Associativity *) -Lemma mult_1_l : forall n, 1 * n = n. +Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). Proof. -simpl in |- *; auto with arith. + intros; elim n; intros; simpl in |- *; auto with arith. + rewrite mult_plus_distr_r. + elim H; auto with arith. Qed. -Hint Resolve mult_1_l: arith v62. +Hint Resolve mult_assoc_reverse: arith v62. -Lemma mult_1_r : forall n, n * 1 = n. +Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. Proof. -intro; elim mult_comm; auto with arith. + auto with arith. Qed. -Hint Resolve mult_1_r: arith v62. +Hint Resolve mult_assoc: arith v62. -(** Compatibility with orders *) +(** * Compatibility with orders *) Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. Proof. -induction m; simpl in |- *; auto with arith. + induction m; simpl in |- *; auto with arith. Qed. Hint Resolve mult_O_le: arith v62. @@ -110,26 +122,27 @@ Hint Resolve mult_le_compat_l: arith. Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. -intros m n p H. -rewrite mult_comm. rewrite (mult_comm n). -auto with arith. +Proof. + intros m n p H. + rewrite mult_comm. rewrite (mult_comm n). + auto with arith. Qed. Lemma mult_le_compat : - forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. -Proof. -intros m n p q Hmn Hpq; induction Hmn. -induction Hpq. -(* m*p<=m*p *) -apply le_n. -(* m*p<=m*m0 -> m*p<=m*(S m0) *) -rewrite <- mult_n_Sm; apply le_trans with (m * m0). -assumption. -apply le_plus_l. -(* m*p<=m0*q -> m*p<=(S m0)*q *) -simpl in |- *; apply le_trans with (m0 * q). -assumption. -apply le_plus_r. + forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. +Proof. + intros m n p q Hmn Hpq; induction Hmn. + induction Hpq. + (* m*p<=m*p *) + apply le_n. + (* m*p<=m*m0 -> m*p<=m*(S m0) *) + rewrite <- mult_n_Sm; apply le_trans with (m * m0). + assumption. + apply le_plus_l. + (* m*p<=m0*q -> m*p<=(S m0)*q *) + simpl in |- *; apply le_trans with (m0 * q). + assumption. + apply le_plus_r. Qed. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. @@ -141,11 +154,12 @@ Qed. Hint Resolve mult_S_lt_compat_l: arith. Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. -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. +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. Qed. Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. @@ -156,27 +170,28 @@ Proof. apply mult_S_lt_compat_l. assumption. Qed. -(** n|->2*n and n|->2n+1 have disjoint image *) +(** * n|->2*n and n|->2n+1 have disjoint image *) Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. -intros p; elim p; auto. -intros q; case q; simpl in |- *. -red in |- *; intros; discriminate. -intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *; - intros; discriminate. -intros p' H q; case q. -simpl in |- *; red in |- *; intros; discriminate. -intros q'; red in |- *; intros H0; case (H q'). -replace (2 * q') with (2 * S q' - 2). -rewrite <- H0; simpl in |- *; auto. -repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. -simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; - auto. -case q'; simpl in |- *; auto. +Proof. + intros p; elim p; auto. + intros q; case q; simpl in |- *. + red in |- *; intros; discriminate. + intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *; + intros; discriminate. + intros p' H q; case q. + simpl in |- *; red in |- *; intros; discriminate. + intros q'; red in |- *; intros H0; case (H q'). + replace (2 * q') with (2 * S q' - 2). + rewrite <- H0; simpl in |- *; auto. + repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. + simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; + auto. + case q'; simpl in |- *; auto. Qed. -(** Tail-recursive mult *) +(** * Tail-recursive mult *) (** [tail_mult] is an alternative definition for [mult] which is tail-recursive, whereas [mult] is not. This can be useful @@ -184,23 +199,23 @@ Qed. Fixpoint mult_acc (s:nat) m n {struct n} : nat := match n with - | O => s - | S p => mult_acc (tail_plus m s) m p + | O => s + | S p => mult_acc (tail_plus m s) m p end. Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. -induction n as [| p IHp]; simpl in |- *; auto. -intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. -rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. -rewrite plus_comm; auto. + induction n as [| p IHp]; simpl in |- *; auto. + intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. + rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. + rewrite plus_comm; auto. Qed. Definition tail_mult n m := mult_acc 0 m n. Lemma mult_tail_mult : forall n m, n * m = tail_mult n m. Proof. -intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. + intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. Qed. (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] @@ -208,4 +223,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 |- *.
\ No newline at end of file diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 4aef7dc0..b17021bc 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Peano_dec.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Decidable. @@ -16,19 +16,19 @@ Implicit Types m n x y : nat. Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}. Proof. -induction n. -auto. -left; exists n; auto. + induction n. + auto. + left; exists n; auto. Defined. Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. Proof. -induction n; induction m; auto. -elim (IHn m); auto. + induction n; induction m; auto. + elim (IHn m); auto. Defined. 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. + intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith. Defined. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 56e1c58a..74d0dc93 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,9 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Plus.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Plus.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** Properties of addition *) +(** Properties of addition. [add] is defined in [Init/Peano.v] as: +<< +Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (p + m) + end +where "n + m" := (plus n m) : nat_scope. +>> + *) Require Import Le. Require Import Lt. @@ -17,126 +26,127 @@ Open Local Scope nat_scope. Implicit Types m n p q : nat. -(** Zero is neutral *) +(** * Zero is neutral *) Lemma plus_0_l : forall n, 0 + n = n. Proof. -reflexivity. + reflexivity. Qed. Lemma plus_0_r : forall n, n + 0 = n. Proof. -intro; symmetry in |- *; apply plus_n_O. + intro; symmetry in |- *; apply plus_n_O. Qed. -(** Commutativity *) +(** * Commutativity *) Lemma plus_comm : forall n m, n + m = m + n. Proof. -intros n m; elim n; simpl in |- *; auto with arith. -intros y H; elim (plus_n_Sm m y); auto with arith. + intros n m; elim n; simpl in |- *; auto with arith. + intros y H; elim (plus_n_Sm m y); auto with arith. Qed. Hint Immediate plus_comm: arith v62. -(** Associativity *) +(** * Associativity *) Lemma plus_Snm_nSm : forall n m, S n + m = n + S m. -intros. -simpl in |- *. -rewrite (plus_comm n m). -rewrite (plus_comm n (S m)). -trivial with arith. +Proof. + intros. + simpl in |- *. + rewrite (plus_comm n m). + rewrite (plus_comm n (S m)). + trivial with arith. Qed. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Proof. -intros n m p; elim n; simpl in |- *; auto with arith. + intros n m p; elim n; simpl in |- *; auto with arith. Qed. Hint Resolve plus_assoc: arith v62. Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p). Proof. -intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. + intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. Qed. Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p). Proof. -auto with arith. + auto with arith. Qed. Hint Resolve plus_assoc_reverse: arith v62. -(** Simplification *) +(** * Simplification *) Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m. Proof. -intros m p n; induction n; simpl in |- *; auto with arith. + intros m p n; induction n; simpl in |- *; auto with arith. Qed. Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m. Proof. -induction p; simpl in |- *; auto with arith. + induction p; simpl in |- *; auto with arith. Qed. Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m. Proof. -induction p; simpl in |- *; auto with arith. + induction p; simpl in |- *; auto with arith. Qed. -(** Compatibility with order *) +(** * Compatibility with order *) Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. Proof. -induction p; simpl in |- *; auto with arith. + induction p; simpl in |- *; auto with arith. Qed. Hint Resolve plus_le_compat_l: arith v62. Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p. Proof. -induction 1; simpl in |- *; auto with arith. + induction 1; simpl in |- *; auto with arith. Qed. Hint Resolve plus_le_compat_r: arith v62. Lemma le_plus_l : forall n m, n <= n + m. Proof. -induction n; simpl in |- *; auto with arith. + induction n; simpl in |- *; auto with arith. Qed. Hint Resolve le_plus_l: arith v62. Lemma le_plus_r : forall n m, m <= n + m. Proof. -intros n m; elim n; simpl in |- *; auto with arith. + intros n m; elim n; simpl in |- *; auto with arith. Qed. Hint Resolve le_plus_r: arith v62. Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p. Proof. -intros; apply le_trans with (m := m); auto with arith. + intros; apply le_trans with (m := m); auto with arith. Qed. Hint Resolve le_plus_trans: arith v62. Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. Proof. -intros; apply lt_le_trans with (m := m); auto with arith. + intros; apply lt_le_trans with (m := m); auto with arith. Qed. Hint Immediate lt_plus_trans: arith v62. Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. Proof. -induction p; simpl in |- *; auto with arith. + induction p; simpl in |- *; auto with arith. Qed. Hint Resolve plus_lt_compat_l: arith v62. Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. Proof. -intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p). -elim p; auto with arith. + intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p). + elim p; auto with arith. Qed. Hint Resolve plus_lt_compat_r: arith v62. Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. -intros n m p q H H0. -elim H; simpl in |- *; auto with arith. + intros n m p q H H0. + elim H; simpl in |- *; auto with arith. Qed. Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. @@ -156,7 +166,7 @@ Proof. apply lt_le_weak. assumption. Qed. -(** Inversion lemmas *) +(** * Inversion lemmas *) Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. Proof. @@ -173,7 +183,7 @@ Proof. simpl in H. discriminate H. Defined. -(** Derived properties *) +(** * Derived properties *) Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). Proof. @@ -182,7 +192,7 @@ Proof. rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. Qed. -(** Tail-recursive plus *) +(** * Tail-recursive plus *) (** [tail_plus] is an alternative definition for [plus] which is tail-recursive, whereas [plus] is not. This can be useful @@ -190,8 +200,8 @@ Qed. Fixpoint plus_acc q n {struct n} : nat := match n with - | O => q - | S p => plus_acc (S q) p + | O => q + | S p => plus_acc (S q) p end. Definition tail_plus n m := plus_acc m n. @@ -201,27 +211,27 @@ unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto. intro m; rewrite <- IHn; simpl in |- *; auto. Qed. -(** Discrimination *) +(** * 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. + 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). + 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). + 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). + intro n; exact (succ_plus_discr n 3). Qed. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index e1bbfad9..11fcd161 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 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Wf_nat.v 9341 2006-11-06 13:08:10Z notin $ i*) (** Well-founded relations and natural numbers *) @@ -18,7 +18,7 @@ Implicit Types m n p : nat. Section Well_founded_Nat. -Variable A : Set. +Variable A : Type. Variable f : A -> nat. Definition ltof (a b:A) := f a < f b. @@ -26,21 +26,21 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. -red in |- *. -cut (forall n (a:A), f a < n -> Acc ltof a). -intros H a; apply (H (S (f a))); auto with arith. -induction n. -intros; absurd (f a < 0); auto with arith. -intros a ltSma. -apply Acc_intro. -unfold ltof in |- *; intros b ltfafb. -apply IHn. -apply lt_le_trans with (f a); auto with arith. + red in |- *. + cut (forall n (a:A), f a < n -> Acc ltof a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply Acc_intro. + unfold ltof in |- *; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. Theorem well_founded_gtof : well_founded gtof. Proof. -exact well_founded_ltof. + exact well_founded_ltof. Defined. (** It is possible to directly prove the induction principle going @@ -48,52 +48,55 @@ Defined. or to use the previous lemmas to extract a program with a fixpoint ([induction_ltof2]) -the ML-like program for [induction_ltof1] is : [[ +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)));; ]] -the ML-like program for [induction_ltof2] is : [[ +the ML-like program for [induction_ltof2] is : +[[ let induction_ltof2 F a = indrec a where rec indrec a = F a indrec;; -]] *) +]] +*) Theorem induction_ltof1 : - forall P:A -> Set, - (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. -Proof. -intros P F; cut (forall n (a:A), f a < n -> P a). -intros H a; apply (H (S (f a))); auto with arith. -induction n. -intros; absurd (f a < 0); auto with arith. -intros a ltSma. -apply F. -unfold ltof in |- *; intros b ltfafb. -apply IHn. -apply lt_le_trans with (f a); auto with arith. + forall P:A -> Set, + (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. +Proof. + intros P F; cut (forall n (a:A), f a < n -> P a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply F. + unfold ltof in |- *; intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. Theorem induction_gtof1 : - forall P:A -> Set, - (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact induction_ltof1. + exact induction_ltof1. Defined. Theorem induction_ltof2 : - forall P:A -> Set, - (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact (well_founded_induction well_founded_ltof). + exact (well_founded_induction well_founded_ltof). Defined. Theorem induction_gtof2 : - forall P:A -> Set, - (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. + forall P:A -> Set, + (forall x:A, (forall y:A, gtof y x -> P y) -> P x) -> forall a:A, P a. Proof. -exact induction_ltof2. + exact induction_ltof2. Defined. (** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] @@ -105,105 +108,105 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. -red in |- *. -cut (forall n (a:A), f a < n -> Acc R a). -intros H a; apply (H (S (f a))); auto with arith. -induction n. -intros; absurd (f a < 0); auto with arith. -intros a ltSma. -apply Acc_intro. -intros b ltfafb. -apply IHn. -apply lt_le_trans with (f a); auto with arith. + red in |- *. + cut (forall n (a:A), f a < n -> Acc R a). + intros H a; apply (H (S (f a))); auto with arith. + induction n. + intros; absurd (f a < 0); auto with arith. + intros a ltSma. + apply Acc_intro. + intros b ltfafb. + apply IHn. + apply lt_le_trans with (f a); auto with arith. Defined. End Well_founded_Nat. Lemma lt_wf : well_founded lt. Proof. -exact (well_founded_ltof nat (fun m => m)). + 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. + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -exact (fun p P F => 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. + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. Proof. -exact (fun p P F => 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. + 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. + intro p; intros; elim (lt_wf p); auto with arith. Qed. Lemma gt_wf_rec : - forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. + forall n (P:nat -> Set), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof. -exact lt_wf_rec. + exact lt_wf_rec. Defined. Lemma gt_wf_ind : - forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n. + forall n (P:nat -> Prop), (forall n, (forall m, n > m -> P m) -> P n) -> P n. Proof lt_wf_ind. Lemma lt_wf_double_rec : forall P:nat -> nat -> Set, (forall n m, - (forall p q, p < n -> P p q) -> - (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. + (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. + 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. Lemma lt_wf_double_ind : - forall P:nat -> nat -> Prop, - (forall n m, + forall P:nat -> nat -> Prop, + (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. + 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. Hint Resolve lt_wf: arith. Hint Resolve well_founded_lt_compat: arith. Section LT_WF_REL. -Variable A : Set. -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). - -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. -Proof. -intros x [n fxn]; generalize dependent x. -pattern n in |- *; apply lt_wf_ind; intros. -constructor; 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. + Variable A : Set. + 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). + + 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. + Proof. + intros x [n fxn]; generalize dependent x. + pattern n in |- *; apply lt_wf_ind; intros. + constructor; 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. + 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. |