diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Peano.v | 56 |
1 files changed, 30 insertions, 26 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 789a020f..c0416b63 100755..100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Peano.v 8642 2006-03-17 10:09:02Z notin $ i*) -(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *) +(** The type [nat] of Peano natural numbers (built from [O] and [S]) + is defined in [Datatypes.v] *) (** This module defines the following operations on natural numbers : - predecessor [pred] @@ -19,13 +20,15 @@ - greater or equal [ge] - greater [gt] - This module states various lemmas and theorems about natural numbers, - including Peano's axioms of arithmetic (in Coq, these are in fact provable) - Case analysis on [nat] and induction on [nat * nat] are provided too *) + It states various lemmas and theorems about natural numbers, + including Peano's axioms of arithmetic (in Coq, these are provable). + Case analysis on [nat] and induction on [nat * nat] are provided too + *) Require Import Notations. Require Import Datatypes. Require Import Logic. +Unset Boxed Definitions. Open Scope nat_scope. @@ -47,6 +50,8 @@ Proof. auto. Qed. +(** Injectivity of successor *) + Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. Proof. intros n m H; change (pred (S n) = pred (S m)) in |- *; auto. @@ -54,21 +59,20 @@ Qed. Hint Immediate eq_add_S: core v62. -(** A consequence of the previous axioms *) - Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. red in |- *; auto. Qed. Hint Resolve not_eq_S: core v62. +(** Zero is not the successor of a number *) + Definition IsSucc (n:nat) : Prop := match n with | O => False | S p => True end. - Theorem O_S : forall n:nat, 0 <> S n. Proof. red in |- *; intros n H. @@ -88,13 +92,14 @@ Hint Resolve n_Sn: core v62. Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m - | S p => S (plus p m) - end. + | S p => S (p + m) + end + +where "n + m" := (plus n m) : nat_scope. + Hint Resolve (f_equal2 plus): v62. Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. -Infix "+" := plus : nat_scope. - Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl in |- *; auto. @@ -122,11 +127,12 @@ Qed. Fixpoint mult (n m:nat) {struct n} : nat := match n with | O => 0 - | S p => m + mult p m - end. -Hint Resolve (f_equal2 mult): core v62. + | S p => m + p * m + end -Infix "*" := mult : nat_scope. +where "n * m" := (mult n m) : nat_scope. + +Hint Resolve (f_equal2 mult): core v62. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. @@ -142,27 +148,25 @@ Proof. Qed. Hint Resolve mult_n_Sm: core v62. -(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *) +(** Truncated subtraction: [m-n] is [0] if [n>=m] *) Fixpoint minus (n m:nat) {struct n} : nat := match n, m with | O, _ => 0 | S k, O => S k - | S k, S l => minus k l - end. + | S k, S l => k - l + end -Infix "-" := minus : nat_scope. +where "n - m" := (minus n m) : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] can be found in files Le and Lt *) -(** An inductive definition to define the order *) - Inductive le (n:nat) : nat -> Prop := - | le_n : le n n - | le_S : forall m:nat, le n m -> le n (S m). + | le_n : n <= n + | le_S : forall m:nat, n <= m -> n <= S m -Infix "<=" := le : nat_scope. +where "n <= m" := (le n m) : nat_scope. Hint Constructors le: core v62. (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) @@ -187,7 +191,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope. Notation "x < y < z" := (x < y /\ y < z) : nat_scope. Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope. -(** Pattern-Matching on natural numbers *) +(** Case analysis *) Theorem nat_case : forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. |