mise sous CVS du repertoire theories/Arith

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 39 insertions, 0 deletions

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
new file mode 100644
index 000000000..a79a4d267
--- /dev/null
+++ b/theories/Arith/Even.v
@@ -0,0 +1,39 @@
+
+(* $Id$ *)
+
+(* Here we define the predicates even and odd by mutual induction
+ * and we prove the decidability and the exclusion of those predicates.
+ *
+ * The main results about parity are proved in the module Div2.
+ *)
+
+Inductive even : nat->Prop :=
+    even_O : (even O)
+  | even_S : (n:nat)(odd n)->(even (S n))
+with odd : nat->Prop :=
+    odd_S : (n:nat)(even n)->(odd (S n)).
+
+Hint constr_even : arith := Constructors even.
+Hint constr_odd : arith := Constructors odd.
+
+Lemma even_or_odd : (n:nat) (even n)\/(odd n).
+Proof.
+Induction n.
+Auto with arith.
+Intros n' H. Elim H; Auto with arith.
+Save.
+
+Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
+Proof.
+Induction n.
+Auto with arith.
+Intros n' H. Elim H; Auto with arith.
+Save.
+
+Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
+Proof.
+Induction n.
+Intros. Inversion H0.
+Intros. Inversion H0. Inversion H1. Auto with arith.
+Save.
+