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.