Module Decidableplus

Require Export DecidableClass.
Require Import Coqlib.

Ltac decide_goal := eapply Decidable_sound; reflexivity.


Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
  Decidable_witness := negb (@Decidable_witness P dP)
}.

Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
  Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
}.

Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
  Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
}.

Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
  Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
}.

Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
  Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
}.


Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y}) (x y: A) : Decidable (eq x y) := {|
  Decidable_witness := proj_sumbool (eqdec x y)
|}.

Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
  Decidable_witness := Bool.eqb x y
}.

Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
  Decidable_witness := beq_nat x y
}.

Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
  Decidable_witness := Pos.eqb x y
}.

Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
  Decidable_witness := Z.eqb x y
}.


Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
  Decidable_witness := Z.leb x y
}.

Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
  Decidable_witness := Z.ltb x y
}.

Program Instance Decidable_ge_Z : forall (x y: Z), Decidable (x >= y) := {
  Decidable_witness := Z.geb x y
}.

Program Instance Decidable_gt_Z : forall (x y: Z), Decidable (x > y) := {
  Decidable_witness := Z.gtb x y
}.

Program Instance Decidable_divides : forall (x y: Z), Decidable (x | y) := {
  Decidable_witness := Z.eqb y ((y / x) * x)%Z
}.


Program Instance Decidable_forall_in_list :
      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
      Decidable (forall x:A, In x l -> P x) := {
  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
}.

Program Instance Decidable_exists_in_list :
      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
      Decidable (exists x:A, In x l /\ P x) := {
  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
}.


Class Finite (T: Type) := {
  Finite_elements: list T;
  Finite_elements_spec: forall x:T, In x Finite_elements
}.


Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
}.

Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
}.


Program Instance Finite_bool : Finite bool := {
  Finite_elements := false :: true :: nil
}.

Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
  Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
}.

Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
  Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
}.