summaryrefslogtreecommitdiff
path: root/theories/Arith/EqNat.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Arith/EqNat.v
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Arith/EqNat.v')
-rwxr-xr-xtheories/Arith/EqNat.v77
1 files changed, 77 insertions, 0 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
new file mode 100755
index 00000000..2e99e068
--- /dev/null
+++ b/theories/Arith/EqNat.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(* 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.14.2.1 2004/07/16 19:31:00 herbelin Exp $ i*)
+
+(** Equality on natural numbers *)
+
+Open Local Scope nat_scope.
+
+Implicit Types m n x y : nat.
+
+Fixpoint eq_nat n m {struct n} : Prop :=
+ match n, m with
+ | O, O => True
+ | O, S _ => False
+ | S _, O => False
+ | S n1, S m1 => eq_nat n1 m1
+ end.
+
+Theorem eq_nat_refl : forall n, eq_nat n n.
+induction n; simpl in |- *; auto.
+Qed.
+Hint Resolve eq_nat_refl: arith v62.
+
+Theorem eq_eq_nat : forall n m, n = m -> eq_nat n m.
+induction 1; trivial with arith.
+Qed.
+Hint Immediate eq_eq_nat: arith v62.
+
+Theorem eq_nat_eq : forall n m, eq_nat n m -> n = m.
+induction n; induction m; simpl in |- *; contradiction || auto with arith.
+Qed.
+Hint Immediate eq_nat_eq: arith v62.
+
+Theorem eq_nat_elim :
+ forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
+intros; replace m with n; auto with arith.
+Qed.
+
+Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
+induction n.
+destruct m as [| n].
+auto with arith.
+intros; right; red in |- *; trivial with arith.
+destruct m as [| n0].
+right; red in |- *; auto with arith.
+intros.
+simpl in |- *.
+apply IHn.
+Defined.
+
+Fixpoint beq_nat n m {struct n} : bool :=
+ match n, m with
+ | O, O => true
+ | O, S _ => false
+ | S _, O => false
+ | S n1, S m1 => beq_nat n1 m1
+ end.
+
+Lemma beq_nat_refl : forall n, true = beq_nat n n.
+Proof.
+ intro x; induction x; simpl in |- *; auto.
+Qed.
+
+Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
+Proof.
+ double induction x y; simpl in |- *.
+ reflexivity.
+ intros; discriminate H0.
+ intros; discriminate H0.
+ intros; case (H0 _ H1); reflexivity.
+Defined.