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