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

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.

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.

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.