Library Coq.Arith.Even

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.

Local Open Scope nat_scope.

Implicit Types m n : nat.

Definition of even and odd, and basic facts

Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
    odd_S : forall n, even n -> odd (S n).

Hint Constructors even: arith.
Hint Constructors odd: arith.

Lemma even_or_odd : forall n, even n \/ odd n.

Lemma even_odd_dec : forall n, {even n } + {odd n }.

Lemma not_even_and_odd : forall n, even n -> odd n -> False.

Facts about even & odd wrt. plus

Lemma even_plus_split : forall n m,
  (even (n + m) -> even n /\ even m \/ odd n /\ odd m)
with odd_plus_split : forall n m,
  odd (n + m) -> odd n /\ even m \/ even n /\ odd m.

Lemma even_even_plus : forall n m, even n -> even m -> even (n + m)
with odd_plus_l : forall n m, odd n -> even m -> odd (n + m).

Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m)
with odd_even_plus : forall n m, odd n -> odd m -> even (n + m).

Lemma even_plus_aux : forall n m,
    (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m ) /\
    (even (n + m) <-> even n /\ even m \/ odd n /\ odd m ).

Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m.

Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n.

Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m.

Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n.
Hint Resolve even_even_plus odd_even_plus: arith.

Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n.

Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m.

Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n.

Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m.
Hint Resolve odd_plus_l odd_plus_r: arith.

Facts about even and odd wrt. mult

Lemma even_mult_aux :
forall n m,
(odd (n * m) <-> odd n /\ odd m ) /\ (even (n * m) <-> even n \/ even m ).

Lemma even_mult_l : forall n m, even n -> even (n * m).

Lemma even_mult_r : forall n m, even m -> even (n * m).
Hint Resolve even_mult_l even_mult_r: arith.

Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m.

Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n.

Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m).
Hint Resolve even_mult_l even_mult_r odd_mult: arith.

Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n.

Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m.