Library Coq.ZArith.Zcomplements


Require Import ZArithRing.
Require Import ZArith_base.
Require Export Omega.
Require Import Wf_nat.
Local Open Scope Z_scope.

About parity

Notation two_or_two_plus_one := Z_modulo_2 (only parsing).

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, Z.abs m < Z.abs 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, Z.abs m < Z.abs 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 n : 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 (Z.succ acc) A l
  end.

Definition Zlength := Zlength_aux 0.

Section Zlength_properties.

  Variable A : Type.

  Implicit Type l : list A.

  Lemma Zlength_correct l : Zlength l = Z.of_nat (length l).

  Lemma Zlength_nil : Zlength (A:=A) nil = 0.

  Lemma Zlength_cons (x:A) l : Zlength (x :: l) = Z.succ (Zlength l).

  Lemma Zlength_nil_inv l : Zlength l = 0 -> l = nil.

End Zlength_properties.