eq_dec.v

From Coq Require Import Nat List Extraction. 
Import ListNotations.

Definition EqDec (A:Type) := forall (a b : A), {a = b} + {a <> b}.
Existing Class EqDec.
Definition eq_dec {A : Type} `{EqDec A} : EqDec A := _.

(* Defining these is somewhat annoying since you need to prove their correctness at the same time. *)
Program Instance eq_dec_option {A} {H : EqDec A} : EqDec (option A) := fun a b => match a, b with
  None, None => left _
| Some a, Some b => if eq_dec a b then left _ else right _
| _, _ => right _ end.
Next Obligation.
  intros ->. destruct b as [b|].
  - now eapply H0.
  - now eapply H1.
Qed.
Next Obligation.
  split.
  - intros a' b' [H1 H2]. congruence.
  - intros [H1 H2]. congruence.  
Qed. 
Next Obligation.
  split.
  - intros a' b' [H1 H2]. congruence.
  - intros [H1 H2]. congruence.  
Qed.

(* Here it's easier, someone already did the work for us. *)
Program Instance eq_dec_nat : EqDec nat := fun a b => match Nat.eqb a b with true => left _ | false => right _ end.
Next Obligation.
  symmetry in Heq_anonymous. now eapply PeanoNat.Nat.eqb_eq in Heq_anonymous.
Qed.
Next Obligation.
  intros H%PeanoNat.Nat.eqb_eq. congruence.
Qed.

(* We can use the [list_eq_dec] from the StdLib, but we massage it into an instance. *)
Instance eq_dec_list {A} {H : EqDec A} : EqDec (list A) := list_eq_dec H.

(* Typeclass resolution find the deciders for us. *)
Definition foo : EqDec (list (option nat)) := _.
(* The computation result is a bit messy, the key is that it reduces to a constructor. *)
Compute (eq_dec [Some 4] [Some 5]).
(* We can even make the extraction turn our [sumbool]s into OCaml [bool]s. *)
Extract Inductive sumbool => "bool" [ "true" "false" ].
(* The extraction removes all the messy proofs from above. *)
Recursive Extraction foo.