diff options
Diffstat (limited to 'theories/Init/Peano.v')
-rwxr-xr-x | theories/Init/Peano.v | 208 |
1 files changed, 100 insertions, 108 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 2356c9cb5..3506b9bab 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -23,196 +23,188 @@ 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 *) -Require Notations. -Require Datatypes. -Require Logic. +Require Import Notations. +Require Import Datatypes. +Require Import Logic. Open Scope nat_scope. -Definition eq_S := (f_equal nat nat S). +Definition eq_S := f_equal S. -Hint eq_S : v62 := Resolve (f_equal nat nat S). -Hint eq_nat_unary : core := Resolve (f_equal nat). +Hint Resolve (f_equal S): v62. +Hint Resolve (f_equal (A:=nat)): core. (** The predecessor function *) -Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end). -Hint eq_pred : v62 := Resolve (f_equal nat nat pred). +Definition pred (n:nat) : nat := match n with + | O => 0 + | S u => u + end. +Hint Resolve (f_equal pred): v62. -Theorem pred_Sn : (m:nat) m=(pred (S m)). +Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. - Auto. + auto. Qed. -Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m. +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)); Auto. + intros n m H; change (pred (S n) = pred (S m)) in |- *; auto. Qed. -Hints Immediate eq_add_S : core v62. +Hint Immediate eq_add_S: core v62. (** A consequence of the previous axioms *) -Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)). +Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. - Red; Auto. + red in |- *; auto. Qed. -Hints Resolve not_eq_S : core v62. +Hint Resolve not_eq_S: core v62. -Definition IsSucc : nat->Prop - := [n:nat]Cases n of O => False | (S p) => True end. +Definition IsSucc (n:nat) : Prop := + match n with + | O => False + | S p => True + end. -Theorem O_S : (n:nat)~(O=(S n)). +Theorem O_S : forall n:nat, 0 <> S n. Proof. - Red;Intros n H. - Change (IsSucc O). - Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption]. + red in |- *; intros n H. + change (IsSucc 0) in |- *. + rewrite <- (sym_eq (x:=0) (y:=(S n))); [ exact I | assumption ]. Qed. -Hints Resolve O_S : core v62. +Hint Resolve O_S: core v62. -Theorem n_Sn : (n:nat) ~(n=(S n)). +Theorem n_Sn : forall n:nat, n <> S n. Proof. - NewInduction n ; Auto. + induction n; auto. Qed. -Hints Resolve n_Sn : core v62. +Hint Resolve n_Sn: core v62. (** Addition *) -Fixpoint plus [n:nat] : nat -> nat := - [m:nat]Cases n of - O => m - | (S p) => (S (plus p m)) end. -Hint eq_plus : v62 := Resolve (f_equal2 nat nat nat plus). -Hint eq_nat_binary : core := Resolve (f_equal2 nat nat). +Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (plus p m) + end. +Hint Resolve (f_equal2 plus): v62. +Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. -V8Infix "+" plus : nat_scope. +Infix "+" := plus : nat_scope. -Lemma plus_n_O : (n:nat) n=(plus n O). +Lemma plus_n_O : forall n:nat, n = n + 0. Proof. - NewInduction n ; Simpl ; Auto. + induction n; simpl in |- *; auto. Qed. -Hints Resolve plus_n_O : core v62. +Hint Resolve plus_n_O: core v62. -Lemma plus_O_n : (n:nat) (plus O n)=n. +Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. - Auto. + auto. Qed. -Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)). +Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. - Intros n m; NewInduction n; Simpl; Auto. + intros n m; induction n; simpl in |- *; auto. Qed. -Hints Resolve plus_n_Sm : core v62. +Hint Resolve plus_n_Sm: core v62. -Lemma plus_Sn_m : (n,m:nat)(plus (S n) m)=(S (plus n m)). +Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. - Auto. + auto. Qed. (** Multiplication *) -Fixpoint mult [n:nat] : nat -> nat := - [m:nat]Cases n of O => O - | (S p) => (plus m (mult p m)) end. -Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult). +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. -V8Infix "*" mult : nat_scope. +Infix "*" := mult : nat_scope. -Lemma mult_n_O : (n:nat) O=(mult n O). +Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. - NewInduction n; Simpl; Auto. + induction n; simpl in |- *; auto. Qed. -Hints Resolve mult_n_O : core v62. +Hint Resolve mult_n_O: core v62. -Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)). +Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. - Intros; NewInduction n as [|p H]; Simpl; Auto. - NewDestruct H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S). - Pattern 1 3 m; Elim m; Simpl; Auto. + intros; induction n as [| p H]; simpl in |- *; auto. + destruct H; rewrite <- plus_n_Sm; apply (f_equal S). + pattern m at 1 3 in |- *; elim m; simpl in |- *; auto. Qed. -Hints Resolve mult_n_Sm : core v62. +Hint Resolve mult_n_Sm: core v62. (** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *) -Fixpoint minus [n:nat] : nat -> nat := - [m:nat]Cases n m of - O _ => O - | (S k) O => (S k) - | (S k) (S l) => (minus k l) - end. +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. -V8Infix "-" minus : nat_scope. +Infix "-" := minus : 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 : (m:nat)(le n m)->(le n (S m)). +Inductive le (n:nat) : nat -> Prop := + | le_n : le n n + | le_S : forall m:nat, le n m -> le n (S m). -V8Infix "<=" le : nat_scope. +Infix "<=" := le : nat_scope. -Hint constr_le : core v62 := Constructors le. +Hint Constructors le: core v62. (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) -Definition lt := [n,m:nat](le (S n) m). -Hints Unfold lt : core v62. +Definition lt (n m:nat) := S n <= m. +Hint Unfold lt: core v62. -V8Infix "<" lt : nat_scope. +Infix "<" := lt : nat_scope. -Definition ge := [n,m:nat](le m n). -Hints Unfold ge : core v62. +Definition ge (n m:nat) := m <= n. +Hint Unfold ge: core v62. -V8Infix ">=" ge : nat_scope. +Infix ">=" := ge : nat_scope. -Definition gt := [n,m:nat](lt m n). -Hints Unfold gt : core v62. +Definition gt (n m:nat) := m < n. +Hint Unfold gt: core v62. -V8Infix ">" gt : nat_scope. +Infix ">" := gt : nat_scope. -V8Notation "x <= y <= z" := (le x y)/\(le y z) : nat_scope. -V8Notation "x <= y < z" := (le x y)/\(lt y z) : nat_scope. -V8Notation "x < y < z" := (lt x y)/\(lt y z) : nat_scope. -V8Notation "x < y <= z" := (lt x y)/\(le y z) : nat_scope. +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. +Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope. (** Pattern-Matching on natural numbers *) -Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n). +Theorem nat_case : + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Proof. - NewInduction n ; Auto. + induction n; auto. Qed. (** Principle of double induction *) -Theorem nat_double_ind : (R:nat->nat->Prop) - ((n:nat)(R O n)) -> ((n:nat)(R (S n) O)) - -> ((n,m:nat)(R n m)->(R (S n) (S m))) - -> (n,m:nat)(R n m). +Theorem nat_double_ind : + forall R:nat -> nat -> Prop, + (forall n:nat, R 0 n) -> + (forall n:nat, R (S n) 0) -> + (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. Proof. - NewInduction n; Auto. - NewDestruct m; Auto. + induction n; auto. + destruct m as [| n0]; auto. Qed. (** Notations *) -V7only[ -Syntax constr - level 0: - S [ (S $p) ] -> [$p:"nat_printer":9] - | O [ O ] -> ["(0)"]. -]. - -V7only [ -(* For parsing/printing based on scopes *) -Module nat_scope. -Infix 4 "+" plus : nat_scope. -Infix 3 "*" mult : nat_scope. -Infix 4 "-" minus : nat_scope. -Infix NONA 5 "<=" le : nat_scope. -Infix NONA 5 "<" lt : nat_scope. -Infix NONA 5 ">=" ge : nat_scope. -Infix NONA 5 ">" gt : nat_scope. -End nat_scope. -]. |