Require Export Coq.Classes.EquivDec.
Require Export Computable.
Require Import Option AutoIndTac.

Global Instance inst_equiv_cm A R `(EqDec A R) (x y : A) :
  Computable (x === y).
Proof.
  eapply H.
Defined.

Global Instance inst_eq_cm A `(EqDec A eq) (x y : A) : Computable (x = y)
  := H x y.

(* Additional instances for EqDec. *)
Definition option_eq_dec A `(EqDec A eq) (x y : option A) :
  {x = y} + {x ≠ y}.
Proof.
  decide equality. apply H.
Defined.

Global Instance inst_eq_dec_option A `(EqDec A eq) : EqDec (option A) eq := {
  equiv_dec := (option_eq_dec A _)
}.

(* For backwards compatibility, eq_dec uses equiv_dec for eq. *)
Definition eq_dec {A : Type} (x y : A) `{@EqDec A eq eq_equivalence} :
  {x = y} + {x ≠ y}.
Proof.
  apply H.
Defined.

Coercion sumbool_bool {A} {B} (x:{A} + {B}) : bool := if x then true else false.

Extraction Inline sumbool_bool.

Coercion sumbool_option {P:Prop} : {P}+{¬P} → option P.
destruct 1. eapply (Some p). eapply None.
Defined.

Extraction Inline sumbool_option.

Lemma sumbool_inversion {P:Prop} (p:{P}+{¬P}) x
  : sumbool_option p = Some x → p = left x.
Proof.
  intros. destruct p; simpl in × |- *; congruence.
Qed.

Coercion sum_option {T:Type} : (T+(T → False)) → option T.
destruct 1. eapply (Some t). eapply None.
Defined.

Lemma not_Is_true_eq_false : ∀ x:bool, ¬ Is_true x → x = false.
  intros [] A; firstorder.
Qed.

Tactic Notation "cases" "in" hyp(H) :=
  match type of H with
  | context [if sumbool_bool ?P then _ else _] ⇒ destruct P
  | context [if ?P then _ else _ ] ⇒
    match goal with
    | [ H' : Is_true (P) |- _ ] ⇒ rewrite (Is_true_eq_true _ H') in H
    | [ H' : ¬ Is_true (P) |- _ ] ⇒ rewrite (not_Is_true_eq_false _ H') in H
    end
  | context [ match (if ?P then _ else _) with _ ⇒ _ end ] ⇒
    match P with
    | decision_procedure _ ⇒
      let EQ := fresh "COND" in
      let NEQ := fresh "NOTCOND" in
      destruct P as [EQ|NEQ]; [ clear_trivial_eqs | try solve [exfalso; eauto] ]
    | _ ⇒
      let EQ := fresh "Heq" in
      let b := fresh "b" in
      remember P as b eqn:EQ; destruct b
    end
  | context [if ?P then _ else _] ⇒
    match P with
    | decision_procedure _ ⇒
      let EQ := fresh "COND" in
      let NEQ := fresh "NOTCOND" in
      destruct P as [EQ|NEQ]; [ clear_trivial_eqs | try solve [exfalso; eauto] ]
    | _ ⇒
      let EQ := fresh "Heq" in
      let b := fresh "b" in
      remember P as b eqn:EQ; destruct b
    end
  end.

Notation "B[ x ]" := (if [ x ] then true else false).

Tactic Notation "cases" :=
  match goal with
  | |- context [if sumbool_bool ?P then _ else _] ⇒ destruct P
  | |- context [ match (if ?P then true else false) with _ ⇒ _ end ] ⇒ destruct P
  | [ H' : Is_true (?P) |- context [if ?P then _ else _] ] ⇒
    rewrite (Is_true_eq_true _ H')
  | [ H' : ¬ Is_true (?P) |- context [if ?P then _ else _] ] ⇒
    rewrite (not_Is_true_eq_false _ H')
  | |- context [ if ?P then _ else _ ] ⇒
    match P with
    | negb (?P':decision_procedure _) ⇒
      let EQ := fresh "COND" in
      let NEQ := fresh "NOTCOND" in
      destruct P' as [EQ|NEQ]; [ clear_trivial_eqs | try solve [exfalso; eauto] ]
    | decision_procedure _ ⇒
      let EQ := fresh "COND" in
      let NEQ := fresh "NOTCOND" in
      destruct P as [EQ|NEQ]; [ clear_trivial_eqs | try solve [exfalso; eauto] ]
    end
  | |- context [ match ?P with _ ⇒ _ end ] ⇒
    let EQ := fresh "Heq" in
    let b := fresh "b" in
    remember P as b eqn:EQ; destruct b
  end; try clear_trivial_eqs.

Extraction Inline sum_option.

Notation "'mdo' X <= A ; B" := (bind (sumbool_option (@decision_procedure A _)) (fun X ⇒ B))
 (at level 200, X ident, A at level 100, B at level 200).

Lemma equiv_dec_refl A `(EqDec A eq) (a:A)
  : equiv_dec a a.
Proof.
  cbv. destruct H; eauto.
Qed.

Lemma equiv_dec_R A eq `(EqDec A eq) (a b:A)
  : equiv_dec a b → eq a b.
Proof.
  intros. cbv in H0. destruct (H a b); eauto; contradiction.
Qed.

Lemma equiv_dec_R_neg A eq `(EqDec A eq) (a b:A)
  : ¬equiv_dec a b → ¬eq a b.
