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
.
Equations
- decidableEq_of_subsingleton a b = isTrue (_ : a = b)
- 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.
For example, 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 ZMod.field
.
In particular, this class is not intended for turning the type class system into an automated theorem prover for first order logic.
Instances
Swaps two pairs of arguments to a function.
Equations
- Function.swap₂ f i₂ j₂ i₁ j₁ = f i₁ j₁ i₂ j₂
Instances For
Declarations about propositional connectives #
Declarations about implies
#
Alias of Decidable.not_imp_symm
.
Equations
Alias of the forward direction of and_rotate
.
Declarations about distributivity #
Declarations about iff
De Morgan's laws #
Declarations about equality #
Alias of ne_of_mem_of_not_mem
.
Alias of ne_of_mem_of_not_mem'
.
Declarations about quantifiers #
We intentionally restrict the type of α
in this lemma so that this is a safer to use in simp
than forall_swap
.
Alias of the reverse direction of exists_imp
.
See IsEmpty.exists_iff
for the False
version.
See IsEmpty.forall_iff
for the False
version.
Classical lemmas #
Any prop p
is decidable classically. A shorthand for classical.prop_decidable
.
Equations
- Classical.dec p = inferInstance
Instances For
Any type α
has decidable equality classically.
Equations
- Classical.decEq α = inferInstance
Instances For
Construct a function from a default value H0
, and a function to use if there exists a value
satisfying the predicate.
Equations
- Classical.existsCases H0 H = if h : ∃ a, p a then H (Classical.existsCases.proof_1 h) (Classical.existsCases.proof_2 h) else H0
Instances For
A version of Classical.indefiniteDescription
which is definitionally equal to a pair
Equations
- Classical.subtype_of_exists h = { val := Classical.choose h, property := Classical.subtype_of_exists.proof_1 h }
Instances For
A version of byContradiction
that uses types instead of propositions.
Equations
- Classical.byContradiction' H = Classical.choice (_ : Nonempty α)
Instances For
classical.byContradiction'
is equivalent to lean's axiom classical.choice
.
Equations
- Classical.choice_of_byContradiction' contra H = contra (_ : (α → False) → False)
Instances For
This function has the same type as Exists.recOn
, and can be used to case on an equality,
but Exists.recOn
can only eliminate into Prop, while this version eliminates into any universe
using the axiom of choice.
Equations
- Exists.classicalRecOn h H = H (Classical.choose h) (Exists.classicalRecOn.proof_1 h)
Instances For
Declarations about bounded quantifiers #
A two-argument function applied to two ite
s is a ite
of that two-argument function
applied to each of the branches.