Require Import Coq.PArith.BinPos.
Require Import ExtLib.Core.RelDec.

Set Implicit Arguments.
Set Strict Implicit.

(* Decidable Instances *)
Global Instance RelDec_peq : RelDec (@eq positive) :=
{ rel_dec := Pos.eqb }.

Global Instance RelDec_plt : RelDec (Pos.lt) :=
{ rel_dec := Pos.ltb }.

Global Instance RelDec_ple : RelDec (Pos.le) :=
{ rel_dec := Pos.leb }.

Global Instance RelDec_pgt : RelDec (Pos.gt) :=
{ rel_dec := fun x y => negb (Pos.leb x y) }.

Global Instance RelDec_pge : RelDec (Pos.ge) :=
{ rel_dec := fun x y => negb (Pos.ltb x y) }.

Global Instance RelDec_Correct_peq : RelDec_Correct RelDec_peq.
Proof.
(* Goal: @RelDec_Correct positive Pos.ge RelDec_pge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec positive (@eq positive) RelDec_peq x y) true) (@eq positive x y) *)
  apply Pos.eqb_eq.
Qed.

Global Instance RelDec_Correct_plt : RelDec_Correct RelDec_plt.
Proof.
(* Goal: forall x y : positive, iff (@eq bool (@rel_dec positive Pos.ge RelDec_pge x y) true) (Pos.ge x y) *)
  constructor; simpl; intros.
(* Goal: iff (@eq bool (@rel_dec positive Pos.lt RelDec_plt x y) true) (Pos.lt x y) *)
  apply Pos.ltb_lt.
Qed.

Global Instance RelDec_Correct_ple : RelDec_Correct RelDec_ple.
Proof.
(* Goal: forall x y : positive, iff (@eq bool (@rel_dec positive Pos.ge RelDec_pge x y) true) (Pos.ge x y) *)
  constructor; simpl; intros.
(* Goal: iff (@eq bool (@rel_dec positive Pos.le RelDec_ple x y) true) (Pos.le x y) *)
  apply Pos.leb_le.
Qed.

Global Instance RelDec_Correct_pgt : RelDec_Correct RelDec_pgt.
Proof.
(* Goal: forall x y : positive, iff (@eq bool (@rel_dec positive Pos.ge RelDec_pge x y) true) (Pos.ge x y) *)
  constructor; simpl; intros.
(* Goal: iff (@eq bool (@rel_dec positive Pos.ge RelDec_pge x y) true) (Pos.ge x y) *)
  unfold rel_dec; simpl.
(* Goal: iff (@eq bool (negb (Pos.leb x y)) true) (Pos.gt x y) *)
  rewrite <- Pos.ltb_antisym. rewrite Pos.ltb_lt.
(* Goal: iff (Pos.lt y x) (Pos.gt x y) *)
  intuition; [ apply Pos.lt_gt | apply Pos.gt_lt ]; auto.
Qed.

Global Instance RelDec_Correct_pge : RelDec_Correct RelDec_pge.
Proof.
(* Goal: @RelDec_Correct positive Pos.ge RelDec_pge *)
  constructor; simpl. intros.
(* Goal: iff (@eq bool (@rel_dec positive Pos.ge RelDec_pge x y) true) (Pos.ge x y) *)
  unfold rel_dec; simpl.
(* Goal: iff (@eq bool (negb (Pos.ltb x y)) true) (Pos.ge x y) *)
  rewrite <- Pos.leb_antisym. rewrite Pos.leb_le.
(* Goal: iff (Pos.le y x) (Pos.ge x y) *)
  intuition; [ apply Pos.le_ge | apply Pos.ge_le ]; auto.
Qed.

Export Coq.PArith.BinPos.
