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