diff options
Diffstat (limited to 'theories7/Arith/EqNat.v')
-rwxr-xr-x | theories7/Arith/EqNat.v | 78 |
1 files changed, 0 insertions, 78 deletions
diff --git a/theories7/Arith/EqNat.v b/theories7/Arith/EqNat.v deleted file mode 100755 index 9f5ee7ee..00000000 --- a/theories7/Arith/EqNat.v +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* 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. - |