Library IntBool

Require Import ZArith.
Require Export Bool.

Definition int := Z.

Open Scope Z_scope.

Theorem int_eq_dec : forall a b : int, {a = b} + {a <> b}.

Fixpoint blt_pos (p q : positive) {struct p} : bool :=
  match (Pcompare p q Eq) with
    | Lt => true
    | _ => false
  end.

Fixpoint blt_int (n m : int) {struct n} : bool :=
  match n, m with
    | Z0, Zpos p => true
    | Zneg p, Z0 => true
    | Zneg p, Zpos q => true
    | Zneg p, Zneg q => blt_pos q p
    | Zpos p, Zpos q => blt_pos p q
    | _, _ => false
  end.

Lemma blt_pos_irrefl :
  forall p : positive, blt_pos p p = false.

Lemma blt_irrefl :
  forall a : int, blt_int a a = false.

Lemma blt_irrefl_Prop :
  forall a : int, ~ (blt_int a a = true).

Fixpoint beq_pos (p p´ : positive) {struct p} : bool :=
  match p, p´ with
    | x~0, x´~0 => andb true (beq_pos x x´)
    | p~1, p´~1 => andb true (beq_pos p p´)
    | 1, 1 => true
    | _, _ => false
  end %positive.

Fixpoint beq_int (z z´ : int) {struct z} : bool :=
  match z, z´ with
    | Z0, Z0 => true
    | Zpos p, Zpos p´ => beq_pos p p´
    | Zneg p, Zneg p´ => beq_pos p p´
    | _, _ => false
  end.

Lemma beq_int_true_eq : forall z z´ : int,
  beq_int z z´ = true -> z = z´.

Lemma beq_int_false_neq : forall z z´ : int,
  beq_int z z´ = false -> z <> z´.

Lemma eq_beq_int_true : forall z z´ : int,
  z = z´ -> beq_int z z´ = true.

Lemma neq_beq_int_false : forall z z´ : int,
  z <> z´ -> beq_int z z´ = false.

Lemma beq_int_dec : forall a b,
  {beq_int a b = true} + {beq_int a b = false}.

Ltac beq_case_tac x y :=
  let Hb := fresh "Hb" in
    (destruct (beq_int_dec x y) as [Hb | Hb]; trivial).

Tactic Notation "bint" "case" constr(i) constr (i´) := beq_case_tac i i´.