# Library Coq.ZArith.Zcomplements

Require Import ZArithRing.
Require Import ZArith_base.
Require Export Omega.
Require Import Wf_nat.
Open Local Scope Z_scope.
About parity
Lemma two_or_two_plus_one :
forall n:Z, { y : Z | n = 2 * y } + { y : Z | n = 2 * y + 1}.
The biggest power of 2 that is stricly less than a
Easy to compute: replace all "1" of the binary representation by "0", except the first "1" (or the first one :-)
Fixpoint floor_pos (a:positive) : positive :=
match a with
| xH => 1%positive
| xO a' => xO (floor_pos a')
| xI b' => xO (floor_pos b')
end.
Definition floor (a:positive) := Zpos (floor_pos a).
Lemma floor_gt0 : forall p:positive, floor p > 0.
Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.
Two more induction principles over Z.
Theorem Z_lt_abs_rec :
forall P:Z -> Set,
(forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) ->
forall n:Z, P n.
Theorem Z_lt_abs_induction :
forall P:Z -> Prop,
(forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) ->
forall n:Z, P n.
To do case analysis over the sign of z
Lemma Zcase_sign :
forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P.
Lemma sqr_pos : forall n:Z, n * n >= 0.
A list length in Z, tail recursive.
Require Import List.
Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z :=
match l with
| nil => acc
| _ :: l => Zlength_aux (Zsucc acc) A l
end.
Definition Zlength := Zlength_aux 0.
Implicit Arguments Zlength [A].
Section Zlength_properties.
Variable A : Type.
Implicit Type l : list A.
Lemma Zlength_correct : forall l, Zlength l = Z_of_nat (length l).
Lemma Zlength_nil : Zlength (A:=A) nil = 0.
Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l).
Lemma Zlength_nil_inv : forall l, Zlength l = 0 -> l = nil.
End Zlength_properties.
Implicit Arguments Zlength_correct [A].
Implicit Arguments Zlength_cons [A].
Implicit Arguments Zlength_nil_inv [A].