Proof.
  intros. cbv in H0. destruct (H a b); eauto; contradiction.
Qed.

Lemma equiv_dec_false A `(EqDec A eq) (a b:A)
  : a ≠ b → false = equiv_dec a b.
Proof.
  intros. destruct (equiv_dec a b); simpl; congruence.
Qed.

Lemma false_equiv_dec A `(EqDec A eq) (a b:A)
  : false = equiv_dec a b → a ≠ b.
Proof.
  intros. destruct (equiv_dec a b); simpl in *; congruence.
Qed.

(* The following proof is from http://cstheory.stackexchange.com/questions/5158/prove-proof-irrelevance-in-coq *)

Let nu a b (p:a = b) : a = b :=
  match Bool.bool_dec a b with
    | left eqxy ⇒ eqxy
    | right neqxy ⇒ False_ind _ (neqxy p)
  end.
Lemma bool_pcanonical : ∀ (a b : bool) (p : a = b), p = nu a b p.
Proof.
  intros. case p. destruct a,b; (try discriminate p);
  unfold nu; simpl; reflexivity.
Qed.

Section PI.
  Variable X:Type.
  Context `{EqDec X eq}.

  Lemma equiv_dec_PI'
    : ∀ x, ∀ (p q :true = equiv_dec x x), p = q.
  Proof.
    intros. rewrite (bool_pcanonical _ _ q). rewrite (bool_pcanonical _ _ p).
    unfold nu. destruct (bool_dec true (equiv_dec x x)).
    reflexivity. congruence.
  Qed.

  Lemma equiv_dec_PI'_false
    : ∀ x y, ∀ (p q :false = equiv_dec x y), p = q.
  Proof.
    intros. rewrite (bool_pcanonical _ _ q). rewrite (bool_pcanonical _ _ p).
    unfold nu. destruct (equiv_dec x y); simpl.
    simpl in p. congruence. reflexivity.
  Qed.

  Lemma equiv_dec_PI
    : ∀ x, ∀ (p q :equiv_dec x x), p = q.
  Proof.
    intros x q.
    pose proof (@Is_true_eq_true (equiv_dec x x) q).
    revert q.
    rewrite H0. intros. destruct q. destruct q0. reflexivity.
  Qed.

End PI.

Ltac eqsubst_assumption H :=
  match goal with
    | [ H : _ |- _ ] ⇒ eapply equiv_dec_R in H
    | [ H : ¬ _ |- _ ] ⇒ eapply equiv_dec_R_neg in H
  end.

Tactic Notation "eqsubst" "in" hyp(H) :=
  eqsubst_assumption H.

Tactic Notation "eqsubst" :=
  progress (match goal with
    | [ H : _ |- _ ] ⇒ eqsubst_assumption H
  end).

Require Import List.

Global Instance inst_in_cm X (a:X) (L:list X) `(EqDec X eq) : Computable (In a L).
eapply In_dec. eapply equiv_dec.
Defined.

Lemma dneg_eq A `(EqDec A eq) (a b:A)
  : (¬ a ≠ b) → a = b.
Proof.
  intros. decide (a=b); firstorder.
Qed.

Global Instance inst_eq_dec_list {A} `{EqDec A eq} : EqDec (list A) eq.
hnf. eapply list_eq_dec. eapply equiv_dec.
Defined.

Lemma length_eq_dec {X} (L L' : list X)
  : length_eq L L' + (length_eq L L' → False).
Proof.
  decide(length L = length L').
  left. eapply length_length_eq; eauto.
  right. intro. eapply length_eq_length in X0. congruence.
Defined.

Set Implicit Arguments.

Let comp A (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
  eq_ind _ (fun a ⇒ a = y') eq2 _ eq1.

Remark trans_sym_eq : ∀ (A:Type) (x y:A) (u:x = y), comp u u = eq_refl y.
Proof.
  intros.
  case u; trivial.
Qed.

Let nu' (A:Type) `{EqDec A eq} (x y:A) (u:x = y) : x = y :=
  match equiv_dec x y with
  | left eqxy ⇒ eqxy
  | right neqxy ⇒ False_ind _ (neqxy u)
  end.

Let nu'_constant : ∀ (A:Type) `{EqDec A eq} (x y:A) (u v:x = y), nu' u = nu' v.
  intros.
  unfold nu'.
  destruct (equiv_dec x y) as [Heq|Hneq].
  reflexivity.
  case Hneq; trivial.
Qed.

Let nu'_inv (A:Type) `{EqDec A eq} (x y:A) (v:x = y) : x = y := comp (nu' (eq_refl x)) v.

Remark nu'_left_inv_on : ∀ (A:Type) `{EqDec A eq} (x y:A) (u:x = y), nu'_inv (nu' u) = u.
Proof.
  intros.
  case u; unfold nu'_inv.
  apply trans_sym_eq.
Qed.

Theorem dec_UIP : ∀ (A:Type) `{EqDec A eq} (x y:A) (p1 p2:x = y), p1 = p2.
Proof.
  intros.
  elim (@nu'_left_inv_on A equiv0 H) with (u := p1).
  elim (@nu'_left_inv_on A equiv0 H) with (u := p2).
  elim (@nu'_constant A equiv0 H x) with y p1 p2.
  reflexivity.
Qed.