Library Coq.Logic.Decidable
Properties of decidable propositions
Definition decidable (P:Prop) := P \/ ~ P.
Theorem dec_not_not : forall P:Prop, decidable P -> (~ P -> False) -> P.
Theorem dec_True : decidable True.
Theorem dec_False : decidable False.
Theorem dec_or :
forall A B:Prop, decidable A -> decidable B -> decidable (A \/ B).
Theorem dec_and :
forall A B:Prop, decidable A -> decidable B -> decidable (A /\ B).
Theorem dec_not : forall A:Prop, decidable A -> decidable (~ A).
Theorem dec_imp :
forall A B:Prop, decidable A -> decidable B -> decidable (A -> B).
Theorem dec_iff :
forall A B:Prop, decidable A -> decidable B -> decidable (A<->B).
Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.
Theorem not_or : forall A B:Prop, ~ (A \/ B) -> ~ A /\ ~ B.
Theorem not_and : forall A B:Prop, decidable A -> ~ (A /\ B) -> ~ A \/ ~ B.
Theorem not_imp : forall A B:Prop, decidable A -> ~ (A -> B) -> A /\ ~ B.
Theorem imp_simp : forall A B:Prop, decidable A -> (A -> B) -> ~ A \/ B.
Theorem not_iff :
forall A B:Prop, decidable A -> decidable B ->
~ (A <-> B) -> (A /\ ~ B) \/ (~ A /\ B).
Register dec_True as core.dec.True.
Register dec_False as core.dec.False.
Register dec_or as core.dec.or.
Register dec_and as core.dec.and.
Register dec_not as core.dec.not.
Register dec_imp as core.dec.imp.
Register dec_iff as core.dec.iff.
Register dec_not_not as core.dec.not_not.
Register not_not as core.dec.dec_not_not.
Register not_or as core.dec.not_or.
Register not_and as core.dec.not_and.
Register not_imp as core.dec.not_imp.
Register imp_simp as core.dec.imp_simp.
Register not_iff as core.dec.not_iff.
Results formulated with iff, used in FSetDecide.
Negation are expanded since it is unclear whether setoid rewrite
will always perform conversion.
We begin with lemmas that, when read from left to right,
can be understood as ways to eliminate uses of not.
Theorem not_true_iff : (True -> False) <-> False.
Theorem not_false_iff : (False -> False) <-> True.
Theorem not_not_iff : forall A:Prop, decidable A ->
(((A -> False) -> False) <-> A).
Theorem contrapositive : forall A B:Prop, decidable A ->
(((A -> False) -> (B -> False)) <-> (B -> A)).
Lemma or_not_l_iff_1 : forall A B: Prop, decidable A ->
((A -> False) \/ B <-> (A -> B)).
Lemma or_not_l_iff_2 : forall A B: Prop, decidable B ->
((A -> False) \/ B <-> (A -> B)).
Lemma or_not_r_iff_1 : forall A B: Prop, decidable A ->
(A \/ (B -> False) <-> (B -> A)).
Lemma or_not_r_iff_2 : forall A B: Prop, decidable B ->
(A \/ (B -> False) <-> (B -> A)).
Lemma imp_not_l : forall A B: Prop, decidable A ->
(((A -> False) -> B) <-> (A \/ B)).
Moving Negations Around:
We have four lemmas that, when read from left to right,
describe how to push negations toward the leaves of a
proposition and, when read from right to left, describe
how to pull negations toward the top of a proposition.
Theorem not_or_iff : forall A B:Prop,
(A \/ B -> False) <-> (A -> False) /\ (B -> False).
Lemma not_and_iff : forall A B:Prop,
(A /\ B -> False) <-> (A -> B -> False).
Lemma not_imp_iff : forall A B:Prop, decidable A ->
(((A -> B) -> False) <-> A /\ (B -> False)).
Lemma not_imp_rev_iff : forall A B : Prop, decidable A ->
(((A -> B) -> False) <-> (B -> False) /\ A).
Theorem dec_functional_relation :
forall (X Y : Type) (A:X->Y->Prop), (forall y y' : Y, decidable (y=y')) ->
(forall x, exists! y, A x y) -> forall x y, decidable (A x y).
With the following hint database, we can leverage auto to check
decidability of propositions.
#[global]
Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff
: decidable_prop.
solve_decidable using lib will solve goals about the
decidability of a proposition, assisted by an auxiliary
database of lemmas. The database is intended to contain
lemmas stating the decidability of base propositions,
(e.g., the decidability of equality on a particular
inductive type).
Tactic Notation "solve_decidable" "using" ident(db) :=
match goal with
| |- decidable _ =>
solve [ auto 100 with decidable_prop db ]
end.
Tactic Notation "solve_decidable" :=
solve_decidable using core.