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:ZZeven z <-> Z.Even zz:ZZeven z <-> Z.Even zdestruct z as [|p|p]; try destruct p; simpl; intuition. Qed.z:ZZeven z <-> Z.even z = truez:ZZodd z <-> Z.Odd zz:ZZodd z <-> Z.Odd zdestruct z as [|p|p]; try destruct p; simpl; intuition. Qed.z:ZZodd z <-> Z.odd z = trueProof (Zeven_equiv n).n:ZZeven n <-> (exists m : Z, n = 2 * m)Proof (Zodd_equiv n).n:ZZodd n <-> (exists m : Z, n = 2 * m + 1)
Boolean tests of parity (now in BinInt.Z)
Notation Zeven_bool := Z.even (only parsing). Notation Zodd_bool := Z.odd (only parsing).n:ZZ.even n = true <-> Zeven nnow rewrite Z.even_spec, Zeven_equiv. Qed.n:ZZ.even n = true <-> Zeven nn:ZZ.odd n = true <-> Zodd nnow rewrite Z.odd_spec, Zodd_equiv. Qed. Ltac boolify_even_odd := rewrite <- ?Zeven_bool_iff, <- ?Zodd_bool_iff.n:ZZ.odd n = true <-> Zodd nn:ZZ.odd n = negb (Z.even n)n:ZZ.odd n = negb (Z.even n)apply Z.negb_even. Qed.n:Znegb (Z.even n) = Z.odd nn:ZZ.even n = negb (Z.odd n)n:ZZ.even n = negb (Z.odd n)apply Z.negb_odd. Qed.n:Znegb (Z.odd n) = Z.even nn:Z{Zeven 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} + {~ Zeven n}destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right). Defined.n:Z{Zeven n} + {~ Zeven n}n:Z{Zodd n} + {~ Zodd n}destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right). Defined.n:Z{Zodd n} + {~ Zodd n}n:ZZeven n -> ~ Zodd nn:ZZeven n -> ~ Zodd nn:ZZ.even n = true -> Z.odd n <> truedestruct Z.odd; intuition. Qed.n:Znegb (Z.odd n) = true -> Z.odd n <> truen:ZZodd n -> ~ Zeven nn:ZZodd n -> ~ Zeven nn:ZZ.odd n = true -> Z.even n <> truedestruct Z.odd; intuition. Qed.n:ZZ.odd n = true -> negb (Z.odd n) <> truen:ZZodd n -> Zeven (Z.succ n)n:ZZodd n -> Zeven (Z.succ n)now rewrite Z.even_succ. Qed.n:ZZ.odd n = true -> Z.even (Z.succ n) = truen:ZZeven n -> Zodd (Z.succ n)n:ZZeven n -> Zodd (Z.succ n)now rewrite Z.odd_succ. Qed.n:ZZ.even n = true -> Z.odd (Z.succ n) = truen:ZZodd n -> Zeven (Z.pred n)n:ZZodd n -> Zeven (Z.pred n)now rewrite Z.even_pred. Qed.n:ZZ.odd n = true -> Z.even (Z.pred n) = truen:ZZeven n -> Zodd (Z.pred n)n:ZZeven n -> Zodd (Z.pred n)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). (******************************************************************)n:ZZ.even n = true -> Z.odd (Z.pred n) = true
Properties of Z.div2
Proof (Z.div2_odd n).n:Zn = 2 * Z.div2 n + (if Z.odd n then 1 else 0)n:ZZeven n -> n = 2 * Z.div2 nn:ZZeven n -> n = 2 * Z.div2 nn:ZZ.even n = true -> n = 2 * Z.div2 nn:ZZ.odd n = false -> n = 2 * Z.div2 nn:ZHn:Z.odd n = falsen = 2 * Z.div2 nnow rewrite Hn, Z.add_0_r. Qed.n:ZHn:Z.odd n = false2 * Z.div2 n + (if Z.odd n then 1 else 0) = 2 * Z.div2 nn:ZZodd n -> n = 2 * Z.div2 n + 1n:ZZodd n -> n = 2 * Z.div2 n + 1n:ZZ.odd n = true -> n = 2 * Z.div2 n + 1n:ZHn:Z.odd n = truen = 2 * Z.div2 n + 1now rewrite Hn. Qed.n:ZHn:Z.odd n = true2 * Z.div2 n + (if Z.odd n then 1 else 0) = 2 * Z.div2 n + 1
Properties of Z.quot2
TODO: move to Numbers someday
n:Zn = 2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0)now destruct n as [ |[p|p| ]|[p|p| ]]. Qed.n:Zn = 2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0)n:ZZeven n -> n = 2 * Z.quot2 nn:ZZeven n -> n = 2 * Z.quot2 nn:ZHn:Zeven nn = 2 * Z.quot2 nn:ZHn:Z.even n = truen = 2 * Z.quot2 nnow rewrite Zodd_even_bool, Hn, Z.add_0_r. Qed.n:ZHn:Z.even n = true2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0) = 2 * Z.quot2 nn:Zn >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1n:Zn >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1n:ZHn:n >= 0Hn':Zodd nn = 2 * Z.quot2 n + 1n:ZHn:n >= 0Hn':Z.odd n = truen = 2 * Z.quot2 n + 1n:ZHn:n >= 0Hn':Z.odd n = true2 * Z.quot2 n + (if Z.odd n then Z.sgn n else 0) = 2 * Z.quot2 n + 1n:ZHn:n >= 0Hn':Z.odd n = true2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n + 1destruct n; (now destruct Hn) || easy. Qed.n:ZHn:n >= 0Hn':Z.odd n = trueZ.sgn n = 1n:Zn <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1n:Zn <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1n:ZHn:n <= 0Hn':Zodd nn = 2 * Z.quot2 n - 1n:ZHn:n <= 0Hn':Z.odd n = truen = 2 * Z.quot2 n - 1n:ZHn:n <= 0Hn':Z.odd n = true2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n - 1n:ZHn:n <= 0Hn':Z.odd n = true2 * Z.quot2 n + Z.sgn n = 2 * Z.quot2 n + - (1)destruct n; (now destruct Hn) || easy. Qed.n:ZHn:n <= 0Hn':Z.odd n = trueZ.sgn n = - (1)n:ZZ.quot2 (- n) = - Z.quot2 nnow destruct n as [ |[p|p| ]|[p|p| ]]. Qed.n:ZZ.quot2 (- n) = - Z.quot2 nn:ZZ.quot2 n = n ÷ 2n:ZZ.quot2 n = n ÷ 2n:Zforall m : Z, 0 < m -> Z.quot2 m = m ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2Z.quot2 n = n ÷ 2n:Zforall m : Z, 0 < m -> Z.quot2 m = m ÷ 2n, m:ZHm:0 < mZ.quot2 m = m ÷ 2n, m:ZHm:0 < m0 <= mn, m:ZHm:0 < m0 <= (if Z.odd m then Z.sgn m else 0) < 2n, m:ZHm:0 < mm = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)n, m:ZHm:0 < m0 <= (if Z.odd m then Z.sgn m else 0) < 2n, m:ZHm:0 < mm = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)n, m:ZHm:0 < m0 <= (if Z.odd m then 1 else 0) < 2n, m:ZHm:0 < mm = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)apply Zquot2_odd_eqn.n, m:ZHm:0 < mm = 2 * Z.quot2 m + (if Z.odd m then Z.sgn m else 0)n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2Z.quot2 n = n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2POS:0 < nZ.quot2 n = n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NUL:0 = nZ.quot2 n = n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 0Z.quot2 n = n ÷ 2now apply AUX.n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2POS:0 < nZ.quot2 n = n ÷ 2now subst.n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NUL:0 = nZ.quot2 n = n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 0Z.quot2 n = n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 0- Z.quot2 n = - (n ÷ 2)n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 0Z.quot2 (- n) = - n ÷ 2n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 02 <> 0n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 00 < - nn:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 02 <> 0easy. Qed.n:ZAUX:forall m : Z, 0 < m -> Z.quot2 m = m ÷ 2NEG:n < 02 <> 0
More properties of parity
n:Z({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:Z({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:ZHn:Zeven n({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:ZHn:Zodd n({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:ZHn:Zeven n({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:ZHn:Zeven n{y : Z | n = 2 * y}exact (Zeven_div2 n Hn).n:ZHn:Zeven nn = 2 * Z.div2 nn:ZHn:Zodd n({y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z})%typen:ZHn:Zodd n{y : Z | n = 2 * y + 1}exact (Zodd_div2 n Hn). Qed.n:ZHn:Zodd nn = 2 * Z.div2 n + 1n: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:ZHy:n = y + y{p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}n, y:ZHy:n = y + y + 1{p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}n, y:ZHy:n = y + y{p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}n, y:ZHy:n = y + yn = y + y /\ (y = y \/ y = y + 1)n, y:ZHy:n = y + yn = y + yn, y:ZHy:n = y + yy = y \/ y = y + 1now left.n, y:ZHy:n = y + yy = y \/ y = y + 1n, y:ZHy:n = y + y + 1{p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}n, y:ZHy:n = y + y + 1n = y + (y + 1) /\ (y = y + 1 \/ y + 1 = y + 1)n, y:ZHy:n = y + y + 1n = y + (y + 1)n, y:ZHy:n = y + y + 1y = y + 1 \/ y + 1 = y + 1now right. Qed.n, y:ZHy:n = y + y + 1y = y + 1 \/ y + 1 = y + 1n:ZZeven n -> exists m : Z, n = 2 * mexists (Z.div2 n); apply Zeven_div2; auto. Qed.n:ZZeven n -> exists m : Z, n = 2 * mn:ZZodd n -> exists m : Z, n = 2 * m + 1exists (Z.div2 n); apply Zodd_div2; auto. Qed.n:ZZodd n -> exists m : Z, n = 2 * m + 1p:ZZeven (2 * p)now destruct p. Qed.p:ZZeven (2 * p)p:ZZodd (2 * p + 1)destruct p as [|p|p]; now try destruct p. Qed.p:ZZodd (2 * p + 1)a, b:ZZeven a -> Zodd b -> Zodd (a + b)a, b:ZZeven a -> Zodd b -> Zodd (a + b)a, b:ZZ.even a = true -> Z.odd b = true -> Z.odd (a + b) = truea, b:ZZ.odd a = false -> Z.odd b = true -> Z.odd (a + b) = truenow rewrite Z.odd_add, Ha, Hb. Qed.a, b:ZHa:Z.odd a = falseHb:Z.odd b = trueZ.odd (a + b) = truea, b:ZZeven a -> Zeven b -> Zeven (a + b)a, b:ZZeven a -> Zeven b -> Zeven (a + b)a, b:ZZ.even a = true -> Z.even b = true -> Z.even (a + b) = truenow rewrite Z.even_add, Ha, Hb. Qed.a, b:ZHa:Z.even a = trueHb:Z.even b = trueZ.even (a + b) = truea, b:ZZodd a -> Zeven b -> Zodd (a + b)a, b:ZZodd a -> Zeven b -> Zodd (a + b)a, b:ZH:Zodd aH0:Zeven bZodd (a + b)now apply Zeven_plus_Zodd. Qed.a, b:ZH:Zodd aH0:Zeven bZodd (b + a)a, b:ZZodd a -> Zodd b -> Zeven (a + b)a, b:ZZodd a -> Zodd b -> Zeven (a + b)a, b:ZZ.odd a = true -> Z.odd b = true -> Z.even (a + b) = truea, b:ZZ.even a = false -> Z.even b = false -> Z.even (a + b) = truenow rewrite Z.even_add, Ha, Hb. Qed.a, b:ZHa:Z.even a = falseHb:Z.even b = falseZ.even (a + b) = truea, b:ZZeven a -> Zeven (a * b)a, b:ZZeven a -> Zeven (a * b)a, b:ZZ.even a = true -> Z.even (a * b) = truenow rewrite Z.even_mul, Ha. Qed.a, b:ZHa:Z.even a = trueZ.even (a * b) = truea, b:ZZeven b -> Zeven (a * b)a, b:ZZeven b -> Zeven (a * b)a, b:ZH:Zeven bZeven (a * b)now apply Zeven_mult_Zeven_l. Qed.a, b:ZH:Zeven bZeven (b * a)a, b:ZZodd a -> Zodd b -> Zodd (a * b)a, b:ZZodd a -> Zodd b -> Zodd (a * b)a, b:ZZ.odd a = true -> Z.odd b = true -> Z.odd (a * b) = truenow rewrite Z.odd_mul, Ha, Hb. Qed. (* for compatibility *) Close Scope Z_scope.a, b:ZHa:Z.odd a = trueHb:Z.odd b = trueZ.odd (a * b) = true