Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
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.

z:Z

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

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

Zeven z <-> Z.even z = true
destruct z as [|p|p]; try destruct p; simpl; intuition. Qed.
z:Z

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

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

Zodd z <-> Z.odd z = true
destruct z as [|p|p]; try destruct p; simpl; intuition. Qed.
n:Z

Zeven n <-> (exists m : Z, n = 2 * m)
Proof (Zeven_equiv n).
n:Z

Zodd n <-> (exists m : Z, n = 2 * m + 1)
Proof (Zodd_equiv n).
Boolean tests of parity (now in BinInt.Z)
Notation Zeven_bool := Z.even (only parsing).
Notation Zodd_bool := Z.odd (only parsing).

n:Z

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

Z.even n = true <-> Zeven n
now rewrite Z.even_spec, Zeven_equiv. Qed.
n:Z

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

Z.odd n = true <-> Zodd n
now rewrite Z.odd_spec, Zodd_equiv. Qed. Ltac boolify_even_odd := rewrite <- ?Zeven_bool_iff, <- ?Zodd_bool_iff.
n:Z

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

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

negb (Z.even n) = Z.odd n
apply Z.negb_even. Qed.
n:Z

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

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

negb (Z.odd n) = Z.even n
apply Z.negb_odd. Qed.
n:Z

{Zeven n} + {Zodd n}
n:Z

{Zeven n} + {Zodd n}
destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right). Defined.
n:Z

{Zeven n} + {~ Zeven n}
n:Z

{Zeven n} + {~ Zeven n}
destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right). Defined.
n:Z

{Zodd n} + {~ Zodd n}
n:Z

{Zodd n} + {~ Zodd n}
destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right). Defined.
n:Z

Zeven n -> ~ Zodd n
n:Z

Zeven n -> ~ Zodd n
n:Z

Z.even n = true -> Z.odd n <> true
n:Z

negb (Z.odd n) = true -> Z.odd n <> true
destruct Z.odd; intuition. Qed.
n:Z

Zodd n -> ~ Zeven n
n:Z

Zodd n -> ~ Zeven n
n:Z

Z.odd n = true -> Z.even n <> true
n:Z

Z.odd n = true -> negb (Z.odd n) <> true
destruct Z.odd; intuition. Qed.
n:Z

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

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

Z.odd n = true -> Z.even (Z.succ n) = true
now rewrite Z.even_succ. Qed.
n:Z

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

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

Z.even n = true -> Z.odd (Z.succ n) = true
now rewrite Z.odd_succ. Qed.
n:Z

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

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

Z.odd n = true -> Z.even (Z.pred n) = true
now rewrite Z.even_pred. Qed.
n:Z

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

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

Z.even n = true -> Z.odd (Z.pred n) = true
now rewrite Z.odd_pred. Qed. Hint Unfold Zeven Zodd: zarith. Notation Zeven_bool_succ := Z.even_succ (only parsing). Notation Zeven_bool_pred := Z.even_pred (only parsing). Notation Zodd_bool_succ := Z.odd_succ (only parsing). Notation Zodd_bool_pred := Z.odd_pred (only parsing). (******************************************************************)

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

and Zodd
Properties of Z.div2
n:Z

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

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

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

Z.even n = true -> n = 2 * Z.div2 n
n:Z

Z.odd n = false -> n = 2 * Z.div2 n
n:Z
Hn:Z.odd n = false

n = 2 * Z.div2 n
n:Z
Hn:Z.odd n = false

2 * Z.div2 n + (if Z.odd n then 1 else 0) = 2 * Z.div2 n
now rewrite Hn, Z.add_0_r. Qed.
n:Z

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

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

Z.odd n = true -> n = 2 * Z.div2 n + 1
n:Z
Hn:Z.odd n = true

n = 2 * Z.div2 n + 1
n:Z
Hn:Z.odd n = true

2 * Z.div2 n + (if Z.odd n then 1 else 0) = 2 * Z.div2 n + 1
now rewrite Hn. Qed.
Properties of Z.quot2
TODO: move to Numbers someday
n:Z

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

n = 2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0)
now destruct n as [ |[p|p| ]|[p|p| ]]. Qed.
n:Z

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

