Set Implicit Arguments.

Require Export Bool.
Require Import Morphisms List list_tools.

Class decidable_set X :=
  { eqX : X → X → bool;
    eqX_eq : ∀ x y, reflect (x = y) (eqX x y)}.

Infix " =?= " := eqX (at level 20).

Section decidable.
  Context { X : Set }.
  Context { D : decidable_set X }.

  Lemma eqX_correct : ∀ x y : X, eqX x y = true ↔ x = y.

  Lemma eqX_false : ∀ x y, eqX x y = false ↔ x ≠ y.

  Lemma X_dec (x y : X) : {x = y} + {x ≠ y}.

  Lemma eqX_refl x : eqX x x = true.

End decidable.

Global Instance NatNum : decidable_set nat :=
  Build_decidable_set PeanoNat.Nat.eqb_spec.

Global Instance Boolean : decidable_set bool.

Global Instance dec_prod A B :
  decidable_set A → decidable_set B → decidable_set (A×B).

Global Instance dec_sum A B :
  decidable_set A → decidable_set B → decidable_set (A+B).

Global Instance dec_option (A : Set) :
  decidable_set A → decidable_set (option A).

Class DecidableProp (P : Prop) := dec_prop: {P} + {¬ P}.
Arguments dec_prop : clear implicits.
Arguments dec_prop P {DecidableProp}.

Ltac case_prop p :=
  let D := fresh "D" in
  let hyp := fresh "hyp" in
  destruct (dec_prop p) as [hyp|hyp].

Global Instance DecidableProp_Eq (A : Set) (x y : A) :
  decidable_set A → DecidableProp (x=y).

Definition test (p : Prop) {d : DecidableProp p} : bool :=
  if (dec_prop p) then true else false.

Arguments test p {d}.

