Library Coq.ZArith.Zeven


Binary Integers : Parity and Division by Two Initial author : Pierre Crégut (CNET, Lannion, France)
THIS FILE IS DEPRECATED. It is now almost entirely made of compatibility formulations for results already present in BinInt.Z.

Require Import BinInt.

Open Scope Z_scope.

Historical formulation of even and odd predicates, based on case analysis. We now rather recommend using Z.Even and Z.Odd, which are based on the exist predicate.

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.

Lemma Zeven_equiv z : Zeven z <-> Z.Even z.

Lemma Zodd_equiv z : Zodd z <-> Z.Odd z.

Theorem Zeven_ex_iff n : Zeven n <-> exists m, n = 2*m.

Theorem Zodd_ex_iff n : Zodd n <-> exists m, n = 2*m + 1.

Boolean tests of parity (now in BinInt.Z)

Notation Zeven_bool := Z.even (compat "8.3").
Notation Zodd_bool := Z.odd (compat "8.3").

Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n.

Lemma Zodd_bool_iff n : Z.odd n = true <-> Zodd n.

Ltac boolify_even_odd := rewrite <- ?Zeven_bool_iff, <- ?Zodd_bool_iff.

Lemma Zodd_even_bool n : Z.odd n = negb (Z.even n).

Lemma Zeven_odd_bool n : Z.even n = negb (Z.odd n).

Definition Zeven_odd_dec n : {Zeven n} + {Zodd n}.

Definition Zeven_dec n : {Zeven n} + {~ Zeven n}.

Definition Zodd_dec n : {Zodd n} + {~ Zodd n}.

Lemma Zeven_not_Zodd n : Zeven n -> ~ Zodd n.

Lemma Zodd_not_Zeven n : Zodd n -> ~ Zeven n.

Lemma Zeven_Sn n : Zodd n -> Zeven (Z.succ n).

Lemma Zodd_Sn n : Zeven n -> Zodd (Z.succ n).

Lemma Zeven_pred n : Zodd n -> Zeven (Z.pred n).

Lemma Zodd_pred n : Zeven n -> Zodd (Z.pred n).

Hint Unfold Zeven Zodd: zarith.

Notation Zeven_bool_succ := Z.even_succ (compat "8.3").
Notation Zeven_bool_pred := Z.even_pred (compat "8.3").
Notation Zodd_bool_succ := Z.odd_succ (compat "8.3").
Notation Zodd_bool_pred := Z.odd_pred (compat "8.3").

Definition of Z.quot2, Z.div2 and properties wrt Zeven

and Zodd

Notation Zdiv2 := Z.div2 (compat "8.3").
Notation Zquot2 := Z.quot2 (compat "8.3").

Properties of Z.div2

Lemma Zdiv2_odd_eqn n : n = 2*(Z.div2 n) + if Z.odd n then 1 else 0.

Lemma Zeven_div2 n : Zeven n -> n = 2 * Z.div2 n.

Lemma Zodd_div2 n : Zodd n -> n = 2 * Z.div2 n + 1.

Properties of Z.quot2
TODO: move to Numbers someday

Lemma Zquot2_odd_eqn n : n = 2*(Z.quot2 n) + if Z.odd n then Z.sgn n else 0.

Lemma Zeven_quot2 n : Zeven n -> n = 2 * Z.quot2 n.

Lemma Zodd_quot2 n : n >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1.

Lemma Zodd_quot2_neg n : n <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1.

Lemma Zquot2_opp n : Z.quot2 (-n) = - Z.quot2 n.

Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.

More properties of parity

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

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

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

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

Theorem Zeven_2p p : Zeven (2 * p).

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

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

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

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

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

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

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

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

Close Scope Z_scope.