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}.
Add InjTyp Inj_bool_Z.

Boolean operators

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

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

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

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

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

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

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

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

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) }.
Add UnOp Op_isZero.

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


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) }.
Add BinOp Op_Zleb.

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) }.
Add BinOp Op_Zgeb.

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;
                   rewrite Z.add_sub_swap;
                   reflexivity) }.
Add BinOp Op_Zgtb.

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) }.
Add BinOp Op_nat_eqb.

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) }.
Add BinOp Op_nat_leb.

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) }.
Add BinOp Op_nat_ltb.

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 |}.
Add Spec Z_eqb_ZSpec.

Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0.

Instance leZeroSpec : UnOpSpec isLeZero :=
  {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}.
Add Spec leZeroSpec.