Lemma test_reflect p `{DecidableProp p} : reflect p (test p).

Remark Is_true_test p `{DecidableProp p} : Is_true (test p) ↔ p.
Global Instance Is_true_dec b : DecidableProp (Is_true b).
Remark Is_true_iff_eq_true b : Is_true b ↔ b = true.
Remark test_Is_true (p : bool) : test (Is_true p) = p.
Remark test_spec ϕ `{DecidableProp ϕ} : test ϕ = true ↔ ϕ.

Global Instance DecidableProp_neg p : DecidableProp p → DecidableProp (¬p).

Global Instance DecidableProp_conj p1 p2 :
  DecidableProp p1 → DecidableProp p2 → DecidableProp (p1 ∧ p2).

Global Instance DecidableProp_disj p1 p2 :
  DecidableProp p1 → DecidableProp p2 → DecidableProp (p1 ∨ p2).

Global Instance DecidableProp_impl p1 p2 :
  DecidableProp p1 → DecidableProp p2 → DecidableProp (p1 → p2).

Global Instance DecidableProp_iff p1 p2 :
  DecidableProp p1 → DecidableProp p2 → DecidableProp (p1 ↔ p2).

Global Instance DecidableProp_forall_bnd (A : Set) p l :
  (∀ a : A, DecidableProp (p a)) →
  DecidableProp (∀ a, a ∈ l → p a).

Global Instance DecidableProp_exists_bnd (A : Set) p l :
  (∀ a : A, DecidableProp (p a)) → DecidableProp (∃ a, a ∈ l ∧ p a).

Global Instance DecidableProp_equiv_prop p q :
  DecidableProp p → (p ↔ q) → DecidableProp q.

Ltac prove_proper :=
  match goal with
  | _ : _ |- Proper ((@equivalent _) ==> iff) _ ⇒
    let l := fresh "l" in
    let m := fresh "m" in
    let E := fresh "E" in
    intros l m E;setoid_rewrite E;reflexivity
  end.


Lemma andb_prop_iff x y: Is_true (x && y) ↔ Is_true x ∧ Is_true y.

Lemma orb_prop_iff x y: Is_true (x || y) ↔ Is_true x ∨ Is_true y.

Global Hint Rewrite andb_prop_iff orb_prop_iff : quotebool.

Ltac case_equal a b :=
  let E := fresh "E" in
  destruct (X_dec a b) as [E|E];
    [try rewrite E in *|].
Goal (∀ n, n = 0 ∨ n ≠ 0).

Ltac mega_simpl :=
  repeat (simpl in *;
           rewrite in_app_iff
           || match goal with
              | [ h : In _ (map _ _ ) |- _ ] ⇒
                let u1 := fresh "u" in
                apply in_map_iff in h as (u1&<-&h)
              | [ h : _ ∨ _ |- _ ] ⇒
                destruct h as [h|h]
              | [ h : In _ (_ ++ _ ) |- _ ] ⇒
                apply in_app_iff in h as [h|h]
              | [ _ : False |- _ ] ⇒ tauto
              | |- (∀ _, _) ⇒ intro
              | |- (_ → _) ⇒ intro
              | |- (In _ (map _ _)) ⇒ apply in_map_iff
              | |- (In _ (_ ++ _)) ⇒ apply in_app_iff
              | |- (_ ∧ _) ⇒ split
              | |- (_ ∨ False) ⇒ left
              | |- (∃ _, _) ⇒ eexists
              | [ h : In _ ?l |- In _ ?l ] ⇒ apply h
              | [ h : In _ ?l |- In _ ?l ∨ _ ] ⇒ left;apply h
              | [ h : In _ ?l |- _ ∨ In _ ?l ] ⇒ right;apply h
              end).

Ltac destruct_eqb x o :=
  let Ei := fresh "E" in
  let Ni := fresh "N" in
  let X := fresh "X" in
  destruct (PeanoNat.Nat.eq_dec x o) as [Ei |Ni];
    [pose proof Ei as X;apply PeanoNat.Nat.eqb_eq in X;
     try rewrite Ei in ×
    |pose proof Ni as X;apply PeanoNat.Nat.eqb_neq in X];
    try rewrite X in *;clear X;
    repeat (rewrite <- plus_n_O || rewrite PeanoNat.Nat.eqb_refl).
Ltac destruct_eqX_D D x o :=
  let Ei := fresh "E" in
  let Ni := fresh "N" in
  let X := fresh "X" in
  destruct (@X_dec _ D x o) as [Ei |Ni];
    [pose proof Ei as X;apply (@eqX_correct _ D)in X;
     try rewrite Ei in ×
    |pose proof Ni as X;apply (@eqX_false _ D) in X];
    repeat rewrite X in *;repeat rewrite (eqX_refl D) in *;clear X.
Ltac destruct_ltb x o :=
  let Li := fresh "L" in
  let X := fresh "X" in
  destruct (Compare_dec.le_lt_dec o x) as [Li |Li];
    [pose proof Li as X;apply PeanoNat.Nat.ltb_ge in X
    |pose proof Li as X;apply PeanoNat.Nat.ltb_lt in X];
    try rewrite X in *;clear X;
    repeat (rewrite <- plus_n_O || rewrite PeanoNat.Nat.eqb_refl).

Ltac destruct_leb o x :=
  let Li := fresh "L" in
  let X := fresh "X" in
  destruct (Compare_dec.le_lt_dec o x) as [Li |Li];
    [try rewrite (Compare_dec.leb_correct _ _ Li) in ×
    |try rewrite (Compare_dec.leb_correct_conv _ _ Li) in *];
    repeat (rewrite <- plus_n_O || rewrite PeanoNat.Nat.eqb_refl).

Ltac simpl_words :=
  try discriminate;
  match goal with
  | [h: [] = _ ++ _ :: _ |- _ ] ⇒ apply app_cons_not_nil in h;tauto
  | [h: _ ++ _ :: _ = [] |- _ ] ⇒ symmetry in h;apply app_cons_not_nil in h;tauto
  | [h: _ ++ [_] = _ ++ [_] |- _ ] ⇒
    let h' := fresh "h" in
    apply app_inj_tail in h as (h,h');
    try discriminate
  end.