diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /theories/Arith/EqNat.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Arith/EqNat.v')
-rw-r--r-- | theories/Arith/EqNat.v | 70 |
1 files changed, 42 insertions, 28 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 09df9464..82d05e2c 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqNat.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: EqNat.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Equality on natural numbers *) @@ -14,52 +14,66 @@ Open Local Scope nat_scope. Implicit Types m n x y : nat. +(** * Propositional equality *) + 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 + | 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. + 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. +(** [eq] restricted to [nat] and [eq_nat] are equivalent *) + +Lemma 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. +Lemma 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_is_eq : forall n m, eq_nat n m <-> n = m. +Proof. + split; auto with arith. +Qed. + 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. + forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. +Proof. + 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. +Proof. + 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. + +(** * Boolean equality on [nat] *) + 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 + | 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. @@ -71,7 +85,7 @@ 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. + intros n H1 H2. discriminate H2. + intros n H1 H2. discriminate H2. + intros n H1 z H2 H3. case (H2 _ H3). reflexivity. Defined. |