Basic logic properties #
This file is one of the earliest imports in mathlib.
Implementation notes #
Theorems that require decidability hypotheses are in the namespace "decidable". Classical versions are in the namespace "classical".
In the presence of automation, this whole file may be unnecessary. On the other hand, maybe it is useful for writing automation.
Add an instance to "undo" coercion transitivity into a chain of coercions, because most simp lemmas are stated with respect to simple coercions and will not match when part of a chain.
- out : p
Wrapper for adding elementary propositions to the type class systems. Warning: this can easily be abused. See the rest of this docstring for details.
Certain propositions should not be treated as a class globally, but sometimes it is very convenient to be able to use the type class system in specific circumstances.
zmod p is a field if and only if
p is a prime number.
In order to be able to find this field instance automatically by type class search,
we have to turn
p.prime into an instance implicit assumption.
On the other hand, making
nat.prime a class would require a major refactoring of the library,
and it is questionable whether making
nat.prime a class is desirable at all.
The compromise is to add the assumption
[fact p.prime] to
In particular, this class is not intended for turning the type class system into an automated theorem prover for first order logic.
Declarations about propositional connectives #
Declarations about distributivity #
Transfer decidability of
a to decidability of
b, if the propositions are equivalent.
Important: this function should be used instead of
decidable b, because the
kernel will get stuck reducing the usage of
dec_trivial will not work.
Transfer decidability of
b to decidability of
a, if the propositions are equivalent.
This is the same as
decidable_of_iff but the iff is flipped.
De Morgan's laws #
Declarations about equality #
Declarations about quantifiers #
Classical lemmas #
Construct a function from a default value
H0, and a function to use if there exists a value
satisfying the predicate.
This function has the same type as
exists.rec_on, and can be used to case on an equality,
exists.rec_on can only eliminate into Prop, while this version eliminates into any universe
using the axiom of choice.
Declarations about bounded quantifiers #
classical.choice, lifts a (
nonempty instance to a (
classical.inhabited_of_nonempty already exists, in
core/init/classical.lean, but the assumption is not a type class argument,
which makes it unsuitable for some applications.
A 'dite' producing a
Π a, β a, applied to a value
x : α
dite that applies either branch to