blob: 2d142cdc87d71314d47b56a9d7b4a403a827a431 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $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.
|