Zeven n -> n = 2 * Z.quot2 n
n:Z
Hn:Zeven n

n = 2 * Z.quot2 n
n:Z
Hn:Z.even n = true

n = 2 * Z.quot2 n
n:Z
Hn:Z.even n = true

2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0) = 2 * Z.quot2 n
now rewrite Zodd_even_bool, Hn, Z.add_0_r. Qed.
n:Z

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

n >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1
n:Z
Hn:n >= 0
Hn':Zodd n

n = 2 * Z.quot2 n + 1
n:Z
Hn:n >= 0
Hn':Z.odd n = true

n = 2 * Z.quot2 n + 1
n:Z
Hn:n >= 0
Hn':Z.odd n = true

2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0) = 2 * Z.quot2 n + 1
n:Z
Hn:n >= 0
Hn':Z.odd n = true

2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n + 1
n:Z
Hn:n >= 0
Hn':Z.odd n = true

Z.sgn n = 1
destruct n; (now destruct Hn) || easy. Qed.
n:Z

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

n <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1
n:Z
Hn:n <= 0
Hn':Zodd n

n = 2 * Z.quot2 n - 1
n:Z
Hn:n <= 0
Hn':Z.odd n = true

n = 2 * Z.quot2 n - 1
n:Z
Hn:n <= 0
Hn':Z.odd n = true

2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n - 1
n:Z
Hn:n <= 0
Hn':Z.odd n = true

2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n + - (1)
n:Z
Hn:n <= 0
Hn':Z.odd n = true

Z.sgn n = - (1)
destruct n; (now destruct Hn) || easy. Qed.
n:Z

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

Z.quot2 (- n) = - Z.quot2 n
now destruct n as [ |[p|p| ]|[p|p| ]]. Qed.
n:Z

Z.quot2 n = n ÷ 2
n:Z

Z.quot2 n = n ÷ 2
n:Z

forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
Z.quot2 n = n ÷ 2
n:Z

forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
n, m:Z
Hm:0 < m

Z.quot2 m = m ÷ 2
n, m:Z
Hm:0 < m

0 <= m
n, m:Z
Hm:0 < m
0 <= (if Z.odd m then Z.sgn m else 0) < 2
n, m:Z
Hm:0 < m
m = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)
n, m:Z
Hm:0 < m

0 <= (if Z.odd m then Z.sgn m else 0) < 2
n, m:Z
Hm:0 < m
m = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)
n, m:Z
Hm:0 < m

0 <= (if Z.odd m then 1 else 0) < 2
n, m:Z
Hm:0 < m
m = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)
n, m:Z
Hm:0 < m

m = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)
apply Zquot2_odd_eqn.
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2

Z.quot2 n = n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
POS:0 < n

Z.quot2 n = n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NUL:0 = n
Z.quot2 n = n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0
Z.quot2 n = n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
POS:0 < n

Z.quot2 n = n ÷ 2
now apply AUX.
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NUL:0 = n

Z.quot2 n = n ÷ 2
now subst.
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0

Z.quot2 n = n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0

- Z.quot2 n = - (n ÷ 2)
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0

Z.quot2 (- n) = - n ÷ 2
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0
2 <> 0
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0

0 < - n
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0
2 <> 0
n:Z
AUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2
NEG:n < 0

2 <> 0
easy. Qed.
More properties of parity
n:Z

