diff options
Diffstat (limited to 'theories/Init/Peano.v')
| -rwxr-xr-x | theories/Init/Peano.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 5f6d2d8a8..55e44d28d 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -23,6 +23,7 @@ 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 Logic. Require LogicSyntax. Require Datatypes. @@ -65,13 +66,13 @@ Theorem O_S : (n:nat)~(O=(S n)). Proof. Red;Intros n H. Change (IsSucc O). - Elim (sym_eq nat O (S n));[Exact I | Assumption]. + Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption]. Qed. Hints Resolve O_S : core v62. Theorem n_Sn : (n:nat) ~(n=(S n)). Proof. - Induction n ; Auto. + NewInduction n ; Auto. Qed. Hints Resolve n_Sn : core v62. @@ -86,7 +87,7 @@ Hint eq_nat_binary : core := Resolve (f_equal2 nat nat). Lemma plus_n_O : (n:nat) n=(plus n O). Proof. - Induction n ; Simpl ; Auto. + NewInduction n ; Simpl ; Auto. Qed. Hints Resolve plus_n_O : core v62. @@ -97,7 +98,7 @@ Qed. Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)). Proof. - Intros m n; Elim m; Simpl; Auto. + Intros n m; NewInduction n; Simpl; Auto. Qed. Hints Resolve plus_n_Sm : core v62. @@ -115,14 +116,14 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult). Lemma mult_n_O : (n:nat) O=(mult n O). Proof. - Induction n; Simpl; Auto. + NewInduction n; Simpl; Auto. Qed. Hints Resolve mult_n_O : core v62. Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)). Proof. - Intros; Elim n; Simpl; Auto. - Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S). + 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. Qed. Hints Resolve mult_n_Sm : core v62. @@ -161,7 +162,7 @@ Hints Unfold gt : core v62. Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n). Proof. - Induction n ; Auto. + NewInduction n ; Auto. Qed. (** Principle of double induction *) @@ -171,8 +172,8 @@ Theorem nat_double_ind : (R:nat->nat->Prop) -> ((n,m:nat)(R n m)->(R (S n) (S m))) -> (n,m:nat)(R n m). Proof. - Induction n; Auto. - Induction m; Auto. + NewInduction n; Auto. + NewDestruct m; Auto. Qed. (** Notations *) |