Library Coq.Arith.Even


Nota : this file is OBSOLETE, and left only for compatibility. Please consider instead predicates Nat.Even and Nat.Odd and Boolean functions Nat.even and Nat.odd.
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.

Require Import PeanoNat.

Local Open Scope nat_scope.

Implicit Types m n : nat.

Inductive definition of even and odd


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).

#[global]
Hint Constructors even: arith.
#[global]
Hint Constructors odd: arith.

Equivalence with predicates Nat.Even and Nat.odd


Lemma even_equiv : forall n, even n <-> Nat.Even n.

Lemma odd_equiv : forall n, odd n <-> Nat.Odd n.

Basic facts

Lemma even_or_odd n : even n \/ odd n.

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

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

Facts about even & odd wrt. plus


Ltac parity2bool :=
 rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec.

Ltac parity_binop_spec :=
 rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul.

Ltac parity_binop :=
 parity2bool; parity_binop_spec; unfold Nat.odd;
 do 2 destruct Nat.even; simpl; tauto.

Lemma even_plus_split n m :
  even (n + m) -> even n /\ even m \/ odd n /\ odd m.

Lemma odd_plus_split n m :
  odd (n + m) -> odd n /\ even m \/ even n /\ odd m.

Lemma even_even_plus n m : even n -> even m -> even (n + m).

Lemma odd_plus_l n m : odd n -> even m -> odd (n + m).

Lemma odd_plus_r n m : even n -> odd m -> odd (n + m).

Lemma odd_even_plus n m : odd n -> odd m -> even (n + m).

Lemma even_plus_aux 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 n m : even (n + m) -> even n -> even m.

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

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

Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n.

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

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

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

Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m.

Facts about even and odd wrt. mult


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

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

Lemma even_mult_r n m : even m -> even (n * m).

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

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

Lemma odd_mult n m : odd n -> odd m -> odd (n * m).

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

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

#[global]
Hint Resolve
 even_even_plus odd_even_plus odd_plus_l odd_plus_r
 even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith.