blob: 9f5ee7ee2fca458438ee0feb8bf5261f9b5ece62 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: EqNat.v,v 1.1.2.1 2004/07/16 19:31:24 herbelin Exp $ i*)
(** Equality on natural numbers *)
V7only [Import nat_scope.].
Open Local Scope nat_scope.
Implicit Variables Type m,n,x,y:nat.
Fixpoint eq_nat [n:nat] : nat -> Prop :=
[m:nat]Cases n m of
O O => True
| O (S _) => False
| (S _) O => False
| (S n1) (S m1) => (eq_nat n1 m1)
end.
Theorem eq_nat_refl : (n:nat)(eq_nat n n).
NewInduction n; Simpl; Auto.
Qed.
Hints Resolve eq_nat_refl : arith v62.
Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
NewInduction 1; Trivial with arith.
Qed.
Hints Immediate eq_eq_nat : arith v62.
Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
NewInduction n; NewInduction m; Simpl; Contradiction Orelse Auto with arith.
Qed.
Hints Immediate eq_nat_eq : arith v62.
Theorem eq_nat_elim : (n:nat)(P:nat->Prop)(P n)->(m:nat)(eq_nat n m)->(P m).
Intros; Replace m with n; Auto with arith.
Qed.
Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
NewInduction n.
NewDestruct m.
Auto with arith.
Intros; Right; Red; Trivial with arith.
NewDestruct m.
Right; Red; Auto with arith.
Intros.
Simpl.
Apply IHn.
Defined.
Fixpoint beq_nat [n:nat] : nat -> bool :=
[m:nat]Cases n m of
O O => true
| O (S _) => false
| (S _) O => false
| (S n1) (S m1) => (beq_nat n1 m1)
end.
Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
Proof.
Intro x; NewInduction x; Simpl; Auto.
Qed.
Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
Proof.
Double Induction x y; Simpl.
Reflexivity.
Intros; Discriminate H0.
Intros; Discriminate H0.
Intros; Case (H0 ? H1); Reflexivity.
Defined.
|
