Zcomplements.v

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)         *)
(************************************************************************)

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.forall p : positive, floor p > 0
Proof.forall p : positive, floor p > 0 reflexivity. Qed.

Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.forall p : positive, floor p <= Z.pos p < 2 * floor p
Proof.forall p : positive, floor p <= Z.pos p < 2 * floor p
 unfold floor.forall p : positive,
Z.pos (floor_pos p) <= Z.pos p <
2 * Z.pos (floor_pos p) induction p; simpl.p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
Z.pos (floor_pos p)~0 <= Z.pos p~1 <
Z.pos (floor_pos p)~0~0
p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
Z.pos (floor_pos p)~0 <= Z.pos p~0 <
Z.pos (floor_pos p)~0~0
1 <= 1 < 2
 -p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
Z.pos (floor_pos p)~0 <= Z.pos p~1 <
Z.pos (floor_pos p)~0~0 rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO.p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
2 * Z.pos (floor_pos p) <= 2 * Z.pos p + 1 <
2 * (2 * Z.pos (floor_pos p)) omega.
 -p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
Z.pos (floor_pos p)~0 <= Z.pos p~0 <
Z.pos (floor_pos p)~0~0 rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO.p:positive
IHp:Z.pos (floor_pos p) <= Z.pos p < 2 * Z.pos (floor_pos p)
2 * Z.pos (floor_pos p) <= 2 * Z.pos p <
2 * (2 * Z.pos (floor_pos p)) omega.
 -1 <= 1 < 2 omega.
Qed.

(**********************************************************************)

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.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
Proof.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
  intros P HP p.P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
P p
  set (Q := fun z => 0 <= z -> P z * P (- z)).P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z * P (- z):Z -> Set
P p
  enough (H:Q (Z.abs p)) by
    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z * P (- z):Z -> Set
Q (Z.abs p)
  apply (Z_lt_rec Q); auto with zarith.P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z * P (- z):Z -> Set
forall x : Z, (forall y : Z, 0 <= y < x -> Q y) -> Q x
  subst Q; intros x H.P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
(fun z : Z => 0 <= z -> P z * P (- z)) x
  split; apply HP.P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs x -> P m
P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs (- x) -> P m
  -P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs x -> P m rewrite Z.abs_eq; auto; intros.P:Z -> Set
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
P m
    destruct (H (Z.abs m)); auto with zarith.P:Z -> Set
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
p0:P (Z.abs m)
p1:P (- Z.abs m)
P m
    destruct (Zabs_dec m) as [-> | ->]; trivial.
  -P:Z -> Set
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs (- x) -> P m rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.P:Z -> Set
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
P m
    destruct (H (Z.abs m)); auto with zarith.P:Z -> Set
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z * P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
p0:P (Z.abs m)
p1:P (- Z.abs m)
P m
    destruct (Zabs_dec m) as [-> | ->]; trivial.
Qed.

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.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
Proof.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
  intros P HP p.P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
P p
  set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z /\ P (- z):Z -> Prop
P p
  enough (Q (Z.abs p)) by
    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z /\ P (- z):Z -> Prop
Q (Z.abs p)
  apply (Z_lt_induction Q); auto with zarith.P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p:Z
Q:=fun z : Z => 0 <= z -> P z /\ P (- z):Z -> Prop
forall x : Z, (forall y : Z, 0 <= y < x -> Q y) -> Q x
  subst Q; intros.P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
(fun z : Z => 0 <= z -> P z /\ P (- z)) x
  split; apply HP.P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs x -> P m
P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs (- x) -> P m
  -P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs x -> P m rewrite Z.abs_eq; auto; intros.P:Z -> Prop
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
P m
    elim (H (Z.abs m)); intros; auto with zarith.P:Z -> Prop
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
H2:P (Z.abs m)
H3:P (- Z.abs m)
P m
    elim (Zabs_dec m); intro eq; rewrite eq; trivial.
  -P:Z -> Prop
HP:forall n : Z,
(forall m : Z, Z.abs m < Z.abs n -> P m) -> P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
forall m : Z, Z.abs m < Z.abs (- x) -> P m rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.P:Z -> Prop
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
P m
    destruct (H (Z.abs m)); auto with zarith.P:Z -> Prop
HP:forall n : Z,
(forall m0 : Z, Z.abs m0 < Z.abs n -> P m0) ->
P n
p, x:Z
H:forall y : Z,
0 <= y < x ->
(fun z : Z => 0 <= z -> P z /\ P (- z)) y
H0:0 <= x
m:Z
H1:Z.abs m < x
H2:P (Z.abs m)
H3:P (- Z.abs m)
P m
    destruct (Zabs_dec m) as [-> | ->]; trivial.
