diff options
Diffstat (limited to 'theories7/Arith/Peano_dec.v')
-rwxr-xr-x | theories7/Arith/Peano_dec.v | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/theories7/Arith/Peano_dec.v b/theories7/Arith/Peano_dec.v new file mode 100755 index 00000000..6646545a --- /dev/null +++ b/theories7/Arith/Peano_dec.v @@ -0,0 +1,36 @@ +(************************************************************************) +(* 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: Peano_dec.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) + +Require Decidable. + +V7only [Import nat_scope.]. +Open Local Scope nat_scope. + +Implicit Variables Type m,n,x,y:nat. + +Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. +Proof. +NewInduction n. +Auto. +Left; Exists n; Auto. +Defined. + +Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}. +Proof. +NewInduction n; NewInduction m; Auto. +Elim (IHn m); Auto. +Defined. + +Hints Resolve O_or_S eq_nat_dec : arith. + +Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)). +Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith. +Defined. + |