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
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.
- out : p
Instances
In most cases, we should not have global instances of Fact
; typeclass search is not an
advanced proof search engine, and adding any such instance has the potential to cause
slowdowns everywhere. We instead declare them as lemmata and make them local instances as required.
Equations
Instances For
Equations
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
#
In most of mathlib, we use the law of excluded middle (LEM) and the axiom of choice (AC) freely.
The Decidable
namespace contains versions of lemmas from the root namespace that explicitly
attempt to avoid the axiom of choice, usually by adding decidability assumptions on the inputs.
You can check if a lemma uses the axiom of choice by using #print axioms foo
and seeing if
Classical.choice
appears in the list.
Equations
Instances For
As mathlib is primarily classical,
if the type signature of a def
or lemma
does not require any Decidable
instances to state,
it is preferable not to introduce any Decidable
instances that are needed in the proof
as arguments, but rather to use the classical
tactic as needed.
In the other direction, when Decidable
instances do appear in the type signature,
it is better to use explicitly introduced ones rather than allowing Lean to automatically infer
classical ones, as these may cause instance mismatch errors later.
Equations
Instances For
Alias of Decidable.not_imp_symm
.
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_eq_of_ne
.
Alias of ne_of_ne_of_eq
.
Alias of eqRec_eq_cast
.
Alias of eqRec_heq_self
.
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 propext
.
The axiom of propositional extensionality. It asserts that if
propositions a
and b
are logically equivalent (that is, if a
can be proved from b
and vice
versa), then a
and b
are equal, meaning a
can be replaced with b
in all contexts.
The standard logical connectives provably respect propositional extensionality. However, an axiom is
needed for higher order expressions like P a
where P : Prop → Prop
is unknown, as well as for
equality. Propositional extensionality is intuitionistically valid.
Instances For
See IsEmpty.forall_iff
for the False
version.
Classical lemmas #
Any predicate p
is decidable classically.
Equations
Instances For
Any relation p
is decidable classically.
Equations
Instances For
Any type α
has decidable equality classically.
Equations
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.choose h) ⋯ else H0
Instances For
A version of byContradiction
that uses types instead of propositions.
Equations
Instances For
Classical.byContradiction'
is equivalent to lean's axiom Classical.choice
.
Equations
- Classical.choice_of_byContradiction' contra H = contra ⋯
Instances For
Alias of Classical.byCases
.
Alias of Classical.byContradiction
.
Alias of Classical.propComplete
.
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
- h.classicalRecOn H = H (Classical.choose h) ⋯
Instances For
Declarations about bounded quantifiers #
Membership #
Alias of ne_of_mem_of_not_mem
.
Alias of ne_of_mem_of_not_mem'
.
Alias of ne_of_mem_of_not_mem
.
Alias of ne_of_mem_of_not_mem
.
Alias of ne_of_mem_of_not_mem'
.
Alias of ne_of_mem_of_not_mem'
.
Alias of Bool.beq_eq_decide_eq
.