# Library Coq.micromega.ZifyBool

Require Import Bool ZArith.
Require Import Zify ZifyClasses.
Local Open Scope Z_scope.

Z_of_bool is the injection function for boolean
Definition Z_of_bool (b : bool) : Z := if b then 1 else 0.

bool_of_Z is a compatible reverse operation
Definition bool_of_Z (z : Z) : bool := negb (Z.eqb z 0).

Lemma Z_of_bool_bound : forall x, 0 <= Z_of_bool x <= 1.

Instance Inj_bool_Z : InjTyp bool Z :=
{ inj := Z_of_bool ; pred :=(fun x => 0 <= x <= 1) ; cstr := Z_of_bool_bound}.

Boolean operators

Instance Op_andb : BinOp andb :=
{ TBOp := Z.min ;
TBOpInj := ltac: (destruct n,m; reflexivity)}.

Instance Op_orb : BinOp orb :=
{ TBOp := Z.max ;
TBOpInj := ltac:(destruct n,m; reflexivity)}.

Instance Op_implb : BinOp implb :=
{ TBOp := fun x y => Z.max (1 - x) y;
TBOpInj := ltac:(destruct n,m; reflexivity) }.

Instance Op_xorb : BinOp xorb :=
{ TBOp := fun x y => Z.max (x - y) (y - x);
TBOpInj := ltac:(destruct n,m; reflexivity) }.

Instance Op_negb : UnOp negb :=
{ TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}.

Instance Op_eq_bool : BinRel (@eq bool) :=
{TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.

Instance Op_true : CstOp true :=
{ TCst := 1 ; TCstInj := eq_refl }.

Instance Op_false : CstOp false :=
{ TCst := 0 ; TCstInj := eq_refl }.

Comparisons are encoded using the predicates isZero and isLeZero.

Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0).

Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0).

Instance Op_isZero : UnOp isZero :=
{ TUOp := isZero; TUOpInj := ltac: (reflexivity) }.

Instance Op_isLeZero : UnOp isLeZero :=
{ TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }.

Lemma Z_eqb_isZero : forall n m,
Z_of_bool (n =? m) = isZero (n - m).

Lemma Z_leb_sub : forall x y, x <=? y = ((x - y) <=? 0).

Lemma Z_ltb_leb : forall x y, x <? y = (x +1 <=? y).

Comparison over Z

Instance Op_Zeqb : BinOp Z.eqb :=
{ TBOp := fun x y => isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}.

Instance Op_Zleb : BinOp Z.leb :=
{ TBOp := fun x y => isLeZero (x-y) ;
TBOpInj :=
ltac: (intros;unfold isLeZero;
rewrite Z_leb_sub;
auto) }.

Instance Op_Zgeb : BinOp Z.geb :=
{ TBOp := fun x y => isLeZero (y-x) ;
TBOpInj := ltac:(
intros;
unfold isLeZero;
rewrite Z.geb_leb;
rewrite Z_leb_sub;
auto) }.

Instance Op_Zltb : BinOp Z.ltb :=
{ TBOp := fun x y => isLeZero (x+1-y) ;
TBOpInj := ltac:(
intros;
unfold isLeZero;
rewrite Z_ltb_leb;
rewrite <- Z_leb_sub;
reflexivity) }.

Instance Op_Zgtb : BinOp Z.gtb :=
{ TBOp := fun x y => isLeZero (y-x+1) ;
TBOpInj := ltac:(
intros;
unfold isLeZero;
rewrite Z.gtb_ltb;
rewrite Z_ltb_leb;
rewrite Z_leb_sub;
reflexivity) }.

Comparison over nat

Lemma Z_of_nat_eqb_iff : forall n m,
(n =? m)%nat = (Z.of_nat n =? Z.of_nat m).

Lemma Z_of_nat_leb_iff : forall n m,
(n <=? m)%nat = (Z.of_nat n <=? Z.of_nat m).

Lemma Z_of_nat_ltb_iff : forall n m,
(n <? m)%nat = (Z.of_nat n <? Z.of_nat m).

Instance Op_nat_eqb : BinOp Nat.eqb :=
{ TBOp := fun x y => isZero (Z.sub x y) ;
TBOpInj := ltac:(
intros; simpl;
rewrite <- Z_eqb_isZero;
f_equal; apply Z_of_nat_eqb_iff) }.

Instance Op_nat_leb : BinOp Nat.leb :=
{ TBOp := fun x y => isLeZero (x-y) ;
TBOpInj := ltac:(
intros;
rewrite Z_of_nat_leb_iff;
unfold isLeZero;
rewrite Z_leb_sub;
auto) }.

Instance Op_nat_ltb : BinOp Nat.ltb :=
{ TBOp := fun x y => isLeZero (x+1-y) ;
TBOpInj := ltac:(
intros;
rewrite Z_of_nat_ltb_iff;
unfold isLeZero;
rewrite Z_ltb_leb;
rewrite <- Z_leb_sub;
reflexivity) }.

Injected boolean operators

Lemma Z_eqb_ZSpec_ok : forall x, 0 <= isZero x <= 1 /\
(x = 0 <-> isZero x = 1).

Instance Z_eqb_ZSpec : UnOpSpec isZero :=
{| UPred := fun n r => 0 <= r <= 1 /\ (n = 0 <-> isZero n = 1) ; USpec := Z_eqb_ZSpec_ok |}.