decidable.v 2.89 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8
Require Export base.

Definition decide_rel {A B} (R : A  B  Prop) 
  {dec :  x y, Decision (R x y)} (x : A) (y : B) : Decision (R x y) := dec x y.

Ltac case_decide := 
  match goal with
  | H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
9 10
  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
     case (@decide_rel _ _ R x y dec) in *
Robbert Krebbers's avatar
Robbert Krebbers committed
11
  | |- context [@decide ?P ?dec] => case (@decide P dec) in *
12 13
  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
     case (@decide_rel _ _ R x y dec) in *
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17 18 19 20
  end.

Ltac solve_trivial_decision :=
  match goal with
  | [ |- Decision (?P) ] => apply _
  | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
  end.
21 22 23
Ltac solve_decision := 
  intros; first [ solve_trivial_decision
                | unfold Decision; decide equality; solve_trivial_decision ].
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27

Program Instance True_dec: Decision True := left _.
Program Instance False_dec: Decision False := right _.
Program Instance prod_eq_dec `(A_dec :  x y : A, Decision (x = y))
28
    `(B_dec :  x y : B, Decision (x = y)) :  x y : A * B, Decision (x = y) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30 31 32 33
  match A_dec (fst x) (fst y) with
  | left _ => match B_dec (snd x) (snd y) with left _ => left _ | right _ => right _ end
  | right _ => right _
  end.
Solve Obligations using (program_simpl; f_equal; firstorder).
34 35
Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
    Decision (P  Q) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40
  match P_dec with
  | left _ => match Q_dec with left _ => left _ | right _ => right _ end
  | right _ => right _
  end.
Solve Obligations using (program_simpl; tauto).
41 42
Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
    Decision (P  Q) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49 50 51 52 53 54 55
  match P_dec with
  | left _ => left _
  | right _ => match Q_dec with left _ => left _ | right _ => right _ end
  end.
Solve Obligations using (program_simpl; firstorder).

Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false.
Coercion Is_true : bool >-> Sortclass.
Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P  P.
Proof. unfold bool_decide. now destruct dec. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P  bool_decide P.
Proof. unfold bool_decide. now destruct dec. Qed.

56 57 58 59 60 61
Definition dsig `(P : A  Prop) `{ x : A, Decision (P x)} :=
  { x | bool_decide (P x) }.
Definition proj2_dsig `{ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
  bool_decide_unpack _ (proj2_sig x).
Definition dexist `{ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
  xbool_decide_pack _ p.
Robbert Krebbers's avatar
Robbert Krebbers committed
62

63 64
Lemma proj1_dsig_inj {A} (P : A  Prop) x (Px : P x) y (Py : P y) :
  xPx = yPy  x = y.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. now injection 1. Qed.
66 67
Lemma dsig_eq {A} (P : A  Prop) {dec :  x, Decision (P x)}
  (x y : { x | bool_decide (P x) }) : `x = `y  x = y.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Proof.
69 70 71 72 73
  intros H1. destruct x as [x Hx], y as [y Hy].
  simpl in *. subst. f_equal.
  revert Hx Hy. case (bool_decide (P y)).
  * now intros [] [].
  * easy.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Qed.