Empty.elim : Empty → C
says that a value of any type can be constructed from
Empty
. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of Empty.rec
.
Instances For
Decidable equality for Empty
Equations
- instDecidableEqEmpty a = a.elim
PEmpty.elim : Empty → C
says that a value of any type can be constructed from
PEmpty
. This can be thought of as a compiler-checked assertion that a code path is unreachable.
This is a non-dependent variant of PEmpty.rec
.
Equations
Instances For
Decidable equality for PEmpty
Equations
- instDecidableEqPEmpty a = a.elim
Store a value in a thunk. Note that the value has already been computed, so there is no laziness.
Equations
- Thunk.pure a = { fn := fun (x : Unit) => a }
Instances For
Forces a thunk to extract the value. This will cache the result, so a second call to the same function will return the value in O(1) instead of calling the stored getter function.
Instances For
definitions #
If and only if, or logical bi-implication. a ↔ b
means that a
implies b
and vice versa.
By propext
, this implies that a
and b
are equal and hence any expression involving a
is equivalent to the corresponding expression with b
instead.
- intro :: (
- mp : a → b
Modus ponens for if and only if. If
a ↔ b
anda
, thenb
. - mpr : b → a
Modus ponens for if and only if, reversed. If
a ↔ b
andb
, thena
. - )
Instances For
If and only if, or logical bi-implication. a ↔ b
means that a
implies b
and vice versa.
By propext
, this implies that a
and b
are equal and hence any expression involving a
is equivalent to the corresponding expression with b
instead.
Equations
- «term_<->_» = Lean.ParserDescr.trailingNode `«term_<->_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <-> ") (Lean.ParserDescr.cat `term 21))
Instances For
If and only if, or logical bi-implication. a ↔ b
means that a
implies b
and vice versa.
By propext
, this implies that a
and b
are equal and hence any expression involving a
is equivalent to the corresponding expression with b
instead.
Equations
- «term_↔_» = Lean.ParserDescr.trailingNode `«term_↔_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 21))
Instances For
Sum α β
, or α ⊕ β
, is the disjoint union of types α
and β
.
An element of α ⊕ β
is either of the form .inl a
where a : α
,
or .inr b
where b : β
.
- inl: {α : Type u} → {β : Type v} → α → α ⊕ β
Left injection into the sum type
α ⊕ β
. Ifa : α
then.inl a : α ⊕ β
. - inr: {α : Type u} → {β : Type v} → β → α ⊕ β
Right injection into the sum type
α ⊕ β
. Ifb : β
then.inr b : α ⊕ β
.
Instances For
Sum α β
, or α ⊕ β
, is the disjoint union of types α
and β
.
An element of α ⊕ β
is either of the form .inl a
where a : α
,
or .inr b
where b : β
.
Equations
- «term_⊕_» = Lean.ParserDescr.trailingNode `«term_⊕_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 30))
Instances For
PSum α β
, or α ⊕' β
, is the disjoint union of types α
and β
.
It differs from α ⊕ β
in that it allows α
and β
to have arbitrary sorts
Sort u
and Sort v
, instead of restricting to Type u
and Type v
. This means
that it can be used in situations where one side is a proposition, like True ⊕' Nat
.
The reason this is not the default is that this type lives in the universe Sort (max 1 u v)
,
which can cause problems for universe level unification,
because the equation max 1 u v = ?u + 1
has no solution in level arithmetic.
PSum
is usually only used in automation that constructs sums of arbitrary types.
- inl: {α : Sort u} → {β : Sort v} → α → α ⊕' β
Left injection into the sum type
α ⊕' β
. Ifa : α
then.inl a : α ⊕' β
. - inr: {α : Sort u} → {β : Sort v} → β → α ⊕' β
Right injection into the sum type
α ⊕' β
. Ifb : β
then.inr b : α ⊕' β
.
Instances For
PSum α β
, or α ⊕' β
, is the disjoint union of types α
and β
.
It differs from α ⊕ β
in that it allows α
and β
to have arbitrary sorts
Sort u
and Sort v
, instead of restricting to Type u
and Type v
. This means
that it can be used in situations where one side is a proposition, like True ⊕' Nat
.
The reason this is not the default is that this type lives in the universe Sort (max 1 u v)
,
which can cause problems for universe level unification,
because the equation max 1 u v = ?u + 1
has no solution in level arithmetic.
PSum
is usually only used in automation that constructs sums of arbitrary types.
Equations
- «term_⊕'_» = Lean.ParserDescr.trailingNode `«term_⊕'_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕' ") (Lean.ParserDescr.cat `term 30))
Instances For
Sigma β
, also denoted Σ a : α, β a
or (a : α) × β a
, is the type of dependent pairs
whose first component is a : α
and whose second component is b : β a
(so the type of the second component can depend on the value of the first component).
It is sometimes known as the dependent sum type, since it is the type level version
of an indexed summation.
- fst : α
The first component of a dependent pair. If
p : @Sigma α β
thenp.1 : α
. - snd : β self.fst
The second component of a dependent pair. If
p : Sigma β
thenp.2 : β p.1
.
Instances For
PSigma β
, also denoted Σ' a : α, β a
or (a : α) ×' β a
, is the type of dependent pairs
whose first component is a : α
and whose second component is b : β a
(so the type of the second component can depend on the value of the first component).
It differs from Σ a : α, β a
in that it allows α
and β
to have arbitrary sorts
Sort u
and Sort v
, instead of restricting to Type u
and Type v
. This means
that it can be used in situations where one side is a proposition, like (p : Nat) ×' p = p
.
The reason this is not the default is that this type lives in the universe Sort (max 1 u v)
,
which can cause problems for universe level unification,
because the equation max 1 u v = ?u + 1
has no solution in level arithmetic.
PSigma
is usually only used in automation that constructs pairs of arbitrary types.
- fst : α
The first component of a dependent pair. If
p : @Sigma α β
thenp.1 : α
. - snd : β self.fst
The second component of a dependent pair. If
p : Sigma β
thenp.2 : β p.1
.
Instances For
Existential quantification. If p : α → Prop
is a predicate, then ∃ x : α, p x
asserts that there is some x
of type α
such that p x
holds.
To create an existential proof, use the exists
tactic,
or the anonymous constructor notation ⟨x, h⟩
.
To unpack an existential, use cases h
where h
is a proof of ∃ x : α, p x
,
or let ⟨x, hx⟩ := h
where `.
Because Lean has proof irrelevance, any two proofs of an existential are definitionally equal. One consequence of this is that it is impossible to recover the witness of an existential from the mere fact of its existence. For example, the following does not compile:
example (h : ∃ x : Nat, x = x) : Nat :=
let ⟨x, _⟩ := h -- fail, because the goal is `Nat : Type`
x
The error message recursor 'Exists.casesOn' can only eliminate into Prop
means
that this only works when the current goal is another proposition:
example (h : ∃ x : Nat, x = x) : True :=
let ⟨x, _⟩ := h -- ok, because the goal is `True : Prop`
trivial
- intro: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
Existential introduction. If
a : α
andh : p a
, then⟨a, h⟩
is a proof that∃ x : α, p x
.
Instances For
Auxiliary type used to compile for x in xs
notation.
This is the return value of the body of a ForIn
call,
representing the body of a for loop. It can be:
.yield (a : α)
, meaning that we should continue the loop anda
is the new state..yield
is produced bycontinue
and reaching the bottom of the loop body..done (a : α)
, meaning that we should early-exit the loop with statea
..done
is produced by calls tobreak
orreturn
in the loop,
Instances For
Equations
- instInhabitedForInStep = { default := ForInStep.done default }
ForIn m ρ α
is the typeclass which supports for x in xs
notation.
Here xs : ρ
is the type of the collection to iterate over, x : α
is the element type which is made available inside the loop, and m
is the monad
for the encompassing do
block.
forIn x b f : m β
runs a for-loop in the monadm
with additional stateβ
. This traverses over the "contents" ofx
, and passes the elementsa : α
tof : α → β → m (ForInStep β)
.b : β
is the initial state, and the return value off
is the new state as well as a directive.done
or.yield
which indicates whether to abort early or continue iteration.The expression
let mut b := ... for x in xs do b ← foo x b
in a
do
block is syntactic sugar for:let b := ... let b ← forIn xs b (fun x b => do let b ← foo x b return .yield b)
(Here
b
corresponds to the variables mutated in the loop.)
Instances
ForIn' m ρ α d
is a variation on the ForIn m ρ α
typeclass which supports the
for h : x in xs
notation. It is the same as for x in xs
except that h : x ∈ xs
is provided as an additional argument to the body of the for-loop.
- forIn' : {β : Type u₁} → [inst : Monad m] → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β
forIn' x b f : m β
runs a for-loop in the monadm
with additional stateβ
. This traverses over the "contents" ofx
, and passes the elementsa : α
along with a proof thata ∈ x
tof : (a : α) → a ∈ x → β → m (ForInStep β)
.b : β
is the initial state, and the return value off
is the new state as well as a directive.done
or.yield
which indicates whether to abort early or continue iteration.
Instances
Auxiliary type used to compile do
notation. It is used when compiling a do block
nested inside a combinator like tryCatch
. It encodes the possible ways the
block can exit:
pure (a : α) s
means that the block exited normally with return valuea
.return (b : β) s
means that the block exited via areturn b
early-exit command.break s
means thatbreak
was called, meaning that we should exit from the containing loop.continue s
means thatcontinue
was called, meaning that we should continue to the next iteration of the containing loop.
All cases return a value s : σ
which bundles all the mutable variables of the do-block.
- pure: {α β σ : Type u} → α → σ → DoResultPRBC α β σ
pure (a : α) s
means that the block exited normally with return valuea
- return: {α β σ : Type u} → β → σ → DoResultPRBC α β σ
- break: {α β σ : Type u} → σ → DoResultPRBC α β σ
- continue: {α β σ : Type u} → σ → DoResultPRBC α β σ
Instances For
Auxiliary type used to compile do
notation. It is the same as
DoResultPRBC α β σ
except that break
and continue
are not available
because we are not in a loop context.
- pure: {α β σ : Type u} → α → σ → DoResultPR α β σ
pure (a : α) s
means that the block exited normally with return valuea
- return: {α β σ : Type u} → β → σ → DoResultPR α β σ
Instances For
Auxiliary type used to compile do
notation. It is an optimization of
DoResultPRBC PEmpty PEmpty σ
to remove the impossible cases,
used when neither pure
nor return
are possible exit paths.
- break: {σ : Type u} → σ → DoResultBC σ
- continue: {σ : Type u} → σ → DoResultBC σ
Instances For
Auxiliary type used to compile do
notation. It is an optimization of
either DoResultPRBC α PEmpty σ
or DoResultPRBC PEmpty α σ
to remove the
impossible case, used when either pure
or return
is never used.
- pureReturn: {α σ : Type u} → α → σ → DoResultSBC α σ
- break: {α σ : Type u} → σ → DoResultSBC α σ
- continue: {α σ : Type u} → σ → DoResultSBC α σ
Instances For
x ≈ y
says that x
and y
are equivalent. Because this is a typeclass,
the notion of equivalence is type-dependent.
Equations
- «term_≈_» = Lean.ParserDescr.trailingNode `«term_≈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))
Instances For
set notation #
Notation type class for the strict subset relation ⊂
.
- SSubset : α → α → Prop
Strict subset relation:
a ⊂ b
Instances
Subset relation: a ⊆ b
Equations
- «term_⊆_» = Lean.ParserDescr.trailingNode `«term_⊆_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ ") (Lean.ParserDescr.cat `term 51))
Instances For
Strict subset relation: a ⊂ b
Equations
- «term_⊂_» = Lean.ParserDescr.trailingNode `«term_⊂_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊂ ") (Lean.ParserDescr.cat `term 51))
Instances For
Superset relation: a ⊇ b
Equations
- «term_⊇_» = Lean.ParserDescr.trailingNode `«term_⊇_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊇ ") (Lean.ParserDescr.cat `term 51))
Instances For
Strict superset relation: a ⊃ b
Equations
- «term_⊃_» = Lean.ParserDescr.trailingNode `«term_⊃_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊃ ") (Lean.ParserDescr.cat `term 51))
Instances For
a ∪ b
is the union ofa
and b
.
Equations
- «term_∪_» = Lean.ParserDescr.trailingNode `«term_∪_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∪ ") (Lean.ParserDescr.cat `term 66))
Instances For
a ∩ b
is the intersection ofa
and b
.
Equations
- «term_∩_» = Lean.ParserDescr.trailingNode `«term_∩_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∩ ") (Lean.ParserDescr.cat `term 71))
Instances For
a \ b
is the set difference of a
and b
,
consisting of all elements in a
that are not in b
.
Equations
- «term_\_» = Lean.ParserDescr.trailingNode `«term_\_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\ ") (Lean.ParserDescr.cat `term 71))
Instances For
collections #
EmptyCollection α
is the typeclass which supports the notation ∅
, also written as {}
.
- emptyCollection : α
∅
or{}
is the empty set or empty collection. It is supported by theEmptyCollection
typeclass.
Instances
∅
or {}
is the empty set or empty collection.
It is supported by the EmptyCollection
typeclass.
Equations
- «term{}» = Lean.ParserDescr.node `«term{}» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{") (Lean.ParserDescr.symbol "}"))
Instances For
∅
or {}
is the empty set or empty collection.
It is supported by the EmptyCollection
typeclass.
Equations
- «term∅» = Lean.ParserDescr.node `«term∅» 1024 (Lean.ParserDescr.symbol "∅")
Instances For
Task α
is a primitive for asynchronous computation.
It represents a computation that will resolve to a value of type α
,
possibly being computed on another thread. This is similar to Future
in Scala,
Promise
in Javascript, and JoinHandle
in Rust.
The tasks have an overridden representation in the runtime.
- pure :: (
- get : α
- )
Instances For
Task priority. Tasks with higher priority will always be scheduled before ones with lower priority.
Equations
Instances For
The default priority for spawned tasks, also the lowest priority: 0
.
Equations
Instances For
The highest regular priority for spawned tasks: 8
.
Spawning a task with a priority higher than Task.Priority.max
is not an error but
will spawn a dedicated worker for the task, see Task.Priority.dedicated
.
Regular priority tasks are placed in a thread pool and worked on according to the priority order.
Equations
Instances For
Any priority higher than Task.Priority.max
will result in the task being scheduled
immediately on a dedicated thread. This is particularly useful for long-running and/or
I/O-bound tasks since Lean will by default allocate no more non-dedicated workers
than the number of cores to reduce context switches.
Equations
Instances For
spawn fn : Task α
constructs and immediately launches a new task for
evaluating the function fn () : α
asynchronously.
prio
, if provided, is the priority of the task.
Equations
- Task.spawn fn prio = { get := fn () }
Instances For
map f x
maps function f
over the task x
: that is, it constructs
(and immediately launches) a new task which will wait for the value of x
to
be available and then calls f
on the result.
prio
, if provided, is the priority of the task.
If sync
is set to true, f
is executed on the current thread if x
has already finished.
Instances For
bind x f
does a monad "bind" operation on the task x
with function f
:
that is, it constructs (and immediately launches) a new task which will wait
for the value of x
to be available and then calls f
on the result,
resulting in a new task which is then run for a result.
prio
, if provided, is the priority of the task.
If sync
is set to true, f
is executed on the current thread if x
has already finished.
Equations
- x.bind f prio sync = { get := (f x.get).get }
Instances For
NonScalar
is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using unsafeCast
. It is somewhat
analogous to C void*
in usage, but the type itself is not special.
- val : Nat
You should not use this function
Instances For
PNonScalar
is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using unsafeCast
. It is somewhat
analogous to C void*
in usage, but the type itself is not special.
This is the universe-polymorphic version of PNonScalar
; it is preferred to use
NonScalar
instead where applicable.
- mk: Nat → PNonScalar
You should not use this function
Instances For
Boolean operators #
x != y
is boolean not-equal. It is the negation of x == y
which is supplied by
the BEq
typeclass.
Unlike x ≠ y
(which is notation for Ne x y
), this is Bool
valued instead of
Prop
valued. It is mainly intended for programming applications.
Equations
- «term_!=_» = Lean.ParserDescr.trailingNode `«term_!=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 51))
Instances For
LawfulBEq α
is a typeclass which asserts that the BEq α
implementation
(which supplies the a == b
notation) coincides with logical equality a = b
.
In other words, a == b
implies a = b
, and a == a
is true.
If
a == b
evaluates totrue
, thena
andb
are equal in the logic.==
is reflexive, that is,(a == a) = true
.
Instances
Logical connectives and equality #
If h : α = β
is a proof of type equality, then h.mp : α → β
is the induced
"cast" operation, mapping elements of α
to elements of β
.
You can prove theorems about the resulting element by induction on h
, since
rfl.mp
is definitionally the identity function.
Equations
- h.mp a = h ▸ a
Instances For
If h : α = β
is a proof of type equality, then h.mpr : β → α
is the induced
"cast" operation in the reverse direction, mapping elements of β
to elements of α
.
You can prove theorems about the resulting element by induction on h
, since
rfl.mpr
is definitionally the identity function.
Equations
- h.mpr b = ⋯ ▸ b
Instances For
a ≠ b
, or Ne a b
is defined as ¬ (a = b)
or a = b → False
,
and asserts that a
and b
are not equal.
Equations
- «term_≠_» = Lean.ParserDescr.trailingNode `«term_≠_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `term 51))
Instances For
Exists #
Decidable #
Equations
Instances For
Equations
Instances For
Similar to decide
, but uses an explicit instance
Equations
- toBoolUsing d = decide p
Instances For
Synonym for dite
(dependent if-then-else). We can construct an element q
(of any sort, not just a proposition) by cases on whether p
is true or false,
provided p
is decidable.
Equations
- Decidable.byCases h1 h2 = h1 h
- Decidable.byCases h1 h2 = h2 h
Instances For
Transfer a decidability proof across an equivalence of propositions.
Equations
- decidable_of_decidable_of_iff h = if hp : p then isTrue ⋯ else isFalse ⋯
Instances For
Transfer a decidability proof across an equality of propositions.
Equations
Instances For
if-then-else expression theorems #
Split an if-then-else into cases. The split
tactic is generally easier to use than this theorem.
Equations
- iteInduction hpos hneg = hpos h
- iteInduction hpos hneg = hneg h
Instances For
Auxiliary definition for generating compact noConfusion
for enumeration types
Equations
- noConfusionTypeEnum f P x y = Decidable.casesOn (inst (f x) (f y)) (fun (x : ¬f x = f y) => P) fun (x : f x = f y) => P → P
Instances For
Auxiliary definition for generating compact noConfusion
for enumeration types
Equations
- noConfusionEnum f h = Decidable.casesOn (inst (f x) (f y)) (fun (h' : ¬f x = f y) => ⋯.elim) fun (x : f x = f y) (x : P) => x
Instances For
Inhabited #
Equations
- instInhabitedNonScalar = { default := { val := default } }
Equations
- instInhabitedPNonScalar = { default := PNonScalar.mk default }
Equations
- instInhabitedForInStep_1 = { default := ForInStep.done default }
Equations
- instInhabitedTrue = { default := True.intro }
Subsingleton #
A "subsingleton" is a type with at most one element.
In other words, it is either empty, or has a unique element.
All propositions are subsingletons because of proof irrelevance, but some other types
are subsingletons as well and they inherit many of the same properties as propositions.
Subsingleton α
is a typeclass, so it is usually used as an implicit argument and
inferred by typeclass inference.
- intro :: (
- allEq : ∀ (a b : α), a = b
Any two elements of a subsingleton are equal.
- )
Instances
An equivalence relation ~ : α → α → Prop
is a relation that is:
- reflexive:
x ~ x
- symmetric:
x ~ y
impliesy ~ x
- transitive:
x ~ y
andy ~ z
impliesx ~ z
Equality is an equivalence relation, and equivalence relations share many of
the properties of equality. In particular, Quot α r
is most well behaved
when r
is an equivalence relation, and in this case we use Quotient
instead.
- refl : ∀ (x : α), r x x
An equivalence relation is reflexive:
x ~ x
- symm : ∀ {x y : α}, r x y → r y x
An equivalence relation is symmetric:
x ~ y
impliesy ~ x
- trans : ∀ {x y z : α}, r x y → r y z → r x z
An equivalence relation is transitive:
x ~ y
andy ~ z
impliesx ~ z
Instances For
The empty relation is the relation on α
which is always False
.
Equations
- emptyRelation x✝ x = False
Instances For
Subrelation q r
means that q ⊆ r
or ∀ x y, q x y → r x y
.
It is the analogue of the subset relation on relations.
Equations
- Subrelation q r = ∀ {x y : α}, q x y → r x y
Instances For
The transitive closure TransGen r
of a relation r
is the smallest relation which is
transitive and contains r
. TransGen r a z
if and only if there exists a sequence
a r b r ... r z
of length at least 1 connecting a
to z
.
- single: ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Relation.TransGen r a b
- tail: ∀ {α : Sort u} {r : α → α → Prop} {a b c : α}, Relation.TransGen r a b → r b c → Relation.TransGen r a c
The transitive closure is transitive.
Instances For
Subtype #
Sum #
Equations
- instDecidableEqSum (Sum.inl a_2) (Sum.inl b_2) = if h : a_2 = b_2 then isTrue ⋯ else isFalse ⋯
- instDecidableEqSum (Sum.inr a_2) (Sum.inr b_2) = if h : a_2 = b_2 then isTrue ⋯ else isFalse ⋯
- instDecidableEqSum (Sum.inr val) (Sum.inl val_1) = isFalse ⋯
- instDecidableEqSum (Sum.inl val) (Sum.inr val_1) = isFalse ⋯
Product #
Equations
- One or more equations did not get rendered due to their size.
Dependent products #
Universe polymorphic unit #
Equations
- instInhabitedPUnit = { default := PUnit.unit }
Setoid #
A setoid is a type with a distinguished equivalence relation, denoted ≈
.
This is mainly used as input to the Quotient
type constructor.
- r : α → α → Prop
x ≈ y
is the distinguished equivalence relation of a setoid. - iseqv : Equivalence Setoid.r
The relation
x ≈ y
is an equivalence relation.
Instances
Propositional extensionality #
The axiom of propositional extensionality. It asserts that if propositions
a
and b
are logically equivalent (i.e. we can prove a
from b
and vice versa),
then a
and b
are equal, meaning that we can replace a
with b
in all
contexts.
For simple expressions like a ∧ c ∨ d → e
we can prove that because all the logical
connectives respect logical equivalence, we can replace a
with b
in this expression
without using propext
. However, for higher order expressions like P a
where
P : Prop → Prop
is unknown, or indeed for a = b
itself, we cannot replace a
with b
without an axiom which says exactly this.
This is a relatively uncontroversial axiom, which is intuitionistically valid.
It does however block computation when using #reduce
to reduce proofs directly
(which is not recommended), meaning that canonicity,
the property that all closed terms of type Nat
normalize to numerals,
fails to hold when this (or any) axiom is used:
set_option pp.proofs true
def foo : Nat := by
have : (True → True) ↔ True := ⟨λ _ => trivial, λ _ _ => trivial⟩
have := propext this ▸ (2 : Nat)
exact this
#reduce foo
-- propext { mp := fun x x => True.intro, mpr := fun x => True.intro } ▸ 2
#eval foo -- 2
#eval
can evaluate it to a numeral because the compiler erases casts and
does not evaluate proofs, so propext
, whose return type is a proposition,
can never block it.
Prop lemmas #
implies #
Quotients #
The quotient axiom, or at least the nontrivial part of the quotient
axiomatization. Quotient types are introduced by the init_quot
command
in Init.Prelude
which introduces the axioms:
opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
(∀ a b : α, r a b → f a = f b) → Quot r → β
opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
(∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
All of these axioms are true if we assume Quot α r = α
and Quot.mk
and
Quot.lift
are identity functions, so they do not add much. However this axiom
cannot be explained in that way (it is false for that interpretation), so the
real power of quotient types come from this axiom.
It says that the quotient by r
maps elements which are related by r
to equal
values in the quotient. Together with Quot.lift
which says that functions
which respect r
can be lifted to functions on the quotient, we can deduce that
Quot α r
exactly consists of the equivalence classes with respect to r
.
It is important to note that r
need not be an equivalence relation in this axiom.
When r
is not an equivalence relation, we are actually taking a quotient with
respect to the equivalence relation generated by r
.
Quot.liftOn q f h
is the same as Quot.lift f h q
. It just reorders
the argument q : Quot r
to be first.
Instances For
Dependent recursion principle for Quot
. This constructor can be tricky to use,
so you should consider the simpler versions if they apply:
Quot.lift
, for nondependent functionsQuot.ind
, for theorems / proofs of propositions about quotientsQuot.recOnSubsingleton
, when the target type is aSubsingleton
Quot.hrecOn
, which usesHEq (f a) (f b)
instead of asound p ▸ f a = f b
assummption
Equations
- Quot.rec f h q = Eq.ndrecOn ⋯ (Quot.lift (Quot.indep f) ⋯ q).snd
Instances For
Dependent recursion principle for Quot
. This constructor can be tricky to use,
so you should consider the simpler versions if they apply:
Quot.lift
, for nondependent functionsQuot.ind
, for theorems / proofs of propositions about quotientsQuot.recOnSubsingleton
, when the target type is aSubsingleton
Quot.hrecOn
, which usesHEq (f a) (f b)
instead of asound p ▸ f a = f b
assummption
Equations
- Quot.recOn q f h = Quot.rec f h q
Instances For
Dependent induction principle for a quotient, when the target type is a Subsingleton
.
In this case the quotient's side condition is trivial so any function can be lifted.
Equations
- Quot.recOnSubsingleton q f = Quot.rec (fun (a : α) => f a) ⋯ q
Instances For
Heterogeneous dependent recursion principle for a quotient.
This may be easier to work with since it uses HEq
instead of
an Eq.ndrec
in the hypothesis.
Equations
- Quot.hrecOn q f c = Quot.recOn q f ⋯
Instances For
The canonical quotient map into a Quotient
.
Equations
- Quotient.mk s a = Quot.mk Setoid.r a
Instances For
The canonical quotient map into a Quotient
.
(This synthesizes the setoid by typeclass inference.)
Equations
- Quotient.mk' a = Quotient.mk s a
Instances For
The analogue of Quot.sound
: If a
and b
are related by the equivalence relation,
then they have equal equivalence classes.
The analogue of Quot.lift
: if f : α → β
respects the equivalence relation ≈
,
then it lifts to a function on Quotient s
such that lift f h (mk a) = f a
.
Equations
- Quotient.lift f = Quot.lift f
Instances For
The analogue of Quot.ind
: every element of Quotient s
is of the form Quotient.mk s a
.
The analogue of Quot.liftOn
: if f : α → β
respects the equivalence relation ≈
,
then it lifts to a function on Quotient s
such that liftOn (mk a) f h = f a
.
Equations
- q.liftOn f c = Quot.liftOn q f c
Instances For
The analogue of Quot.inductionOn
: every element of Quotient s
is of the form Quotient.mk s a
.
The analogue of Quot.rec
for Quotient
. See Quot.rec
.
Equations
- Quotient.rec f h q = Quot.rec f h q
Instances For
The analogue of Quot.recOn
for Quotient
. See Quot.recOn
.
Equations
- Quotient.recOn q f h = Quot.recOn q f h
Instances For
The analogue of Quot.recOnSubsingleton
for Quotient
. See Quot.recOnSubsingleton
.
Equations
Instances For
The analogue of Quot.hrecOn
for Quotient
. See Quot.hrecOn
.
Equations
- Quotient.hrecOn q f c = Quot.hrecOn q f c
Instances For
Lift a binary function to a quotient on both arguments.
Equations
- Quotient.lift₂ f c q₁ q₂ = Quotient.lift (fun (a₁ : α) => Quotient.lift (f a₁) ⋯ q₂) ⋯ q₁
Instances For
Lift a binary function to a quotient on both arguments.
Equations
- q₁.liftOn₂ q₂ f c = Quotient.lift₂ f c q₁ q₂
Instances For
Lift a binary function to a quotient on both arguments.
Equations
- Quotient.recOnSubsingleton₂ q₁ q₂ g = Quot.recOnSubsingleton q₁ fun (a : α) => Quot.recOnSubsingleton q₂ fun (a_1 : β) => g a a_1
Instances For
Function extensionality #
Function extensionality is the statement that if two functions take equal values
every point, then the functions themselves are equal: (∀ x, f x = g x) → f = g
.
It is called "extensionality" because it talks about how to prove two objects are equal
based on the properties of the object (compare with set extensionality,
which is (∀ x, x ∈ s ↔ x ∈ t) → s = t
).
This is often an axiom in dependent type theory systems, because it cannot be proved
from the core logic alone. However in lean's type theory this follows from the existence
of quotient types (note the Quot.sound
in the proof, as well as the show
line
which makes use of the definitional equality Quot.lift f h (Quot.mk x) = f x
).
Squash #
Squash α
is the quotient of α
by the always true relation.
It is empty if α
is empty, otherwise it is a singleton.
(Thus it is unconditionally a Subsingleton
.)
It is the "universal Subsingleton
" mapped from α
.
It is similar to Nonempty α
, which has the same properties, but unlike
Nonempty
this is a Type u
, that is, it is "data", and the compiler
represents an element of Squash α
the same as α
itself
(as compared to Nonempty α
, whose elements are represented by a dummy value).
Squash.lift
will extract a value in any subsingleton β
from a function on α
,
while Nonempty.rec
can only do the same when β
is a proposition.
Instances For
Kernel reduction hints #
Depends on the correctness of the Lean compiler, interpreter, and all [implemented_by ...]
and [extern ...]
annotations.
When the kernel tries to reduce a term Lean.reduceBool c
, it will invoke the Lean interpreter to evaluate c
.
The kernel will not use the interpreter if c
is not a constant.
This feature is useful for performing proofs by reflection.
Remark: the Lean frontend allows terms of the from Lean.reduceBool t
where t
is a term not containing
free variables. The frontend automatically declares a fresh auxiliary constant c
and replaces the term with
Lean.reduceBool c
. The main motivation is that the code for t
will be pre-compiled.
Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.
Recall that the compiler trusts the correctness of all [implemented_by ...]
and [extern ...]
annotations.
If an extern function is executed, then the trusted code base will also include the implementation of the associated
foreign function.
Similar to Lean.reduceBool
for closed Nat
terms.
Remark: we do not have plans for supporting a generic reduceValue {α} (a : α) : α := a
.
The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
We believe Lean.reduceBool
enables most interesting applications (e.g., proof by reflection).
The axiom ofReduceBool
is used to perform proofs by reflection. See reduceBool
.
This axiom is usually not used directly, because it has some syntactic restrictions.
Instead, the native_decide
tactic can be used to prove any proposition whose
decidability instance can be evaluated to true
using the lean compiler / interpreter.
Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.
The axiom ofReduceNat
is used to perform proofs by reflection. See reduceBool
.
Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base. This is extra 30k lines of code. More importantly, you will probably not be able to check your development using external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers.
Associative op
indicates op
is an associative operation,
i.e. (a ∘ b) ∘ c = a ∘ (b ∘ c)
.
- assoc : ∀ (a b c : α), op (op a b) c = op a (op b c)
An associative operation satisfies
(a ∘ b) ∘ c = a ∘ (b ∘ c)
.
Instances
Commutative op
says that op
is a commutative operation,
i.e. a ∘ b = b ∘ a
.
- comm : ∀ (a b : α), op a b = op b a
A commutative operation satisfies
a ∘ b = b ∘ a
.
Instances
IdempotentOp op
indicates op
is an idempotent binary operation.
i.e. a ∘ a = a
.
- idempotent : ∀ (x : α), op x x = x
An idempotent operation satisfies
a ∘ a = a
.
Instances
LawfulLeftIdentify op o
indicates o
is a verified left identity of
op
.
- left_id : ∀ (a : β), op o a = a
Left identity
o
is an identity.
Instances
LawfulRightIdentify op o
indicates o
is a verified right identity of
op
.
- right_id : ∀ (a : α), op a o = a
Right identity
o
is an identity.
Instances
Identity op o
indicates o
is a left and right identity of op
.
This class does not require a proof that o
is an identity, and is used
primarily for inferring the identity using class resolution.
Instances
LawfulIdentity op o
indicates o
is a verified left and right
identity of op
.
Instances
LawfulCommIdentity
can simplify defining instances of LawfulIdentity
on commutative functions by requiring only a left or right identity
proof.
This class is intended for simplifying defining instances of
LawfulIdentity
and functions needed commutative operations with
identity should just add a LawfulIdentity
constraint.