({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z

({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z
Hn:Zeven n

({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z
Hn:Zodd n
({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z
Hn:Zeven n

({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z
Hn:Zeven n

{y : Z | n = 2 * y}
n:Z
Hn:Zeven n

n = 2 * Z.div2 n
exact (Zeven_div2 n Hn).
n:Z
Hn:Zodd n

({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%type
n:Z
Hn:Zodd n

{y : Z | n = 2 * y + 1}
n:Z
Hn:Zodd n

n = 2 * Z.div2 n + 1
exact (Zodd_div2 n Hn). Qed.
n:Z

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

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

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

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

n = y + y /\ (y = y \/ y = y + 1)
n, y:Z
Hy:n = y + y

n = y + y
n, y:Z
Hy:n = y + y
y = y \/ y = y + 1
n, y:Z
Hy:n = y + y

y = y \/ y = y + 1
now left.
n, y:Z
Hy:n = y + y + 1

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

n = y + (y + 1) /\ (y = y + 1 \/ y + 1 = y + 1)
n, y:Z
Hy:n = y + y + 1

n = y + (y + 1)
n, y:Z
Hy:n = y + y + 1
y = y + 1 \/ y + 1 = y + 1
n, y:Z
Hy:n = y + y + 1

y = y + 1 \/ y + 1 = y + 1
now right. Qed.
n:Z

Zeven n -> exists m : Z, n = 2 * m
n:Z

Zeven n -> exists m : Z, n = 2 * m
exists (Z.div2 n); apply Zeven_div2; auto. Qed.
n:Z

Zodd n -> exists m : Z, n = 2 * m + 1
n:Z

Zodd n -> exists m : Z, n = 2 * m + 1
exists (Z.div2 n); apply Zodd_div2; auto. Qed.
p:Z

Zeven (2 * p)
p:Z

Zeven (2 * p)
now destruct p. Qed.
p:Z

Zodd (2 * p + 1)
p:Z

Zodd (2 * p + 1)
destruct p as [|p|p]; now try destruct p. Qed.
a, b:Z

Zeven a -> Zodd b -> Zodd (a + b)
a, b:Z

Zeven a -> Zodd b -> Zodd (a + b)
a, b:Z

Z.even a = true -> Z.odd b = true -> Z.odd (a + b) = true
a, b:Z

Z.odd a = false -> Z.odd b = true -> Z.odd (a + b) = true
a, b:Z
Ha:Z.odd a = false
Hb:Z.odd b = true

Z.odd (a + b) = true
now rewrite Z.odd_add, Ha, Hb. Qed.
a, b:Z

Zeven a -> Zeven b -> Zeven (a + b)
a, b:Z

Zeven a -> Zeven b -> Zeven (a + b)
a, b:Z

Z.even a = true -> Z.even b = true -> Z.even (a + b) = true
a, b:Z
Ha:Z.even a = true
Hb:Z.even b = true

Z.even (a + b) = true
now rewrite Z.even_add, Ha, Hb. Qed.
a, b:Z

Zodd a -> Zeven b -> Zodd (a + b)
a, b:Z

Zodd a -> Zeven b -> Zodd (a + b)
a, b:Z
H:Zodd a
H0:Zeven b

Zodd (a + b)
a, b:Z
H:Zodd a
H0:Zeven b

Zodd (b + a)
now apply Zeven_plus_Zodd. Qed.
a, b:Z

Zodd a -> Zodd b -> Zeven (a + b)
a, b:Z

Zodd a -> Zodd b -> Zeven (a + b)
a, b:Z

Z.odd a = true -> Z.odd b = true -> Z.even (a + b) = true
a, b:Z

Z.even a = false -> Z.even b = false -> Z.even (a + b) = true
a, b:Z
Ha:Z.even a = false
Hb:Z.even b = false

Z.even (a + b) = true
now rewrite Z.even_add, Ha, Hb. Qed.
a, b:Z

Zeven a -> Zeven (a * b)
a, b:Z

Zeven a -> Zeven (a * b)
a, b:Z

Z.even a = true -> Z.even (a * b) = true
a, b:Z
Ha:Z.even a = true

Z.even (a * b) = true
now rewrite Z.even_mul, Ha. Qed.
a, b:Z

Zeven b -> Zeven (a * b)
a, b:Z

Zeven b -> Zeven (a * b)
a, b:Z
H:Zeven b

Zeven (a * b)
a, b:Z
H:Zeven b

Zeven (b * a)
now apply Zeven_mult_Zeven_l. Qed.
a, b:Z

Zodd a -> Zodd b -> Zodd (a * b)
a, b:Z

Zodd a -> Zodd b -> Zodd (a * b)
a, b:Z

Z.odd a = true -> Z.odd b = true -> Z.odd (a * b) = true
a, b:Z
Ha:Z.odd a = true
Hb:Z.odd b = true

Z.odd (a * b) = true
now rewrite Z.odd_mul, Ha, Hb. Qed. (* for compatibility *) Close Scope Z_scope.