Commit 02687b13 authored by Robbert's avatar Robbert

Merge branch 'ralf/bool_decide' into 'master'

add invserses of bool_decide_{true,false}

See merge request !81
parents 3b8eed3c 3db8e2f7
Pipeline #18099 passed with stage
in 8 minutes and 31 seconds
...@@ -112,14 +112,29 @@ Proof. rewrite bool_decide_spec; trivial. Qed. ...@@ -112,14 +112,29 @@ Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P. Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed. Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack : core. Hint Resolve bool_decide_pack : core.
Lemma bool_decide_true (P : Prop) `{Decision P} : P bool_decide P = true.
Proof. case_bool_decide; tauto. Qed. Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true P.
Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P bool_decide P = false. Proof. case_bool_decide; intuition discriminate. Qed.
Proof. case_bool_decide; tauto. Qed. Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ¬P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} : Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
(P Q) bool_decide P = bool_decide Q. (P Q) bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed. Proof. repeat case_bool_decide; tauto. Qed.
Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true P.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_true_2 P `{!Decision P}: P bool_decide P = true.
Proof. apply bool_decide_eq_true. Qed.
Lemma bool_decide_eq_false_1 P `{!Decision P}: bool_decide P = false ¬P.
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.
(** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2.
Notation bool_decide_false := bool_decide_eq_false_2.
(** * Decidable Sigma types *) (** * Decidable Sigma types *)
(** Leibniz equality on Sigma types requires the equipped proofs to be (** Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we equal as Coq does not support proof irrelevance. For decidable we
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment