Basic logic properties #
This file is one of the earliest imports in mathlib.
Implementation notes #
Theorems that require decidability hypotheses are in the namespace
Classical versions are in the namespace
- 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.
Swaps two pairs of arguments to a function.
Declarations about propositional connectives #
Declarations about distributivity #
De Morgan's laws #
Declarations about equality #
Declarations about quantifiers #
Classical lemmas #
This function has the same type as
Exists.recOn, and can be used to case on an equality,
Exists.recOn can only eliminate into Prop, while this version eliminates into any universe
using the axiom of choice.
Declarations about bounded quantifiers #
A 'dite' producing a
Π a, σ a, applied to a value
a : α is a
dite that applies
either branch to