PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Tools.ZUtils

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global imports

From Coq Require Import Relations.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.

Local imports

From Padec Require Import SetoidUtil.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Lemma le_plus:
  forall x y, x <= y -> exists i, y = x + Z.of_nat i.

Lemma gt_plus:
  forall x y, x > y -> exists i, y = x - 1 - Z.of_nat i.

Lemma Z_zero_place: forall a b: Z, 0 <= a * b < a -> b = 0.

Lemma Z_no_place: forall a b: Z, ~ 0 < a * b < a.

Some tools about Z/kZ

Section Tools_mod_k.

  Variable (k: Z) (k_pos: k > 0).

  Definition eqk: relation Z := fun x y => exists q, x = y + q*k.
  Definition eqk_alt: relation Z :=
    fun x y => Z.modulo x k = Z.modulo y k.
  Lemma eqk_def_equiv: (eq ==> eq ==> iff) eqk eqk_alt.

  Lemma eqk_def_equiv': forall x y, eqk x y <-> eqk_alt x y.

  Global Instance eqk_equiv: Equivalence eqk.

  Global Instance eqk_Setoid: Setoid Z :=
    @Build_Setoid _ _ eqk_equiv.

  Lemma eqk_dec: forall x y, {eqk x y} + {~eqk x y}.

  Definition gtk: relation Z := (fun x y => x mod k > y mod k).

  Lemma gtk_dec: forall x y, {gtk x y} + {~gtk x y}.

  Global Instance gtk_compat: Proper (eqk ==> eqk ==> iff) gtk.

  Lemma gt_diff: forall x y, k - x mod k + y mod k > 0.

  Lemma mod_nil: forall a, 0 <= a < k -> a mod k = a.

  Lemma mod_add_dist:
    forall a b, a mod k + b mod k < k ->
                (a + b) mod k = a mod k + b mod k.

  Lemma mod1: forall x, x mod 1 = 0.

  Lemma mod1_eq: k = 1 -> forall x y, eqk x y.

  Lemma mod1_gt: k = 1 -> forall x y, ~gtk x y.

  Lemma mod_plus_1: forall y, y mod k <> k - 1 ->
                              (y + 1) mod k = y mod k + 1.

  Lemma mod_plus_1': forall y, y mod k = k - 1 ->
                               (y + 1) mod k = 0.

  Lemma mod_minus_1: forall y, y mod k <> 0 ->
                               (y - 1) mod k = y mod k - 1.

  Lemma mod_minus_1': forall y, y mod k = 0 ->
                                (y - 1) mod k = k - 1.

End Tools_mod_k.

Boolean Test

Section Boolean_Test.

  Context {A: Type} `{SA: Setoid A}.
  Variable (eqA_dec: Decider (equiv (A:=A))).

  Definition dec2b x y := if eqA_dec x y then true else false.

  Global Instance dec2b_compat: Proper fequiv dec2b.

  Lemma dec2b_spec:
    forall x1 x2 y1 y2, dec2b x1 y1 = dec2b x2 y2 <->
                        (x1 == y1 <-> x2 == y2).

  Lemma dec2b_spec_true: forall x y,
      dec2b x y = true <-> x == y.

  Lemma dec2b_spec_false: forall x y,
      dec2b x y = false <-> ~(x == y).

End Boolean_Test.

Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.