summaryrefslogtreecommitdiff
path: root/theories/Init/Peano.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init/Peano.v')
-rw-r--r--theories/Init/Peano.v139
1 files changed, 56 insertions, 83 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index ef2d9584..7a14ab39 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -26,21 +26,22 @@
Require Import Notations.
Require Import Datatypes.
Require Import Logic.
+Require Coq.Init.Nat.
Open Scope nat_scope.
Definition eq_S := f_equal S.
+Definition f_equal_nat := f_equal (A:=nat).
-Hint Resolve (f_equal S): v62.
-Hint Resolve (f_equal (A:=nat)): core.
+Hint Resolve eq_S: v62.
+Hint Resolve f_equal_nat: core.
(** The predecessor function *)
-Definition pred (n:nat) : nat := match n with
- | O => n
- | S u => u
- end.
-Hint Resolve (f_equal pred): v62.
+Notation pred := Nat.pred (compat "8.4").
+
+Definition f_equal_pred := f_equal pred.
+Hint Resolve f_equal_pred: v62.
Theorem pred_Sn : forall n:nat, n = pred (S n).
Proof.
@@ -80,16 +81,13 @@ Hint Resolve n_Sn: core.
(** Addition *)
-Fixpoint plus (n m:nat) : nat :=
- match n with
- | O => m
- | S p => S (p + m)
- end
-
-where "n + m" := (plus n m) : nat_scope.
+Notation plus := Nat.add (compat "8.4").
+Infix "+" := Nat.add : nat_scope.
-Hint Resolve (f_equal2 plus): v62.
-Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+Definition f_equal2_plus := f_equal2 plus.
+Hint Resolve f_equal2_plus: v62.
+Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat).
+Hint Resolve f_equal2_nat: core.
Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
@@ -99,7 +97,7 @@ Hint Resolve plus_n_O: core.
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.
- auto.
+ reflexivity.
Qed.
Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
@@ -110,7 +108,7 @@ Hint Resolve plus_n_Sm: core.
Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m).
Proof.
- auto.
+ reflexivity.
Qed.
(** Standard associated names *)
@@ -120,15 +118,11 @@ Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2").
(** Multiplication *)
-Fixpoint mult (n m:nat) : nat :=
- match n with
- | O => 0
- | S p => m + p * m
- end
-
-where "n * m" := (mult n m) : nat_scope.
+Notation mult := Nat.mul (compat "8.4").
+Infix "*" := Nat.mul : nat_scope.
-Hint Resolve (f_equal2 mult): core.
+Definition f_equal2_mult := f_equal2 mult.
+Hint Resolve f_equal2_mult: core.
Lemma mult_n_O : forall n:nat, 0 = n * 0.
Proof.
@@ -151,14 +145,8 @@ Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2").
(** Truncated subtraction: [m-n] is [0] if [n>=m] *)
-Fixpoint minus (n m:nat) : nat :=
- match n, m with
- | O, _ => n
- | S k, O => n
- | S k, S l => k - l
- end
-
-where "n - m" := (minus n m) : nat_scope.
+Notation minus := Nat.sub (compat "8.4").
+Infix "-" := Nat.sub : nat_scope.
(** Definition of the usual orders, the basic properties of [le] and [lt]
can be found in files Le and Lt *)
@@ -202,6 +190,16 @@ Proof.
intros n m. exact (le_pred (S n) (S m)).
Qed.
+Theorem le_0_n : forall n, 0 <= n.
+Proof.
+ induction n; constructor; trivial.
+Qed.
+
+Theorem le_n_S : forall n m, n <= m -> S n <= S m.
+Proof.
+ induction 1; constructor; trivial.
+Qed.
+
(** Case analysis *)
Theorem nat_case :
@@ -224,73 +222,48 @@ Qed.
(** Maximum and minimum : definitions and specifications *)
-Fixpoint max n m : nat :=
- match n, m with
- | O, _ => m
- | S n', O => n
- | S n', S m' => S (max n' m')
- end.
-
-Fixpoint min n m : nat :=
- match n, m with
- | O, _ => 0
- | S n', O => 0
- | S n', S m' => S (min n' m')
- end.
+Notation max := Nat.max (compat "8.4").
+Notation min := Nat.min (compat "8.4").
-Theorem max_l : forall n m : nat, m <= n -> max n m = n.
+Lemma max_l n m : m <= n -> Nat.max n m = n.
Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
Qed.
-Theorem max_r : forall n m : nat, n <= m -> max n m = m.
+Lemma max_r n m : n <= m -> Nat.max n m = m.
Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
Qed.
-Theorem min_l : forall n m : nat, n <= m -> min n m = n.
+Lemma min_l n m : n <= m -> Nat.min n m = n.
Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
Qed.
-Theorem min_r : forall n m : nat, m <= n -> min n m = m.
+Lemma min_r n m : m <= n -> Nat.min n m = m.
Proof.
-induction n; destruct m; simpl; auto. inversion 1.
-intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+ revert m; induction n; destruct m; simpl; trivial.
+ - inversion 1.
+ - intros. apply f_equal, IHn, le_S_n; trivial.
Qed.
-(** [n]th iteration of the function [f] *)
-Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A :=
- match n with
- | O => x
- | S n' => f (nat_iter n' f x)
- end.
-
-Lemma nat_iter_succ_r n {A} (f:A->A) (x:A) :
- nat_iter (S n) f x = nat_iter n f (f x).
+Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n :
+ nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
Proof.
induction n; intros; simpl; rewrite <- ?IHn; trivial.
Qed.
-Theorem nat_iter_plus :
+Theorem nat_rect_plus :
forall (n m:nat) {A} (f:A -> A) (x:A),
- nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
+ nat_rect (fun _ => A) x (fun _ => f) (n + m) =
+ nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n.
Proof.
induction n; intros; simpl; rewrite ?IHn; trivial.
Qed.
-
-(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv],
- then the iterates of [f] also preserve it. *)
-
-Theorem nat_iter_invariant :
- forall (n:nat) {A} (f:A -> A) (P : A -> Prop),
- (forall x, P x -> P (f x)) ->
- forall x, P x -> P (nat_iter n f x).
-Proof.
- induction n; simpl; trivial.
- intros A f P Hf x Hx. apply Hf, IHn; trivial.
-Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:43:18 +0000