# Library Coq.ZArith.Zeven

Require Import BinInt.

Open Scope Z_scope.

About parity: even and odd predicates on Z, division by 2 on Z

# Zeven, Zodd and their related properties

Definition Zeven (z:Z) :=
match z with
| Z0 => True
| Zpos (xO _) => True
| Zneg (xO _) => True
| _ => False
end.

Definition Zodd (z:Z) :=
match z with
| Zpos xH => True
| Zneg xH => True
| Zpos (xI _) => True
| Zneg (xI _) => True
| _ => False
end.

Definition Zeven_bool (z:Z) :=
match z with
| Z0 => true
| Zpos (xO _) => true
| Zneg (xO _) => true
| _ => false
end.

Definition Zodd_bool (z:Z) :=
match z with
| Z0 => false
| Zpos (xO _) => false
| Zneg (xO _) => false
| _ => true
end.

Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}.

Definition Zeven_dec : forall z:Z, {Zeven z} + {~ Zeven z}.

Definition Zodd_dec : forall z:Z, {Zodd z} + {~ Zodd z}.

Lemma Zeven_not_Zodd : forall n:Z, Zeven n -> ~ Zodd n.

Lemma Zodd_not_Zeven : forall n:Z, Zodd n -> ~ Zeven n.

Lemma Zeven_Sn : forall n:Z, Zodd n -> Zeven (Zsucc n).

Lemma Zodd_Sn : forall n:Z, Zeven n -> Zodd (Zsucc n).

Lemma Zeven_pred : forall n:Z, Zodd n -> Zeven (Zpred n).

Lemma Zodd_pred : forall n:Z, Zeven n -> Zodd (Zpred n).

Hint Unfold Zeven Zodd: zarith.

# Definition of Zdiv2 and properties wrt Zeven and Zodd

Zdiv2 is defined on all Z, but notice that for odd negative integers it is not the euclidean quotient: in that case we have n = 2*(n/2)-1

Definition Zdiv2 (z:Z) :=
match z with
| Z0 => 0
| Zpos xH => 0
| Zpos p => Zpos (Pdiv2 p)
| Zneg xH => 0
| Zneg p => Zneg (Pdiv2 p)
end.

Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.

Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.

Lemma Zodd_div2_neg :
forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.

Lemma Z_modulo_2 :
forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.

Lemma Zsplit2 :
forall n:Z,
{p : Z * Z |
let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.

Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.

Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.

Theorem Zeven_2p: forall p, Zeven (2 * p).

Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1).

Theorem Zeven_plus_Zodd: forall a b,
Zeven a -> Zodd b -> Zodd (a + b).

Theorem Zeven_plus_Zeven: forall a b,
Zeven a -> Zeven b -> Zeven (a + b).

Theorem Zodd_plus_Zeven: forall a b,
Zodd a -> Zeven b -> Zodd (a + b).

Theorem Zodd_plus_Zodd: forall a b,
Zodd a -> Zodd b -> Zeven (a + b).

Theorem Zeven_mult_Zeven_l: forall a b,
Zeven a -> Zeven (a * b).

Theorem Zeven_mult_Zeven_r: forall a b,
Zeven b -> Zeven (a * b).

Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l
Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand.

Theorem Zodd_mult_Zodd: forall a b,
Zodd a -> Zodd b -> Zodd (a * b).

Close Scope Z_scope.