Properties of decidable propositions
Note: the following definition of
decidable can be used to
express the notion of decidability in computability theory only in
an axiom-free Coq (since a proof of
forall n, decidable (P n),
for
P a countable class of problems, induces by extraction the
existence of a (total) recursive algorithm
f such that
f(n)
evaluates to
true iff
P n, and since, conversely, a Coq proof
of termination of a recursive algorithm deciding
P n can be
extracted in turn into a proof of
forall n, decidable (P n)). In
the presence of axioms such as
Classical_prop.classic, it would
take a different meaning.
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.
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.