This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the Decision
type class.
Require Export proof_irrel.
Hint Extern 200 (
Decision _) =>
progress (
lazy beta) :
typeclass_instances.
Lemma dec_stable `{
Decision P} : ¬¬
P →
P.
Proof.
firstorder. Qed.
Lemma Is_true_reflect (
b :
bool) :
reflect b b.
Proof.
destruct b. by left. right. intros []. Qed.
Instance:
Injective (=) (↔)
Is_true.
Proof.
intros [] []; simpl; intuition. Qed.
We introduce decide_rel to avoid inefficienct computation due to eager
evaluation of propositions by vm_compute. This inefficiency occurs if
(x = y) := (f x = f y) as decide (x = y) evaluates to decide (f x = f y)
which then might lead to evaluation of f x and f y. Using decide_rel
we hide f under a lambda abstraction to avoid this unnecessary evaluation.
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.
Lemma decide_rel_correct {
A B} (
R :
A →
B →
Prop) `{∀
x y,
Decision (
R x y)}
(
x :
A) (
y :
B) :
decide_rel R x y =
decide (
R x y).
Proof.
done. Qed.
Lemma decide_True {
A} `{
Decision P} (
x y :
A) :
P → (
if decide P then x else y) =
x.
Proof.
by destruct (decide P). Qed.
Lemma decide_False {
A} `{
Decision P} (
x y :
A) :
¬
P → (
if decide P then x else y) =
y.
Proof.
by destruct (decide P). Qed.
Lemma decide_iff {
A}
P Q `{
Decision P,
Decision Q} (
x y :
A) :
(
P ↔
Q) → (
if decide P then x else y) = (
if decide Q then x else y).
Proof.
intros [??]. destruct (decide P), (decide Q); intuition. Qed.
The tactic destruct_decide destructs a sumbool dec. If one of the
components is double negated, it will try to remove the double negation.
Tactic Notation "
destruct_decide"
constr(
dec) "
as"
ident(
H) :=
destruct dec as [
H|
H];
try match type of H with
| ¬¬
_ =>
apply dec_stable in H
end.
Tactic Notation "
destruct_decide"
constr(
dec) :=
let H :=
fresh in destruct_decide dec as H.
The tactic case_decide performs case analysis on an arbitrary occurrence
of decide or decide_rel in the conclusion or hypotheses.
Tactic Notation "
case_decide" "
as"
ident(
Hd) :=
match goal with
|
H :
context [@
decide ?
P ?
dec] |-
_ =>
destruct_decide (@
decide P dec)
as Hd
|
H :
context [@
decide_rel _ _ ?
R ?
x ?
y ?
dec] |-
_ =>
destruct_decide (@
decide_rel _ _ R x y dec)
as Hd
| |-
context [@
decide ?
P ?
dec] =>
destruct_decide (@
decide P dec)
as Hd
| |-
context [@
decide_rel _ _ ?
R ?
x ?
y ?
dec] =>
destruct_decide (@
decide_rel _ _ R x y dec)
as Hd
end.
Tactic Notation "
case_decide" :=
let H :=
fresh in case_decide as H.
The tactic solve_decision uses Coq's decide equality tactic together
with instance resolution to automatically generate decision procedures.
Ltac solve_trivial_decision :=
match goal with
| |-
Decision (?
P) =>
apply _
| |-
sumbool ?
P (¬?
P) =>
change (
Decision P);
apply _
end.
Ltac solve_decision :=
intros;
first
[
solve_trivial_decision
|
unfold Decision;
decide equality;
solve_trivial_decision ].
The following combinators are useful to create Decision proofs in
combination with the refine tactic.
Notation swap_if S := (
match S with left H =>
right H |
right H =>
left H end).
Notation cast_if S := (
if S then left _ else right _).
Notation cast_if_and S1 S2 := (
if S1 then cast_if S2 else right _).
Notation cast_if_and3 S1 S2 S3 := (
if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_and4 S1 S2 S3 S4 :=
(
if S1 then cast_if_and3 S2 S3 S4 else right _).
Notation cast_if_and5 S1 S2 S3 S4 S5 :=
(
if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
Notation cast_if_and6 S1 S2 S3 S4 S5 S6 :=
(
if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
Notation cast_if_or S1 S2 := (
if S1 then left _ else cast_if S2).
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 _).
We can convert decidable propositions to booleans.
Definition bool_decide (
P :
Prop) {
dec :
Decision P} :
bool :=
if dec then true else false.
Lemma bool_decide_reflect P `{
dec :
Decision P} :
reflect P (
bool_decide P).
Proof.
unfold bool_decide. destruct dec. by left. by right. Qed.
Tactic Notation "
case_bool_decide" "
as"
ident (
Hd) :=
match goal with
|
H :
context [@
bool_decide ?
P ?
dec] |-
_ =>
destruct_decide (@
bool_decide_reflect P dec)
as Hd
| |-
context [@
bool_decide ?
P ?
dec] =>
destruct_decide (@
bool_decide_reflect P dec)
as Hd
end.
Tactic Notation "
case_bool_decide" :=
let H :=
fresh in case_bool_decide as H.
Lemma bool_decide_spec (
P :
Prop) {
dec :
Decision P} :
bool_decide P ↔
P.
Proof.
unfold bool_decide. by destruct dec. Qed.
Lemma bool_decide_unpack (
P :
Prop) {
dec :
Decision P} :
bool_decide P →
P.
Proof.
by rewrite bool_decide_spec. Qed.
Lemma bool_decide_pack (
P :
Prop) {
dec :
Decision P} :
P →
bool_decide P.
Proof.
by rewrite bool_decide_spec. Qed.
Lemma bool_decide_true (
P :
Prop) `{
Decision P} :
P →
bool_decide P =
true.
Proof.
by case_bool_decide. Qed.
Lemma bool_decide_false (
P :
Prop) `{
Decision P} : ¬
P →
bool_decide P =
false.
Proof.
by case_bool_decide. Qed.
Lemma bool_decide_iff (
P Q :
Prop) `{
Decision P,
Decision Q} :
(
P ↔
Q) →
bool_decide P =
bool_decide Q.
Proof.
repeat case_bool_decide; tauto. Qed.
Decidable Sigma types
Leibniz equality on Sigma types requires the equipped proofs to be
equal as Coq does not support proof irrelevance. For decidable we
propositions we define the type dsig P whose Leibniz equality is proof
irrelevant. That is ∀ x y : dsig P, x = y ↔ `x = `y. Due to the absence of
universe polymorpic definitions we also define a variant dsigS for types
in Set.
Definition dsig `(
P :
A →
Prop) `{∀
x :
A,
Decision (
P x)} :=
{
x |
bool_decide (
P x) }.
Definition dsigS {
A :
Set} (
P :
A →
Prop) `{∀
x :
A,
Decision (
P x)} :
Set :=
{
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 :=
x↾
bool_decide_pack _ p.
Lemma dsig_eq `(
P :
A →
Prop) `{∀
x,
Decision (
P x)}
(
x y :
dsig P) :
x =
y ↔ `
x = `
y.
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.
by apply dsig_eq. Qed.
Instances of Decision
Instances of Decision for operators of propositional logic.
Instance True_dec:
Decision True :=
left I.
Instance False_dec:
Decision False :=
right (
False_rect False).
Instance Is_true_dec b :
Decision (
Is_true b).
Proof.
destruct b; 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.
Instance iff_dec `(
P_dec :
Decision P) `(
Q_dec :
Decision Q) :
Decision (
P ↔
Q) :=
and_dec _ _.
Instances of Decision for common data types.
Instance bool_eq_dec (
x y :
bool) :
Decision (
x =
y).
Proof.
solve_decision. Defined.
Instance unit_eq_dec (
x y :
unit) :
Decision (
x =
y).
Proof.
solve_decision. Defined.
Instance prod_eq_dec `(
A_dec : ∀
x y :
A,
Decision (
x =
y))
`(
B_dec : ∀
x y :
B,
Decision (
x =
y)) (
x y :
A *
B) :
Decision (
x =
y).
Proof.
solve_decision. Defined.
Instance sum_eq_dec `(
A_dec : ∀
x y :
A,
Decision (
x =
y))
`(
B_dec : ∀
x y :
B,
Decision (
x =
y)) (
x y :
A +
B) :
Decision (
x =
y).
Proof.
solve_decision. Defined.
Instance curry_dec `(
P_dec : ∀ (
x :
A) (
y :
B),
Decision (
P x y))
p :
Decision (
curry P p) :=
match p as p return Decision (
curry P p)
with
| (
x,
y) =>
P_dec x y
end.
Instance uncurry_dec `(
P_dec : ∀ (
p :
A *
B),
Decision (
P p))
x y :
Decision (
uncurry P x y) :=
P_dec (
x,
y).
Instance sig_eq_dec `(
P :
A →
Prop) `{∀
x,
ProofIrrel (
P x)}
`{∀
x y :
A,
Decision (
x =
y)} (
x y :
sig P) :
Decision (
x =
y).
Proof.
refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. 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.