1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: EqNat.v 9966 2007-07-10 23:54:53Z letouzey $ i*)
11
(** Equality on natural numbers *)
13
Open Local Scope nat_scope.
15
Implicit Types m n x y : nat.
17
(** * Propositional equality *)
19
Fixpoint eq_nat n m {struct n} : Prop :=
24
| S n1, S m1 => eq_nat n1 m1
27
Theorem eq_nat_refl : forall n, eq_nat n n.
28
induction n; simpl in |- *; auto.
30
Hint Resolve eq_nat_refl: arith v62.
32
(** [eq] restricted to [nat] and [eq_nat] are equivalent *)
34
Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m.
35
induction 1; trivial with arith.
37
Hint Immediate eq_eq_nat: arith v62.
39
Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m.
40
induction n; induction m; simpl in |- *; contradiction || auto with arith.
42
Hint Immediate eq_nat_eq: arith v62.
44
Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m.
46
split; auto with arith.
50
forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
52
intros; replace m with n; auto with arith.
55
Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
60
intros; right; red in |- *; trivial with arith.
62
right; red in |- *; auto with arith.
69
(** * Boolean equality on [nat] *)
71
Fixpoint beq_nat n m {struct n} : bool :=
76
| S n1, S m1 => beq_nat n1 m1
79
Lemma beq_nat_refl : forall n, true = beq_nat n n.
81
intro x; induction x; simpl in |- *; auto.
84
Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
86
double induction x y; simpl in |- *.
88
intros n H1 H2. discriminate H2.
89
intros n H1 H2. discriminate H2.
90
intros n H1 z H2 H3. case (H2 _ H3). reflexivity.
93
Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y.
95
induction x; destruct y; simpl; auto; intros; discriminate.
98
Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y.
100
induction x; destruct y; simpl; auto; intros; discriminate.