diff options
Diffstat (limited to 'theories/Arith')
| -rwxr-xr-x | theories/Arith/Arith.v | 21 | ||||
| -rwxr-xr-x | theories/Arith/Between.v | 189 | ||||
| -rw-r--r-- | theories/Arith/Bool_nat.v | 39 | ||||
| -rwxr-xr-x | theories/Arith/Compare.v | 59 | ||||
| -rwxr-xr-x | theories/Arith/Compare_dec.v | 107 | ||||
| -rwxr-xr-x | theories/Arith/Div.v | 64 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 175 | ||||
| -rwxr-xr-x | theories/Arith/EqNat.v | 77 | ||||
| -rw-r--r-- | theories/Arith/Euclid.v | 68 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 305 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 50 | ||||
| -rwxr-xr-x | theories/Arith/Gt.v | 148 | ||||
| -rwxr-xr-x | theories/Arith/Le.v | 122 | ||||
| -rwxr-xr-x | theories/Arith/Lt.v | 175 | ||||
| -rwxr-xr-x | theories/Arith/Max.v | 85 | ||||
| -rwxr-xr-x | theories/Arith/Min.v | 83 | ||||
| -rwxr-xr-x | theories/Arith/Minus.v | 123 | ||||
| -rwxr-xr-x | theories/Arith/Mult.v | 211 | ||||
| -rwxr-xr-x | theories/Arith/Peano_dec.v | 34 | ||||
| -rwxr-xr-x | theories/Arith/Plus.v | 202 | ||||
| -rwxr-xr-x | theories/Arith/Wf_nat.v | 206 | ||||
| -rwxr-xr-x | theories/Arith/intro.tex | 55 |
22 files changed, 2598 insertions, 0 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v new file mode 100755 index 00000000..d44efb56 --- /dev/null +++ b/theories/Arith/Arith.v @@ -0,0 +1,21 @@ +(************************************************************************) +(* 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: Arith.v,v 1.11.2.1 2004/07/16 19:30:59 herbelin Exp $ i*) + +Require Export Le. +Require Export Lt. +Require Export Plus. +Require Export Gt. +Require Export Minus. +Require Export Mult. +Require Export Between. +Require Export Minus. +Require Export Peano_dec. +Require Export Compare_dec. +Require Export Factorial.
\ No newline at end of file diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v new file mode 100755 index 00000000..448ce002 --- /dev/null +++ b/theories/Arith/Between.v @@ -0,0 +1,189 @@ +(************************************************************************) +(* 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: Between.v,v 1.12.2.1 2004/07/16 19:30:59 herbelin Exp $ i*) + +Require Import Le. +Require Import Lt. + +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 : + forall k l (n:nat), + 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. + +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. + +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 diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v new file mode 100644 index 00000000..55dfd47f --- /dev/null +++ b/theories/Arith/Bool_nat.v @@ -0,0 +1,39 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: Bool_nat.v,v 1.5.2.1 2004/07/16 19:30:59 herbelin Exp $ *) + +Require Export Compare_dec. +Require Export Peano_dec. +Require Import Sumbool. + +Open Local Scope nat_scope. + +Implicit Types m n x y : nat. + +(** The decidability of equality and order relations over + type [nat] give some boolean functions with the adequate specification. *) + +Definition notzerop n := sumbool_not _ _ (zerop n). +Definition lt_ge_dec : forall x y, {x < y} + {x >= y} := + fun n m => sumbool_not _ _ (le_lt_dec m n). + +Definition nat_lt_ge_bool x y := bool_of_sumbool (lt_ge_dec x y). +Definition nat_ge_lt_bool x y := + bool_of_sumbool (sumbool_not _ _ (lt_ge_dec x y)). + +Definition nat_le_gt_bool x y := bool_of_sumbool (le_gt_dec x y). +Definition nat_gt_le_bool x y := + bool_of_sumbool (sumbool_not _ _ (le_gt_dec x y)). + +Definition nat_eq_bool x y := bool_of_sumbool (eq_nat_dec x y). +Definition nat_noteq_bool x y := + bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)). + +Definition zerop_bool x := bool_of_sumbool (zerop x). +Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v new file mode 100755 index 00000000..46827bae --- /dev/null +++ b/theories/Arith/Compare.v @@ -0,0 +1,59 @@ +(************************************************************************) +(* 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: Compare.v,v 1.12.2.1 2004/07/16 19:31:00 herbelin Exp $ 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 Peano_dec. +Require Import Compare_dec. + +Definition le_or_le_S := le_le_S_dec. + +Definition Pcompare := gt_eq_gt_dec. + +Lemma le_dec : forall n m, {n <= m} + {m <= n}. +Proof le_ge_dec. + +Definition lt_or_eq n m := {m > n} + {n = m}. + +Lemma le_decide : forall n m, n <= m -> lt_or_eq n m. +Proof le_lt_eq_dec. + +Lemma le_le_S_eq : forall n m, n <= m -> S n <= m \/ n = m. +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))). +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. +Qed. + +Require Export Wf_nat. + +Require Export Min. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v new file mode 100755 index 00000000..ea21437d --- /dev/null +++ b/theories/Arith/Compare_dec.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* 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: Compare_dec.v,v 1.13.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Le. +Require Import Lt. +Require Import Gt. +Require Import Decidable. + +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. +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. +Defined. + +Lemma gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}. +Proof lt_eq_lt_dec. + +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. +Defined. + +Definition le_le_S_dec : forall n m, {n <= m} + {S m <= n}. +Proof. +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. +Defined. + +Definition le_gt_dec : forall n m, {n <= m} + {n > m}. +Proof. +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. +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 ]. +Qed. + +Theorem dec_lt : forall n m, decidable (n < m). +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. +Qed. + +Theorem dec_ge : forall n m, decidable (n >= m). +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 ]. +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 ]. +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 ]. +Qed. + +Theorem not_ge : forall n m, ~ n >= m -> n < m. +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). +Qed. diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v new file mode 100755 index 00000000..adb5593d --- /dev/null +++ b/theories/Arith/Div.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Div.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Euclidean division *) + +V7only [Import nat_scope.]. +Open Local Scope nat_scope. + +Require Le. +Require Euclid_def. +Require Compare_dec. + +Implicit Variables Type n,a,b,q,r:nat. + +Fixpoint inf_dec [n:nat] : nat->bool := + [m:nat] Cases n m of + O _ => true + | (S n') O => false + | (S n') (S m') => (inf_dec n' m') + end. + +Theorem div1 : (b:nat)(gt b O)->(a:nat)(diveucl a b). +Realizer Fix div1 {div1/2: nat->nat->diveucl := + [b,a]Cases a of + O => (O,O) + | (S n) => + let (q,r) = (div1 b n) in + if (le_gt_dec b (S r)) then ((S q),O) + else (q,(S r)) + end}. +Program_all. +Rewrite e. +Replace b with (S r). +Simpl. +Elim plus_n_O; Auto with arith. +Apply le_antisym; Auto with arith. +Elim plus_n_Sm; Auto with arith. +Qed. + +Theorem div2 : (b:nat)(gt b O)->(a:nat)(diveucl a b). +Realizer Fix div1 {div1/2: nat->nat->diveucl := + [b,a]Cases a of + O => (O,O) + | (S n) => + let (q,r) = (div1 b n) in + if (inf_dec b (S r)) :: :: { {(le b (S r))}+{(gt b (S r))} } + then ((S q),O) + else (q,(S r)) + end}. +Program_all. +Rewrite e. +Replace b with (S r). +Simpl. +Elim plus_n_O; Auto with arith. +Apply le_antisym; Auto with arith. +Elim plus_n_Sm; Auto with arith. +Qed. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v new file mode 100644 index 00000000..c005f061 --- /dev/null +++ b/theories/Arith/Div2.v @@ -0,0 +1,175 @@ +(************************************************************************) +(* 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: Div2.v,v 1.15.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Lt. +Require Import Plus. +Require Import Compare_dec. +Require Import Even. + +Open Local Scope nat_scope. + +Implicit Type n : nat. + +(** Here we define [n/2] and prove some of its properties *) + +Fixpoint div2 n : nat := + match n with + | O => 0 + | S O => 0 + | S (S n') => S (div2 n') + end. + +(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is + 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. +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. +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. +Qed. + +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)). +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. +Qed. + +(** Specializations *) + +Lemma even_div2 : forall n, even n -> div2 n = div2 (S n). +Proof fun n => proj1 (proj1 (even_odd_div2 n)). + +Lemma div2_even : forall n, div2 n = div2 (S n) -> even n. +Proof fun n => proj2 (proj1 (even_odd_div2 n)). + +Lemma odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). +Proof fun n => proj1 (proj2 (even_odd_div2 n)). + +Lemma div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n. +Proof fun n => proj2 (proj2 (even_odd_div2 n)). + +Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. + +(** Properties related to the double ([2n]) *) + +Definition double n := n + n. + +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. +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. +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))). +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. +Qed. + + +(** Specializations *) + +Lemma even_double : forall n, even n -> n = double (div2 n). +Proof fun n => proj1 (proj1 (even_odd_double n)). + +Lemma double_even : forall n, n = double (div2 n) -> even n. +Proof fun n => proj2 (proj1 (even_odd_double n)). + +Lemma odd_double : forall n, odd n -> n = S (double (div2 n)). +Proof fun n => proj1 (proj2 (even_odd_double n)). + +Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n. +Proof fun n => proj2 (proj2 (even_odd_double n)). + +Hint Resolve even_double double_even odd_double double_odd: arith. + +(** Application: + - if [n] is even then there is a [p] such that [n = 2p] + - if [n] is odd then there is a [p] such that [n = 2p+1] + + (Immediate: it is [n/2]) *) + +Lemma even_2n : forall n, even n -> {p : nat | n = double p}. +Proof. +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. +Qed. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v new file mode 100755 index 00000000..2e99e068 --- /dev/null +++ b/theories/Arith/EqNat.v @@ -0,0 +1,77 @@ +(************************************************************************) +(* 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: EqNat.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Equality on natural numbers *) + +Open Local Scope nat_scope. + +Implicit Types m n x y : nat. + +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 + end. + +Theorem eq_nat_refl : forall n, eq_nat n n. +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. +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. +Qed. +Hint Immediate eq_nat_eq: arith v62. + +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. +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. +Defined. + +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 + end. + +Lemma beq_nat_refl : forall n, true = beq_nat n n. +Proof. + intro x; induction x; simpl in |- *; auto. +Qed. + +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. +Defined. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v new file mode 100644 index 00000000..e50e3d70 --- /dev/null +++ b/theories/Arith/Euclid.v @@ -0,0 +1,68 @@ +(************************************************************************) +(* 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: Euclid.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Mult. +Require Import Compare_dec. +Require Import Wf_nat. + +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. + + +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. +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. +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 diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v new file mode 100644 index 00000000..f7a2ad71 --- /dev/null +++ b/theories/Arith/Even.v @@ -0,0 +1,305 @@ +(************************************************************************) +(* 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: Even.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Here we define the predicates [even] and [odd] by mutual induction + and we prove the decidability and the exclusion of those predicates. + The main results about parity are proved in the module Div2. *) + +Open Local Scope nat_scope. + +Implicit Types m n : nat. + +Inductive even : nat -> Prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) +with odd : nat -> Prop := + odd_S : forall n, even n -> odd (S n). + +Hint Constructors even: arith. +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. +Qed. + +Lemma even_odd_dec : forall n, {even n} + {odd n}. +Proof. +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. +Qed. + +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). +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +Qed. +Hint Resolve odd_plus_l odd_plus_r: arith. + +Lemma even_mult_aux : + 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. +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. +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. +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. +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. +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. +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. +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. +Qed. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v new file mode 100644 index 00000000..4db211e4 --- /dev/null +++ b/theories/Arith/Factorial.v @@ -0,0 +1,50 @@ +(************************************************************************) +(* 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: Factorial.v,v 1.5.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Plus. +Require Import Mult. +Require Import Lt. +Open Local Scope nat_scope. + +(** Factorial *) + +Fixpoint fact (n:nat) : nat := + match n with + | 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. +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. +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. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v new file mode 100755 index 00000000..299c664d --- /dev/null +++ b/theories/Arith/Gt.v @@ -0,0 +1,148 @@ +(************************************************************************) +(* 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: Gt.v,v 1.8.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Le. +Require Import Lt. +Require Import Plus. +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +(** Order and successor *) + +Theorem gt_Sn_O : forall n, S n > 0. +Proof. + auto with arith. +Qed. +Hint Resolve gt_Sn_O: arith v62. + +Theorem gt_Sn_n : forall n, S n > n. +Proof. + auto with arith. +Qed. +Hint Resolve gt_Sn_n: arith v62. + +Theorem gt_n_S : forall n m, n > m -> S n > S m. +Proof. + auto with arith. +Qed. +Hint Resolve gt_n_S: arith v62. + +Lemma gt_S_n : forall n m, S m > S n -> m > n. +Proof. + auto with arith. +Qed. +Hint Immediate gt_S_n: arith v62. + +Theorem gt_S : forall n m, S n > m -> n > m \/ m = n. +Proof. + intros n m H; unfold gt in |- *; apply le_lt_or_eq; auto with arith. +Qed. + +Lemma gt_pred : forall n m, m > S n -> pred m > n. +Proof. + auto with arith. +Qed. +Hint Immediate gt_pred: arith v62. + +(** Irreflexivity *) + +Lemma gt_irrefl : forall n, ~ n > n. +Proof lt_irrefl. +Hint Resolve gt_irrefl: arith v62. + +(** 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 *) + +Lemma le_not_gt : forall n m, n <= m -> ~ n > m. +Proof le_not_lt. +Hint Resolve le_not_gt: arith v62. + +Lemma gt_not_le : forall n m, n > m -> ~ n <= m. +Proof. +auto with arith. +Qed. + +Hint Resolve gt_not_le: arith v62. + +Theorem le_S_gt : forall n m, S n <= m -> m > n. +Proof. + auto with arith. +Qed. +Hint Immediate le_S_gt: arith v62. + +Lemma gt_S_le : forall n m, S m > n -> n <= m. +Proof. + intros n p; exact (lt_n_Sm_le n p). +Qed. +Hint Immediate gt_S_le: arith v62. + +Lemma gt_le_S : forall n m, m > n -> S n <= m. +Proof. + auto with arith. +Qed. +Hint Resolve gt_le_S: arith v62. + +Lemma le_gt_S : forall n m, n <= m -> S m > n. +Proof. + auto with arith. +Qed. +Hint Resolve le_gt_S: arith v62. + +(** Transitivity *) + +Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. +Proof. + red in |- *; intros; apply lt_le_trans with m; auto with arith. +Qed. + +Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p. +Proof. + red in |- *; intros; apply le_lt_trans with m; auto with arith. +Qed. + +Lemma gt_trans : forall n m p, n > m -> m > p -> n > p. +Proof. + red in |- *; intros n m p H1 H2. + apply lt_trans with m; auto with arith. +Qed. + +Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p. +Proof. + red in |- *; intros; apply lt_le_trans with m; auto with arith. +Qed. + +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. + +(** 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 *) + +Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. +Proof. + red in |- *; intros n m p H; apply plus_lt_reg_l with p; auto with arith. +Qed. + +Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m. +Proof. + auto with arith. +Qed. +Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v new file mode 100755 index 00000000..a5378cff --- /dev/null +++ b/theories/Arith/Le.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* 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: Le.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Order on natural numbers *) +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +(** Reflexivity *) + +Theorem le_refl : forall n, n <= n. +Proof. +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 *) + +Theorem le_n_S : forall n m, n <= m -> S n <= S m. +Proof. + induction 1; auto. +Qed. + +Theorem le_n_Sn : forall n, n <= S n. +Proof. + auto. +Qed. + +Theorem le_O_n : forall n, 0 <= n. +Proof. + induction n; auto. +Qed. + +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. +Proof. +induction n; auto with arith. +Qed. +Hint Resolve le_pred_n: 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. +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 |- *. +elim H; simpl in |- *; auto with arith. +Qed. +Hint Immediate le_S_n: arith v62. + +Theorem le_pred : forall n m, n <= m -> pred n <= pred m. +Proof. +induction n as [| n IHn]. simpl in |- *. auto with arith. +destruct m as [| m]. simpl in |- *. intro H. inversion H. +simpl in |- *. auto with arith. +Qed. + +(** Comparison to 0 *) + +Theorem le_Sn_O : forall n, ~ S n <= 0. +Proof. +red in |- *; intros n H. +change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. +Qed. +Hint Resolve le_Sn_O: arith v62. + +Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. +Proof. +induction n; auto with arith. +intro; contradiction le_Sn_O with n. +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. + +(** 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. +Qed. +Hint Immediate le_antisym: arith v62. + +(** A different elimination principle for the order on natural numbers *) + +Lemma le_elim_rel : + forall P:nat -> nat -> Prop, + (forall p, P 0 p) -> + (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 diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v new file mode 100755 index 00000000..e1b3e4b8 --- /dev/null +++ b/theories/Arith/Lt.v @@ -0,0 +1,175 @@ +(************************************************************************) +(* 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: Lt.v,v 1.11.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Le. +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +(** Irreflexivity *) + +Theorem lt_irrefl : forall n, ~ n < n. +Proof le_Sn_n. +Hint Resolve lt_irrefl: arith v62. + +(** Relationship between [le] and [lt] *) + +Theorem lt_le_S : forall n m, n < m -> S n <= m. +Proof. +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. +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. +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. +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). +Qed. +Hint Immediate le_not_lt lt_not_le: arith v62. + +(** Asymmetry *) + +Theorem lt_asym : forall n m, n < m -> ~ m < n. +Proof. +induction 1; auto with arith. +Qed. + +(** Order and successor *) + +Theorem lt_n_Sn : forall n, n < S n. +Proof. +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. +Qed. +Hint Resolve lt_S: arith v62. + +Theorem lt_n_S : forall n m, n < m -> S n < S m. +Proof. +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. +Qed. +Hint Immediate lt_S_n: arith v62. + +Theorem lt_O_Sn : forall n, 0 < S n. +Proof. +auto with arith. +Qed. +Hint Resolve lt_O_Sn: arith v62. + +Theorem lt_n_O : forall n, ~ n < 0. +Proof le_Sn_O. +Hint Resolve lt_n_O: arith v62. + +(** Predecessor *) + +Lemma S_pred : forall n m, m < n -> n = S (pred n). +Proof. +induction 1; auto with arith. +Qed. + +Lemma lt_pred : forall n m, S n < m -> n < pred m. +Proof. +induction 1; simpl in |- *; auto with arith. +Qed. +Hint Immediate lt_pred: arith v62. + +Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n. +destruct 1; simpl in |- *; auto with arith. +Qed. +Hint Resolve lt_pred_n_n: arith v62. + +(** Transitivity properties *) + +Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. +Proof. +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. +Qed. + +Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. +Proof. +induction 2; auto with arith. +Qed. + +Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. + +(** Large = strict or equal *) + +Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. +Proof. +induction 1; auto with arith. +Qed. + +Theorem lt_le_weak : forall n m, n < m -> n <= m. +Proof. +auto with arith. +Qed. +Hint Immediate lt_le_weak: arith v62. + +(** 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. +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. +Qed. + +(** 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. +Qed. +Hint Immediate neq_O_lt: arith v62. + +Theorem lt_O_neq : forall n, 0 < n -> 0 <> n. +Proof. +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 new file mode 100755 index 00000000..82673ed0 --- /dev/null +++ b/theories/Arith/Max.v @@ -0,0 +1,85 @@ +(************************************************************************) +(* 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: Max.v,v 1.7.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Arith. + +Open Local Scope nat_scope. + +Implicit Types m n : nat. + +(** 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') + end. + +(** Simplifications of [max] *) + +Lemma max_SS : forall n m, S (max n m) = max (S n) (S m). +Proof. +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. +Qed. + +(** [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. +Qed. + +Lemma max_r : forall n m, n <= m -> max n m = m. +Proof. +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. +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. +Qed. +Hint Resolve max_r max_l le_max_l le_max_r: arith v62. + + +(** [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. +Qed. + +Lemma max_case : forall n m (P:nat -> Set), P n -> P m -> P (max n m). +Proof. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (max n m) in |- *; apply IHn; auto with arith. +Qed. + +Lemma max_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (max n m). +Proof. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (max n m) in |- *; apply IHn; auto with arith. +Qed. + diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v new file mode 100755 index 00000000..912e7ba3 --- /dev/null +++ b/theories/Arith/Min.v @@ -0,0 +1,83 @@ +(************************************************************************) +(* 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: Min.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Arith. + +Open Local Scope nat_scope. + +Implicit Types m n : nat. + +(** 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') + end. + +(** Simplifications of [min] *) + +Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). +Proof. +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. +Qed. + +(** [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. +Qed. + +Lemma min_r : forall n m, m <= n -> min n m = m. +Proof. +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. +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. +Qed. +Hint Resolve min_l min_r le_min_l le_min_r: arith v62. + +(** [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. +Qed. + +Lemma min_case : forall n m (P:nat -> Set), P n -> P m -> P (min n m). +Proof. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (min n m) in |- *; apply IHn; auto with arith. +Qed. + +Lemma min_case2 : forall n m (P:nat -> Prop), P n -> P m -> P (min n m). +Proof. +induction n; simpl in |- *; auto with arith. +induction m; intros; simpl in |- *; auto with arith. +pattern (min n m) in |- *; apply IHn; auto with arith. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v new file mode 100755 index 00000000..ba9a46ad --- /dev/null +++ b/theories/Arith/Minus.v @@ -0,0 +1,123 @@ +(************************************************************************) +(* 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: Minus.v,v 1.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Subtraction (difference between two natural numbers) *) + +Require Import Lt. +Require Import Le. + +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +(** 0 is right neutral *) + +Lemma minus_n_O : forall n, n = n - 0. +Proof. +induction n; simpl in |- *; auto with arith. +Qed. +Hint Resolve minus_n_O: arith v62. + +(** 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. +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. +Qed. + +(** Diagonal *) + +Lemma minus_n_n : forall n, 0 = n - n. +Proof. +induction n; simpl in |- *; auto with arith. +Qed. +Hint Resolve minus_n_n: arith v62. + +(** Simplification *) + +Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). +Proof. + induction p; simpl in |- *; auto with arith. +Qed. +Hint Resolve minus_plus_simpl_l_reverse: arith v62. + +(** 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. +Qed. +Hint Immediate plus_minus: arith v62. + +Lemma minus_plus : forall n m, n + m - n = m. +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. +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. +Qed. +Hint Resolve le_plus_minus_r: arith v62. + +(** 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 ]. +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. +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. +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 diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v new file mode 100755 index 00000000..abfade57 --- /dev/null +++ b/theories/Arith/Mult.v @@ -0,0 +1,211 @@ +(************************************************************************) +(* 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: Mult.v,v 1.21.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Export Plus. +Require Export Minus. +Require Export Lt. +Require Export Le. + +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +(** Zero property *) + +Lemma mult_0_r : forall n, n * 0 = 0. +Proof. +intro; symmetry in |- *; apply mult_n_O. +Qed. + +Lemma mult_0_l : forall n, 0 * n = 0. +Proof. +reflexivity. +Qed. + +(** Distributivity *) + +Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. +Proof. +intros; elim n; simpl in |- *; intros; auto with arith. +elim plus_assoc; elim H; auto with arith. +Qed. +Hint Resolve mult_plus_distr_r: arith v62. + +Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. +Proof. + induction n. trivial. + intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. +Qed. + +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. + +(** Associativity *) + +Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). +Proof. +intros; elim n; intros; simpl in |- *; auto with arith. +rewrite mult_plus_distr_r. +elim H; auto with arith. +Qed. +Hint Resolve mult_assoc_reverse: arith v62. + +Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. +Proof. +auto with arith. +Qed. +Hint Resolve mult_assoc: arith v62. + +(** Commutativity *) + +Lemma mult_comm : forall n m, n * m = m * n. +Proof. +intros; elim n; intros; simpl in |- *; auto with arith. +elim mult_n_Sm. +elim H; apply plus_comm. +Qed. +Hint Resolve mult_comm: arith v62. + +(** 1 is neutral *) + +Lemma mult_1_l : forall n, 1 * n = n. +Proof. +simpl in |- *; auto with arith. +Qed. +Hint Resolve mult_1_l: arith v62. + +Lemma mult_1_r : forall n, n * 1 = n. +Proof. +intro; elim mult_comm; auto with arith. +Qed. +Hint Resolve mult_1_r: arith v62. + +(** Compatibility with orders *) + +Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. +Proof. +induction m; simpl in |- *; auto with arith. +Qed. +Hint Resolve mult_O_le: arith v62. + +Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. +Proof. + induction p as [| p IHp]. intros. simpl in |- *. apply le_n. + intros. simpl in |- *. apply plus_le_compat. assumption. + apply IHp. assumption. +Qed. +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. +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. +Qed. + +Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. +Proof. + intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption. + intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)). +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. +Qed. + +Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. +Proof. + intros m n p H. elim (le_or_lt n p). trivial. + intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1). + apply le_lt_trans with (m := S m * p). assumption. + apply mult_S_lt_compat_l. assumption. +Qed. + +(** 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. +Qed. + + +(** Tail-recursive mult *) + +(** [tail_mult] is an alternative definition for [mult] which is + tail-recursive, whereas [mult] is not. This can be useful + when extracting programs. *) + +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 + 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. +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. +Qed. + +(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] + and [mult] and simplify *) + +Ltac tail_simpl := + repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult; + simpl in |- *.
\ No newline at end of file diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v new file mode 100755 index 00000000..01204ee6 --- /dev/null +++ b/theories/Arith/Peano_dec.v @@ -0,0 +1,34 @@ +(************************************************************************) +(* 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: Peano_dec.v,v 1.10.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +Require Import Decidable. + +Open Local Scope nat_scope. + +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. +Defined. + +Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. +Proof. +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. +Defined. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v new file mode 100755 index 00000000..e4ac631e --- /dev/null +++ b/theories/Arith/Plus.v @@ -0,0 +1,202 @@ +(************************************************************************) +(* 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: Plus.v,v 1.18.2.1 2004/07/16 19:31:00 herbelin Exp $ i*) + +(** Properties of addition *) + +Require Import Le. +Require Import Lt. + +Open Local Scope nat_scope. + +Implicit Types m n p q : nat. + +(** Zero is neutral *) + +Lemma plus_0_l : forall n, 0 + n = n. +Proof. +reflexivity. +Qed. + +Lemma plus_0_r : forall n, n + 0 = n. +Proof. +intro; symmetry in |- *; apply plus_n_O. +Qed. + +(** 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. +Qed. +Hint Immediate plus_comm: arith v62. + +(** 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. +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. +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. +Qed. + +Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p). +Proof. +auto with arith. +Qed. +Hint Resolve plus_assoc_reverse: arith v62. + +(** 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. +Qed. + +Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m. +Proof. +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. +Qed. + +(** 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. +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. +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. +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. +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. +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. +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. +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. +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. +Qed. + +Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. +Proof. + unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm. + apply plus_le_compat; assumption. +Qed. + +Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. +Proof. + unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption. +Qed. + +Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. +Proof. + intros. apply plus_lt_le_compat. assumption. + apply lt_le_weak. assumption. +Qed. + +(** Inversion lemmas *) + +Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. +Proof. + intro m; destruct m as [| n]; auto. + intros. discriminate H. +Qed. + +Definition plus_is_one : + forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. +Proof. + intro m; destruct m as [| n]; auto. + destruct n; auto. + intros. + simpl in H. discriminate H. +Defined. + +(** Derived properties *) + +Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). +Proof. + intros m n p q. + rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q). + rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. +Qed. + +(** Tail-recursive plus *) + +(** [tail_plus] is an alternative definition for [plus] which is + tail-recursive, whereas [plus] is not. This can be useful + when extracting programs. *) + +Fixpoint plus_acc q n {struct n} : nat := + match n with + | O => q + | S p => plus_acc (S q) p + end. + +Definition tail_plus n m := plus_acc m n. + +Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. +unfold tail_plus in |- *; induction n as [| n IHn]; simpl in |- *; auto. +intro m; rewrite <- IHn; simpl in |- *; auto. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v new file mode 100755 index 00000000..8bf237b5 --- /dev/null +++ b/theories/Arith/Wf_nat.v @@ -0,0 +1,206 @@ +(************************************************************************) +(* 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: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*) + +(** Well-founded relations and natural numbers *) + +Require Import Lt. + +Open Local Scope nat_scope. + +Implicit Types m n p : nat. + +Section Well_founded_Nat. + +Variable A : Set. + +Variable f : A -> nat. +Definition ltof (a b:A) := f a < f b. +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. +Qed. + +Theorem well_founded_gtof : well_founded gtof. +Proof well_founded_ltof. + +(** It is possible to directly prove the induction principle going + back to primitive recursion on natural numbers ([induction_ltof1]) + or to use the previous lemmas to extract a program with a fixpoint + ([induction_ltof2]) + +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 : [[ + 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. +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. +Proof. +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. +Proof. +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. +Proof. +exact induction_ltof2. +Defined. + +(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)] + then [R] is well-founded. *) + +Variable R : A -> A -> Prop. + +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. +Qed. + +End Well_founded_Nat. + +Lemma lt_wf : well_founded lt. +Proof well_founded_ltof nat (fun m => m). + +Lemma lt_wf_rec1 : + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. +Proof. +exact + (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => + induction_ltof1 nat (fun m => m) P F p). +Defined. + +Lemma lt_wf_rec : + forall n (P:nat -> Set), (forall n, (forall m, m < n -> P m) -> P n) -> P n. +Proof. +exact + (fun p (P:nat -> Set) (F:forall n, (forall m, m < n -> P m) -> P n) => + induction_ltof2 nat (fun m => m) P F p). +Defined. + +Lemma lt_wf_ind : + forall n (P:nat -> Prop), (forall n, (forall m, m < n -> P m) -> P n) -> P n. +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. +Proof. +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. +Proof lt_wf_ind. + +Lemma lt_wf_double_rec : + forall P:nat -> nat -> Set, + (forall n m, + (forall p (q:nat), p < n -> P p q) -> + (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. +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 (q:nat), p < n -> P p q) -> + (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m. +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. +intros x [n fxn]; generalize x fxn; clear x fxn. +pattern n in |- *; apply lt_wf_ind; intros. +constructor; intros. +case (F_compat y x); trivial; intros. +apply (H x0); auto. +Qed. + +Theorem well_founded_inv_lt_rel_compat : well_founded R. +constructor; intros. +case (F_compat y a); trivial; intros. +apply acc_lt_rel; trivial. +exists x; trivial. +Qed. + + +End LT_WF_REL. + +Lemma well_founded_inv_rel_inv_lt_rel : + forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. +Qed.
\ No newline at end of file diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex new file mode 100755 index 00000000..655de34c --- /dev/null +++ b/theories/Arith/intro.tex @@ -0,0 +1,55 @@ +\section{Arith}\label{Arith} + +The {\tt Arith} library deals with various arithmetical notions and +their properties. + +\subsection*{Standard {\tt Arith} library} + +The following files are automatically loaded by {\tt Require Arith}. + +\begin{itemize} + +\item {\tt Le.v} states and proves properties of the large order {\tt le}. + +\item {\tt Lt.v} states and proves properties of the strict order {\tt +lt} (especially, the relationship with {\tt le}). + +\item {\tt Plus.v} states and proves properties on the addition. + +\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. + +\item {\tt Minus.v} defines the difference on +{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is +{\tt O} if {\tt n} $<$ {\tt p}. + +\item {\tt Mult.v} states and proves properties on the multiplication. + +\item {\tt Between.v} defines modalities on {\tt nat} and proves properties +of them. + +\end{itemize} + +\subsection*{Additional {\tt Arith} library} + +\begin{itemize} + +\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state +and prove various decidability results on {\tt nat}. + +\item {\tt Wf\_nat.v} states and proves various induction and recursion +principles on {\tt nat}. Especially, recursion for objects measurable by +a natural number and recursion on {\tt nat * nat} are provided. + +\item {\tt Min.v} defines the minimum of two natural numbers and proves +properties of it. + +\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows +the equivalence with Leibniz' equality. + +\item {\tt Euclid.v} proves that the euclidean +division specification is realisable. Conversely, {\tt Div.v} exhibits +two different algorithms and semi-automatically reconstruct the proof of +their correctness. These files emphasize the extraction of program vs +reconstruction of proofs paradigm. + +\end{itemize} |