summaryrefslogtreecommitdiff
path: root/theories/Init/Peano.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/Init/Peano.v
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Init/Peano.v')
-rw-r--r--theories/Init/Peano.v38
1 files changed, 17 insertions, 21 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 9ef63cc8..43b1f634 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Peano.v 11115 2008-06-12 16:03:32Z werner $ i*)
+(*i $Id: Peano.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
(** The type [nat] of Peano natural numbers (built from [O] and [S])
is defined in [Datatypes.v] *)
@@ -47,7 +47,7 @@ Hint Resolve (f_equal pred): v62.
Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
- simpl; reflexivity.
+ simpl; reflexivity.
Qed.
(** Injectivity of successor *)
@@ -59,13 +59,13 @@ Proof.
rewrite Sn_eq_Sm; trivial.
Qed.
-Hint Immediate eq_add_S: core v62.
+Hint Immediate eq_add_S: core.
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.
+Hint Resolve not_eq_S: core.
Definition IsSucc (n:nat) : Prop :=
match n with
@@ -80,13 +80,13 @@ Proof.
unfold not; intros n H.
inversion H.
Qed.
-Hint Resolve O_S: core v62.
+Hint Resolve O_S: core.
Theorem n_Sn : forall n:nat, n <> S n.
Proof.
induction n; auto.
Qed.
-Hint Resolve n_Sn: core v62.
+Hint Resolve n_Sn: core.
(** Addition *)
@@ -105,7 +105,7 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl in |- *; auto.
Qed.
-Hint Resolve plus_n_O: core v62.
+Hint Resolve plus_n_O: core.
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.
@@ -116,7 +116,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
Proof.
intros n m; induction n; simpl in |- *; auto.
Qed.
-Hint Resolve plus_n_Sm: core v62.
+Hint Resolve plus_n_Sm: core.
Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
Proof.
@@ -138,13 +138,13 @@ Fixpoint mult (n m:nat) {struct n} : nat :=
where "n * m" := (mult n m) : nat_scope.
-Hint Resolve (f_equal2 mult): core v62.
+Hint Resolve (f_equal2 mult): core.
Lemma mult_n_O : forall n:nat, 0 = n * 0.
Proof.
induction n; simpl in |- *; auto.
Qed.
-Hint Resolve mult_n_O: core v62.
+Hint Resolve mult_n_O: core.
Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m.
Proof.
@@ -152,7 +152,7 @@ Proof.
destruct H; rewrite <- plus_n_Sm; apply (f_equal S).
pattern m at 1 3 in |- *; elim m; simpl in |- *; auto.
Qed.
-Hint Resolve mult_n_Sm: core v62.
+Hint Resolve mult_n_Sm: core.
(** Standard associated names *)
@@ -165,16 +165,12 @@ Fixpoint minus (n m:nat) {struct n} : nat :=
match n, m with
| O, _ => n
| S k, O => n
-(*=======
-
- | O, _ => n
- | S k, O => S k *)
| S k, S l => k - l
end
where "n - m" := (minus n m) : nat_scope.
-(** Definition of the usual orders, the basic properties of [le] and [lt]
+(** Definition of the usual orders, the basic properties of [le] and [lt]
can be found in files Le and Lt *)
Inductive le (n:nat) : nat -> Prop :=
@@ -183,21 +179,21 @@ Inductive le (n:nat) : nat -> Prop :=
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*)
+Hint Constructors le: core.
+(*i equivalent to : "Hints Resolve le_n le_S : core." i*)
Definition lt (n m:nat) := S n <= m.
-Hint Unfold lt: core v62.
+Hint Unfold lt: core.
Infix "<" := lt : nat_scope.
Definition ge (n m:nat) := m <= n.
-Hint Unfold ge: core v62.
+Hint Unfold ge: core.
Infix ">=" := ge : nat_scope.
Definition gt (n m:nat) := m < n.
-Hint Unfold gt: core v62.
+Hint Unfold gt: core.
Infix ">" := gt : nat_scope.