add bool_decide_negb

I had to move up all the Decision stuff since the new lemma needs the not_dec instance.

Proof by Yun-Sheng.

theories/decidable.v

@@ -85,6 +85,74 @@ Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
 Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
 Notation cast_if_not S := (if S then right _ else left _).
 
+(** * Instances of [Decision] *)
+(** Instances of [Decision] for operators of propositional logic. *)
+Global Instance True_dec: Decision True := left I.
+Global Instance False_dec: Decision False := right (False_rect False).
+Global Instance Is_true_dec b : Decision (Is_true b).
+Proof. destruct b; simpl; apply _. Defined.
+
+Section prop_dec.
+  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
+
+  Global Instance not_dec: Decision (¬P).
+  Proof. refine (cast_if_not P_dec); intuition. Defined.
+  Global Instance and_dec: Decision (P ∧ Q).
+  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
+  Global Instance or_dec: Decision (P ∨ Q).
+  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
+  Global Instance impl_dec: Decision (P → Q).
+  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
+End prop_dec.
+Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+  Decision (P ↔ Q) := and_dec _ _.
+
+(** Instances of [Decision] for common data types. *)
+Global Instance bool_eq_dec : EqDecision bool.
+Proof. solve_decision. Defined.
+Global Instance unit_eq_dec : EqDecision unit.
+Proof. solve_decision. Defined.
+Global Instance Empty_set_eq_dec : EqDecision Empty_set.
+Proof. solve_decision. Defined.
+Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
+Proof. solve_decision. Defined.
+Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
+Proof. solve_decision. Defined.
+
+Global Instance uncurry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+    Decision (uncurry P p) :=
+  match p as p return Decision (uncurry P p) with
+  | (x,y) => P_dec x y
+  end.
+
+Global Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
+  EqDecision (sig P).
+Proof.
+ refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
+Defined.
+
+(** Some laws for decidable propositions *)
+Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+
+Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
+  `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
+Solve Obligations with firstorder congruence.
+
+(** * Instances of [RelDecision] *)
+Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
+  RelDecision (flip R) := λ x y, decide_rel R y x.
+(** We do not declare this as an actual instance since Coq can unify [flip ?R]
+with any relation. Coq's standard library is carrying out the same approach for
+the [Reflexive], [Transitive], etc, instance of [flip]. *)
+Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
+
 (** We can convert decidable propositions to booleans. *)
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
@@ -135,6 +203,16 @@ Proof. apply bool_decide_eq_false. Qed.
 Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
 Proof. apply bool_decide_eq_false. Qed.
 
+Lemma bool_decide_not P `{Decision P} :
+  bool_decide (¬ P) = negb (bool_decide P).
+Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_or P Q `{Decision P, Decision Q} :
+  bool_decide (P ∨ Q) = bool_decide P || bool_decide Q.
+Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_and P Q `{Decision P, Decision Q} :
+  bool_decide (P ∧ Q) = bool_decide P && bool_decide Q.
+Proof. repeat case_bool_decide; intuition. Qed.
+
 (** The tactic [compute_done] solves the following kinds of goals:
 - Goals [P] where [Decidable P] can be derived.
 - Goals that compute to [True] or [x = x].
@@ -171,71 +249,3 @@ Proof. apply (sig_eq_pi _). Qed.
 Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
 Proof. apply dsig_eq; reflexivity. Qed.
-
-(** * Instances of [Decision] *)
-(** Instances of [Decision] for operators of propositional logic. *)
-Global Instance True_dec: Decision True := left I.
-Global Instance False_dec: Decision False := right (False_rect False).
-Global Instance Is_true_dec b : Decision (Is_true b).
-Proof. destruct b; simpl; apply _. Defined.
-
-Section prop_dec.
-  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
-
-  Global Instance not_dec: Decision (¬P).
-  Proof. refine (cast_if_not P_dec); intuition. Defined.
-  Global Instance and_dec: Decision (P ∧ Q).
-  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
-  Global Instance or_dec: Decision (P ∨ Q).
-  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
-  Global Instance impl_dec: Decision (P → Q).
-  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
-End prop_dec.
-Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
-  Decision (P ↔ Q) := and_dec _ _.
-
-(** Instances of [Decision] for common data types. *)
-Global Instance bool_eq_dec : EqDecision bool.
-Proof. solve_decision. Defined.
-Global Instance unit_eq_dec : EqDecision unit.
-Proof. solve_decision. Defined.
-Global Instance Empty_set_eq_dec : EqDecision Empty_set.
-Proof. solve_decision. Defined.
-Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
-Proof. solve_decision. Defined.
-Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
-Proof. solve_decision. Defined.
-
-Global Instance uncurry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
-    Decision (uncurry P p) :=
-  match p as p return Decision (uncurry P p) with
-  | (x,y) => P_dec x y
-  end.
-
-Global Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
-  EqDecision (sig P).
-Proof.
- refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
-Defined.
-
-(** Some laws for decidable propositions *)
-Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
-Proof. destruct (decide P); tauto. Qed.
-Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
-Proof. destruct (decide Q); tauto. Qed.
-Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
-Proof. destruct (decide P); tauto. Qed.
-Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
-Proof. destruct (decide Q); tauto. Qed.
-
-Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
-  `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
-Solve Obligations with firstorder congruence.
-
-(** * Instances of [RelDecision] *)
-Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
-  RelDecision (flip R) := λ x y, decide_rel R y x.
-(** We do not declare this as an actual instance since Coq can unify [flip ?R]
-with any relation. Coq's standard library is carrying out the same approach for
-the [Reflexive], [Transitive], etc, instance of [flip]. *)
-Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.