Require Import ZArith.
Require Import ExtLib.Core.RelDec.

Set Implicit Arguments.
Set Strict Implicit.

Global Instance RelDec_zeq : RelDec (@eq Z) :=
{ rel_dec := Z.eqb }.

Global Instance RelDec_zlt : RelDec (Z.lt) :=
{ rel_dec := Z.ltb }.

Global Instance RelDec_zle : RelDec (Z.le) :=
{ rel_dec := Z.leb }.

Global Instance RelDec_zgt : RelDec (Z.gt) :=
{ rel_dec := Z.gtb }.

Global Instance RelDec_zge : RelDec (Z.ge) :=
{ rel_dec := Z.geb }.

Global Instance RelDec_Correct_zeq : RelDec_Correct RelDec_zeq.
Proof.
(* Goal: @RelDec_Correct Z Z.ge RelDec_zge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec Z (@eq Z) RelDec_zeq x y) true) (@eq Z x y) *)
  apply Z.eqb_eq.
Qed.

Global Instance RelDec_Correct_zlt : RelDec_Correct RelDec_zlt.
Proof.
(* Goal: @RelDec_Correct Z Z.ge RelDec_zge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec Z Z.lt RelDec_zlt x y) true) (Z.lt x y) *)
  generalize (Zlt_cases x y).
(* Goal: forall _ : if Z.ltb x y then Z.lt x y else Z.ge x y, iff (@eq bool (@rel_dec Z Z.lt RelDec_zlt x y) true) (Z.lt x y) *)
  unfold rel_dec. simpl.
(* Goal: forall _ : if Z.ltb x y then Z.lt x y else Z.ge x y, iff (@eq bool (Z.ltb x y) true) (Z.lt x y) *)
  destruct ((x <? y)%Z); intros; intuition; try congruence.
Qed.

Global Instance RelDec_Correct_zle : RelDec_Correct RelDec_zle.
Proof.
(* Goal: @RelDec_Correct Z Z.ge RelDec_zge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec Z Z.le RelDec_zle x y) true) (Z.le x y) *)
  generalize (Zle_cases x y).
(* Goal: forall _ : if Z.ltb x y then Z.lt x y else Z.ge x y, iff (@eq bool ((let (rel_dec) := RelDec_zlt in rel_dec) x y) true) (Z.lt x y) *)
  unfold rel_dec; simpl.
(* Goal: forall _ : if Z.leb x y then Z.le x y else Z.gt x y, iff (@eq bool (Z.leb x y) true) (Z.le x y) *)
  destruct ((x <=? y)%Z); intros; intuition; congruence.
Qed.

Global Instance RelDec_Correct_zgt : RelDec_Correct RelDec_zgt.
Proof.
(* Goal: @RelDec_Correct Z Z.ge RelDec_zge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec Z Z.gt RelDec_zgt x y) true) (Z.gt x y) *)
  generalize (Zgt_cases x y).
(* Goal: forall _ : if Z.ltb x y then Z.lt x y else Z.ge x y, iff (@eq bool ((let (rel_dec) := RelDec_zlt in rel_dec) x y) true) (Z.lt x y) *)
  unfold rel_dec; simpl.
(* Goal: forall _ : if Z.gtb x y then Z.gt x y else Z.le x y, iff (@eq bool (Z.gtb x y) true) (Z.gt x y) *)
  destruct ((x >? y)%Z); intros; intuition; congruence.
Qed.

Global Instance RelDec_Correct_zge : RelDec_Correct RelDec_zge.
Proof.
(* Goal: @RelDec_Correct Z Z.ge RelDec_zge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec Z Z.ge RelDec_zge x y) true) (Z.ge x y) *)
  generalize (Zge_cases x y).
(* Goal: forall _ : if Z.ltb x y then Z.lt x y else Z.ge x y, iff (@eq bool ((let (rel_dec) := RelDec_zlt in rel_dec) x y) true) (Z.lt x y) *)
  unfold rel_dec; simpl.
(* Goal: forall _ : if Z.geb x y then Z.ge x y else Z.lt x y, iff (@eq bool (Z.geb x y) true) (Z.ge x y) *)
  destruct ((x >=? y)%Z); intros; intuition; congruence.
Qed.
