diff options
Diffstat (limited to 'theories/Init/Peano.v')
-rw-r--r-- | theories/Init/Peano.v | 139 |
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. |