Qed.

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.forall (n : Z) (P : Prop),
(n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P
Proof.forall (n : Z) (P : Prop),
(n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P
  intros x P Hzero Hpos Hneg.x:Z
P:Prop
Hzero:x = 0 -> P
Hpos:x > 0 -> P
Hneg:x < 0 -> P
P
  destruct x; [apply Hzero|apply Hpos|apply Hneg]; easy.
Qed.

Lemma sqr_pos n : n * n >= 0.n:Z
n * n >= 0
Proof.n:Z
n * n >= 0
 Z.swap_greater.n:Z
0 <= n * n apply Z.square_nonneg.
Qed.

(**********************************************************************)

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.
Arguments Zlength [A] l.

Section Zlength_properties.

  Variable A : Type.

  Implicit Type l : list A.

  Lemma Zlength_correct l : Zlength l = Z.of_nat (length l).A:Type
l:list A
Zlength l = Z.of_nat (length l)
  Proof.A:Type
l:list A
Zlength l = Z.of_nat (length l)
    assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)).A:Type
l:list A
forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l)
    clear l.A:Type
forall (l : list A) (acc : Z),
Zlength_aux acc A l = acc + Z.of_nat (length l)
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l) induction l.A:Type
forall acc : Z,
Zlength_aux acc A nil = acc + Z.of_nat (length nil)
A:Type
a:A
l:list A
IHl:forall acc : Z, Zlength_aux acc A l = acc + Z.of_nat (length l)
forall acc : Z,
Zlength_aux acc A (a :: l) =
acc + Z.of_nat (length (a :: l))
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l)
    auto with zarith.A:Type
a:A
l:list A
IHl:forall acc : Z, Zlength_aux acc A l = acc + Z.of_nat (length l)
forall acc : Z,
Zlength_aux acc A (a :: l) =
acc + Z.of_nat (length (a :: l))
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l)
    intros.A:Type
a:A
l:list A
IHl:forall acc0 : Z, Zlength_aux acc0 A l = acc0 + Z.of_nat (length l)
acc:Z
Zlength_aux acc A (a :: l) =
acc + Z.of_nat (length (a :: l))
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l) simpl length; simpl Zlength_aux.A:Type
a:A
l:list A
IHl:forall acc0 : Z, Zlength_aux acc0 A l = acc0 + Z.of_nat (length l)
acc:Z
Zlength_aux (Z.succ acc) A l =
acc + Z.of_nat (S (length l))
A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l)
     rewrite IHl, Nat2Z.inj_succ; auto with zarith.A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength l = Z.of_nat (length l)
    unfold Zlength.A:Type
l:list A
H:forall (l0 : list A) (acc : Z),
Zlength_aux acc A l0 = acc + Z.of_nat (length l0)
Zlength_aux 0 A l = Z.of_nat (length l) now rewrite H.
  Qed.

  Lemma Zlength_nil : Zlength (A:=A) nil = 0.A:Type
Zlength nil = 0
  Proof.A:Type
Zlength nil = 0 reflexivity. Qed.

  Lemma Zlength_cons (x:A) l : Zlength (x :: l) = Z.succ (Zlength l).A:Type
x:A
l:list A
Zlength (x :: l) = Z.succ (Zlength l)
  Proof.A:Type
x:A
l:list A
Zlength (x :: l) = Z.succ (Zlength l)
    intros.A:Type
x:A
l:list A
Zlength (x :: l) = Z.succ (Zlength l) now rewrite !Zlength_correct, <- Nat2Z.inj_succ.
  Qed.

  Lemma Zlength_nil_inv l : Zlength l = 0 -> l = nil.A:Type
l:list A
Zlength l = 0 -> l = nil
  Proof.A:Type
l:list A
Zlength l = 0 -> l = nil
    rewrite Zlength_correct.A:Type
l:list A
Z.of_nat (length l) = 0 -> l = nil
    destruct l as [|x l]; auto.A:Type
x:A
l:list A
Z.of_nat (length (x :: l)) = 0 -> x :: l = nil
    now rewrite <- Nat2Z.inj_0, Nat2Z.inj_iff.
  Qed.

End Zlength_properties.

Arguments Zlength_correct [A] l.
Arguments Zlength_cons [A] x l.
Arguments Zlength_nil_inv [A] l _.