def inline {α : Sort u} (a : α) : α

inline (f x) is an indication to the compiler to inline the definition of f at the application site itself (by comparison to the @[inline] attribute, which applies to all applications of the function).

Equations

• inline a = a

theorem id_def {α : Sort u} (a : α) : id a = a

@[inline]

def flip {α : Sort u} {β : Sort v} {φ : Sort w} (f : α → β → φ) : β → α → φ

flip f a b is f b a. It is useful for "point-free" programming, since it can sometimes be used to avoid introducing variables. For example, (·<·) is the less-than relation, and flip (·<·) is the greater-than relation.

Equations

• flip f b a = f a b

@[simp]

theorem Function.const_apply {β : Sort u_1} {α : Sort u_2} {y : β} {x : α} : const α y x = y

@[simp]

theorem Function.comp_apply {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α} : (f ∘ g) x = f (g x)

theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β) : f ∘ g = fun (x : α) => f (g x)

@[simp]

theorem Function.const_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {c : γ} : const β c ∘ f = const α c

@[simp]

theorem Function.comp_const {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} {f : β → γ} {b : β} : f ∘ const α b = const α (f b)

@[simp]

theorem Function.true_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} : (fun (x : β) => true) ∘ f = fun (x : α) => true

@[simp]

theorem Function.false_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} : (fun (x : β) => false) ∘ f = fun (x : α) => false

@[macro_inline]

def Empty.elim {C : Sort u} : Empty → C

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.

Equations

• t.elim = Empty.rec (fun (x : Empty) => C) t

instance instDecidableEqEmpty : DecidableEq Empty

Decidable equality for Empty

Equations

• instDecidableEqEmpty a = a.elim

@[macro_inline]

def PEmpty.elim {C : Sort u_1} : PEmpty → C

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.

instance instDecidableEqPEmpty : DecidableEq PEmpty

Decidable equality for PEmpty

Equations

• instDecidableEqPEmpty a = a.elim

structure Thunk (α : Type u) : Type u

Delays evaluation. The delayed code is evaluated at most once.

A thunk is code that constructs a value when it is requested via Thunk.get, Thunk.map, or Thunk.bind. The resulting value is cached, so the code is executed at most once. This is also known as lazy or call-by-need evaluation.

The Lean runtime has special support for the Thunk type in order to implement the caching behavior.

• fn : Unit → α

  Extract the getter function out of a thunk. Use Thunk.get instead.

@[extern lean_thunk_pure]

def Thunk.pure {α : Type u_1} (a : α) : Thunk α

Stores an already-computed value in a thunk.

Because the value has already been computed, there is no laziness.

Equations

• Thunk.pure a = { fn := fun (x : Unit) => a }

@[extern lean_thunk_get_own]

def Thunk.get {α : Type u_1} (x : Thunk α) : α

Gets the thunk's value. If the value is cached, it is returned in constant time; if not, it is computed.

Computed values are cached, so the value is not recomputed.

Equations

• x.get = Thunk.fn✝ x ()

@[inline]

def Thunk.map {α : Type u_1} {β : Type u_2} (f : α → β) (x : Thunk α) : Thunk β

Constructs a new thunk that forces x and then applies x to the result. Upon forcing, the result of f is cached and the reference to the thunk x is dropped.

Equations

• Thunk.map f x = { fn := fun (x_1 : Unit) => f x.get }

@[inline]

def Thunk.bind {α : Type u_1} {β : Type u_2} (x : Thunk α) (f : α → Thunk β) : Thunk β

Constructs a new thunk that applies f to the result of x when forced.

Equations

• x.bind f = { fn := fun (x_1 : Unit) => (f x.get).get }

@[simp]

theorem Thunk.sizeOf_eq {α : Type u_1} [SizeOf α] (a : Thunk α) : sizeOf a = 1 + sizeOf a.get

instance thunkCoe {α : Type u_1} : CoeTail α (Thunk α)

Equations

• thunkCoe = { coe := fun (a : α) => { fn := fun (x : Unit) => a } }

definitions

structure Iff (a b : Prop) : Prop

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.

Conventions for notations in identifiers:

• The recommended spelling of ↔ in identifiers is iff.

• The recommended spelling of <-> in identifiers is iff (prefer ↔ over <->).

• intro :: (
• mp : a → b

  Modus ponens for if and only if. If a ↔ b and a, then b.

• mpr : b → a

  Modus ponens for if and only if, reversed. If a ↔ b and b, then a.

• )

def «term_<->_» : Lean.TrailingParserDescr

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.

Conventions for notations in identifiers:

• The recommended spelling of <-> in identifiers is iff (prefer ↔ over <->).

Equations

• «term_<->_» = Lean.ParserDescr.trailingNode `«term_<->_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <-> ") (Lean.ParserDescr.cat `term 21))

def «term_↔_» : Lean.TrailingParserDescr

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.

Conventions for notations in identifiers:

• The recommended spelling of ↔ in identifiers is iff.

Equations

• «term_↔_» = Lean.ParserDescr.trailingNode `«term_↔_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↔ ") (Lean.ParserDescr.cat `term 21))

inductive Sum (α : Type u) (β : Type v) : Type (max u v)

The disjoint union of types α and β, ordinarily written α ⊕ β.

An element of α ⊕ β is either an a : α wrapped in Sum.inl or a b : β wrapped in Sum.inr. α ⊕ β is not equivalent to the set-theoretic union of α and β because its values include an indication of which of the two types was chosen. The union of a singleton set with itself contains one element, while Unit ⊕ Unit contains distinct values inl () and inr ().

• inl {α : Type u} {β : Type v} (val : α) : α ⊕ β

  Left injection into the sum type α ⊕ β.

• inr {α : Type u} {β : Type v} (val : β) : α ⊕ β

  Right injection into the sum type α ⊕ β.

def «term_⊕_» : Lean.TrailingParserDescr

The disjoint union of types α and β, ordinarily written α ⊕ β.

An element of α ⊕ β is either an a : α wrapped in Sum.inl or a b : β wrapped in Sum.inr. α ⊕ β is not equivalent to the set-theoretic union of α and β because its values include an indication of which of the two types was chosen. The union of a singleton set with itself contains one element, while Unit ⊕ Unit contains distinct values inl () and inr ().

Equations

• «term_⊕_» = Lean.ParserDescr.trailingNode `«term_⊕_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 30))

inductive PSum (α : Sort u) (β : Sort v) : Sort (max (max 1 u) v)

The disjoint union of arbitrary sorts α β, or α ⊕' β.

It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting them to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat. However, the resulting universe level constraints are often more difficult to solve than those that result from Sum.

• inl {α : Sort u} {β : Sort v} (val : α) : α ⊕' β

  Left injection into the sum type α ⊕' β.

• inr {α : Sort u} {β : Sort v} (val : β) : α ⊕' β

  Right injection into the sum type α ⊕' β.

def «term_⊕'_» : Lean.TrailingParserDescr

The disjoint union of arbitrary sorts α β, or α ⊕' β.

It differs from α ⊕ β in that it allows α and β to have arbitrary sorts Sort u and Sort v, instead of restricting them to Type u and Type v. This means that it can be used in situations where one side is a proposition, like True ⊕' Nat. However, the resulting universe level constraints are often more difficult to solve than those that result from Sum.

Equations

• «term_⊕'_» = Lean.ParserDescr.trailingNode `«term_⊕'_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕' ") (Lean.ParserDescr.cat `term 30))

@[reducible]

def PSum.inhabitedLeft {α : Sort u_1} {β : Sort u_2} [Inhabited α] : Inhabited (α ⊕' β)

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

Equations

• PSum.inhabitedLeft = { default := PSum.inl default }

@[reducible]

def PSum.inhabitedRight {α : Sort u_1} {β : Sort u_2} [Inhabited β] : Inhabited (α ⊕' β)

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

Equations

• PSum.inhabitedRight = { default := PSum.inr default }

instance PSum.nonemptyLeft {α : Sort u_1} {β : Sort u_2} [h : Nonempty α] : Nonempty (α ⊕' β)

instance PSum.nonemptyRight {β : Sort u_1} {α : Sort u_2} [h : Nonempty β] : Nonempty (α ⊕' β)

@[unbox]

structure Sigma {α : Type u} (β : α → Type v) : Type (max u v)

Dependent pairs, in which the second element's type depends on the value of the first element. The type Sigma β is typically written Σ a : α, β a or (a : α) × β a.

Although its values are pairs, Sigma 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.

• snd : β self.fst

  The second component of a dependent pair. Its type depends on the first component.

structure PSigma {α : Sort u} (β : α → Sort v) : Sort (max (max 1 u) v)

Fully universe-polymorphic dependent pairs, in which the second element's type depends on the value of the first element and both types are allowed to be propositions. The type PSigma β is typically written Σ' a : α, β a or (a : α) ×' β a.

In practice, this generality leads to universe level constraints that are difficult to solve, so PSigma is rarely used in manually-written code. It is usually only used in automation that constructs pairs of arbitrary types.

To pair a value with a proof that a predicate holds for it, use Subtype. To demonstrate that a value exists that satisfies a predicate, use Exists. A dependent pair with a proposition as its first component is not typically useful due to proof irrelevance: there's no point in depending on a specific proof because all proofs are equal anyway.

• fst : α

  The first component of a dependent pair.

• snd : β self.fst

  The second component of a dependent pair. Its type depends on the first component.

inductive Exists {α : Sort u} (p : α → Prop) : Prop

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 : α) (h : p w) : Exists p

  Existential introduction. If a : α and h : p a, then ⟨a, h⟩ is a proof that ∃ x : α, p x.

inductive ForInStep (α : Type u) : Type u

An indication of whether a loop's body terminated early that's used to compile the for x in xs notation.

A collection's ForIn or ForIn' instance describe's how to iterate over its elements. The monadic action that represents the body of the loop returns a ForInStep α, where α is the local state used to implement features such as let mut.

• done {α : Type u} : α → ForInStep α

  The loop should terminate early.

  ForInStep.done is produced by uses of break or return in the loop body.

• yield {α : Type u} : α → ForInStep α

  The loop should continue with the next iteration, using the returned state.

  ForInStep.yield is produced by continue and by reaching the bottom of the loop body.

instance instInhabitedForInStep {a✝ : Type u_1} [Inhabited a✝] : Inhabited (ForInStep a✝)

Equations

• instInhabitedForInStep = { default := ForInStep.done default }

class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) : Type (max (max (max u (u₁ + 1)) u₂) v)

Monadic iteration in do-blocks, using the for x in xs notation.

The parameter m is the monad of the do-block in which iteration is performed, ρ is the type of the collection being iterated over, and α is the type of elements.

• forIn {β : Type u₁} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

  Monadically iterates over the contents of a collection xs, with a local state b and the possibility of early termination.

  Because a do block supports local mutable bindings along with return, and break, the monadic action passed to ForIn.forIn takes a starting state in addition to the current element of the collection and returns an updated state together with an indication of whether iteration should continue or terminate. If the action returns ForInStep.done, then ForIn.forIn should stop iteration and return the updated state. If the action returns ForInStep.yield, then ForIn.forIn should continue iterating if there are further elements, passing the updated state to the action.

  More information about the translation of for loops into ForIn.forIn is available in the Lean reference manual.

class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam (Membership α ρ)) : Type (max (max (max u (u₁ + 1)) u₂) v)

Monadic iteration in do-blocks with a membership proof, using the for h : x in xs notation.

The parameter m is the monad of the do-block in which iteration is performed, ρ is the type of the collection being iterated over, α is the type of elements, and d is the specific membership predicate to provide.

• forIn' {β : Type u₁} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β

  Monadically iterates over the contents of a collection xs, with a local state b and the possibility of early termination. At each iteration, the body of the loop is provided with a proof that the current element is in the collection.

  Because a do block supports local mutable bindings along with return, and break, the monadic action passed to ForIn'.forIn' takes a starting state in addition to the current element of the collection with its membership proof. The action returns an updated state together with an indication of whether iteration should continue or terminate. If the action returns ForInStep.done, then ForIn'.forIn' should stop iteration and return the updated state. If the action returns ForInStep.yield, then ForIn'.forIn' should continue iterating if there are further elements, passing the updated state to the action.

  More information about the translation of for loops into ForIn'.forIn' is available in the Lean reference manual.

inductive DoResultPRBC (α β σ : Type u) : Type u

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 value a.
• return (b : β) s means that the block exited via a return b early-exit command.
• break s means that break was called, meaning that we should exit from the containing loop.
• continue s means that continue 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 value a

• return {α β σ : Type u} : β → σ → DoResultPRBC α β σ

  return (b : β) s means that the block exited via a return b early-exit command

• break {α β σ : Type u} : σ → DoResultPRBC α β σ

  break s means that break was called, meaning that we should exit from the containing loop

• continue {α β σ : Type u} : σ → DoResultPRBC α β σ

  continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

inductive DoResultPR (α β σ : Type u) : Type u

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 value a

• return {α β σ : Type u} : β → σ → DoResultPR α β σ

  return (b : β) s means that the block exited via a return b early-exit command

inductive DoResultBC (σ : Type u) : Type u

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 σ

  break s means that break was called, meaning that we should exit from the containing loop

• continue {σ : Type u} : σ → DoResultBC σ

  continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

inductive DoResultSBC (α σ : Type u) : Type u

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 α σ

  This encodes either pure (a : α) or return (a : α):

  • pure (a : α) s means that the block exited normally with return value a
  • return (b : β) s means that the block exited via a return b early-exit command

  The one that is actually encoded depends on the context of use.

• break {α σ : Type u} : σ → DoResultSBC α σ

  break s means that break was called, meaning that we should exit from the containing loop

• continue {α σ : Type u} : σ → DoResultSBC α σ

  continue s means that continue was called, meaning that we should continue to the next iteration of the containing loop

class HasEquiv (α : Sort u) : Sort (max u (v + 1))

HasEquiv α is the typeclass which supports the notation x ≈ y where x y : α.

• Equiv : α → α → Sort v

  x ≈ y says that x and y are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent.

  Conventions for notations in identifiers:

  • The recommended spelling of ≈ in identifiers is equiv.

def «term_≈_» : Lean.TrailingParserDescr

x ≈ y says that x and y are equivalent. Because this is a typeclass, the notion of equivalence is type-dependent.

Conventions for notations in identifiers:

• The recommended spelling of ≈ in identifiers is equiv.

Equations

• «term_≈_» = Lean.ParserDescr.trailingNode `«term_≈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≈ ") (Lean.ParserDescr.cat `term 51))

set notation

class HasSubset (α : Type u) : Type u

Notation type class for the subset relation ⊆.

• Subset : α → α → Prop

  Subset relation: a ⊆ b

  Conventions for notations in identifiers:

  • The recommended spelling of ⊆ in identifiers is subset.

class HasSSubset (α : Type u) : Type u

Notation type class for the strict subset relation ⊂.

• SSubset : α → α → Prop

  Strict subset relation: a ⊂ b

  Conventions for notations in identifiers:

  • The recommended spelling of ⊂ in identifiers is ssubset.

@[reducible, inline]

abbrev Superset {α : Type u_1} [HasSubset α] (a b : α) : Prop

Superset relation: a ⊇ b

Conventions for notations in identifiers:

• The recommended spelling of ⊇ in identifiers is superset (prefer ⊆ over ⊇).

Equations

• (a ⊇ b) = (b ⊆ a)

@[reducible, inline]

abbrev SSuperset {α : Type u_1} [HasSSubset α] (a b : α) : Prop

Strict superset relation: a ⊃ b

Conventions for notations in identifiers:

• The recommended spelling of ⊃ in identifiers is ssuperset (prefer ⊂ over ⊃).

Equations

• (a ⊃ b) = (b ⊂ a)

class Union (α : Type u) : Type u

Notation type class for the union operation ∪.

• union : α → α → α

  a ∪ b is the union ofa and b.

  Conventions for notations in identifiers:

  • The recommended spelling of ∪ in identifiers is union.

class Inter (α : Type u) : Type u

Notation type class for the intersection operation ∩.

• inter : α → α → α

  a ∩ b is the intersection ofa and b.

  Conventions for notations in identifiers:

  • The recommended spelling of ∩ in identifiers is inter.

class SDiff (α : Type u) : Type u

Notation type class for the set difference \.

• sdiff : α → α → α

  a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

  Conventions for notations in identifiers:

  • The recommended spelling of \ in identifiers is sdiff.

def «term_⊆_» : Lean.TrailingParserDescr

Subset relation: a ⊆ b

Conventions for notations in identifiers:

• The recommended spelling of ⊆ in identifiers is subset.

Equations

• «term_⊆_» = Lean.ParserDescr.trailingNode `«term_⊆_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ ") (Lean.ParserDescr.cat `term 51))

def «term_⊂_» : Lean.TrailingParserDescr

Strict subset relation: a ⊂ b

Conventions for notations in identifiers:

• The recommended spelling of ⊂ in identifiers is ssubset.

Equations

• «term_⊂_» = Lean.ParserDescr.trailingNode `«term_⊂_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊂ ") (Lean.ParserDescr.cat `term 51))

def «term_⊇_» : Lean.TrailingParserDescr

Superset relation: a ⊇ b

Conventions for notations in identifiers:

• The recommended spelling of ⊇ in identifiers is superset (prefer ⊆ over ⊇).

Equations

• «term_⊇_» = Lean.ParserDescr.trailingNode `«term_⊇_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊇ ") (Lean.ParserDescr.cat `term 51))

def «term_⊃_» : Lean.TrailingParserDescr

Strict superset relation: a ⊃ b

Conventions for notations in identifiers:

• The recommended spelling of ⊃ in identifiers is ssuperset (prefer ⊂ over ⊃).

Equations

• «term_⊃_» = Lean.ParserDescr.trailingNode `«term_⊃_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊃ ") (Lean.ParserDescr.cat `term 51))

def «term_∪_» : Lean.TrailingParserDescr

a ∪ b is the union ofa and b.

Conventions for notations in identifiers:

• The recommended spelling of ∪ in identifiers is union.

Equations

• «term_∪_» = Lean.ParserDescr.trailingNode `«term_∪_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∪ ") (Lean.ParserDescr.cat `term 66))

def «term_∩_» : Lean.TrailingParserDescr

a ∩ b is the intersection ofa and b.

Conventions for notations in identifiers:

• The recommended spelling of ∩ in identifiers is inter.

Equations

• «term_∩_» = Lean.ParserDescr.trailingNode `«term_∩_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∩ ") (Lean.ParserDescr.cat `term 71))

def «term_\_» : Lean.TrailingParserDescr

a \ b is the set difference of a and b, consisting of all elements in a that are not in b.

Conventions for notations in identifiers:

• The recommended spelling of \ in identifiers is sdiff.

Equations

• «term_\_» = Lean.ParserDescr.trailingNode `«term_\_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\ ") (Lean.ParserDescr.cat `term 71))

collections

class EmptyCollection (α : Type u) : Type u

EmptyCollection α is the typeclass which supports the notation ∅, also written as {}.

• emptyCollection : α

  ∅ or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

  Conventions for notations in identifiers:

  • The recommended spelling of {} in identifiers is empty.

  • The recommended spelling of ∅ in identifiers is empty.

def «term{}» : Lean.ParserDescr

∅ or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

Conventions for notations in identifiers:

• The recommended spelling of {} in identifiers is empty.

Equations

• «term{}» = Lean.ParserDescr.node `«term{}» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{") (Lean.ParserDescr.symbol "}"))

def «term∅» : Lean.ParserDescr

∅ or {} is the empty set or empty collection. It is supported by the EmptyCollection typeclass.

Conventions for notations in identifiers:

• The recommended spelling of ∅ in identifiers is empty.

Equations

• «term∅» = Lean.ParserDescr.node `«term∅» 1024 (Lean.ParserDescr.symbol "∅")

class Insert (α : outParam (Type u)) (γ : Type v) : Type (max u v)

Type class for the insert operation. Used to implement the { a, b, c } syntax.

• insert : α → γ → γ

  insert x xs inserts the element x into the collection xs.

class Singleton (α : outParam (Type u)) (β : Type v) : Type (max u v)

Type class for the singleton operation. Used to implement the { a, b, c } syntax.

• singleton : α → β

  singleton x is a collection with the single element x (notation: {x}).

  Conventions for notations in identifiers:

  • The recommended spelling of {x} in identifiers is singleton.

class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] : Prop

insert x ∅ = {x}

• insert_empty_eq (x : α) : insert x ∅ = {x}

  insert x ∅ = {x}

@[deprecated LawfulSingleton.insert_empty_eq (since := "2025-03-12")]

theorem insert_emptyc_eq {β : Type u_1} {α : Type u_2} [EmptyCollection β] [Insert α β] [Singleton α β] [LawfulSingleton α β] (x : α) : insert x ∅ = {x}

@[deprecated LawfulSingleton.insert_empty_eq (since := "2025-03-12")]

theorem LawfulSingleton.insert_emptyc_eq {β : Type u_1} {α : Type u_2} [EmptyCollection β] [Insert α β] [Singleton α β] [LawfulSingleton α β] (x : α) : insert x ∅ = {x}

class Sep (α : outParam (Type u)) (γ : Type v) : Type (max u v)

Type class used to implement the notation { a ∈ c | p a }

• sep : (α → Prop) → γ → γ

  Computes { a ∈ c | p a }.

structure Task (α : Type u) : Type u

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 : α

  Blocks the current thread until the given task has finished execution, and then returns the result of the task. If the current thread is itself executing a (non-dedicated) task, the maximum threadpool size is temporarily increased by one while waiting so as to ensure the process cannot be deadlocked by threadpool starvation. Note that when the current thread is unblocked, more tasks than the configured threadpool size may temporarily be running at the same time until sufficiently many tasks have finished.

  Task.map and Task.bind should be preferred over Task.get for setting up task dependencies where possible as they do not require temporarily growing the threadpool in this way.

• )

instance instInhabitedTask {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Task a✝)

Equations

• instInhabitedTask = { default := { get := default } }

instance instNonemptyTask {α✝ : Type u_1} [Nonempty α✝] : Nonempty (Task α✝)

@[reducible, inline]

abbrev Task.Priority : Type

Task priority.

Tasks with higher priority will always be scheduled before tasks with lower priority. Tasks with a priority greater than Task.Priority.max are scheduled on dedicated threads.

Equations

• Task.Priority = Nat

def Task.Priority.default : Priority

The default priority for spawned tasks, also the lowest priority: 0.

Equations

• Task.Priority.default = 0

def Task.Priority.max : Priority

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. This is indicated using Task.Priority.dedicated. Regular priority tasks are placed in a thread pool and worked on according to their priority order.

Equations

• Task.Priority.max = 8

def Task.Priority.dedicated : Priority

Indicates that a task should be scheduled on a dedicated thread.

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

• Task.Priority.dedicated = 9

@[noinline, extern lean_task_spawn]

def Task.spawn {α : Type u} (fn : Unit → α) (prio : Priority := Priority.default) : Task α

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 () }

@[noinline, extern lean_task_map]

def Task.map {α : Type u_1} {β : Type u_2} (f : α → β) (x : Task α) (prio : Priority := Priority.default) (sync : Bool := false) : Task β

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 and otherwise on the thread that x finished on. prio is ignored in this case. This should only be done when executing f is cheap and non-blocking.

Equations

• Task.map f x prio sync = { get := f x.get }

@[noinline, extern lean_task_bind]

def Task.bind {α : Type u_1} {β : Type u_2} (x : Task α) (f : α → Task β) (prio : Priority := Priority.default) (sync : Bool := false) : Task β

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 and otherwise on the thread that x finished on. prio is ignored in this case. This should only be done when executing f is cheap and non-blocking.

Equations

• x.bind f prio sync = { get := (f x.get).get }

structure NonScalar : Type

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

inductive PNonScalar : Type u

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 (v : Nat) : PNonScalar

  You should not use this function

@[simp]

theorem Nat.add_zero (n : Nat) : n + 0 = n

theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α

Boolean operators

@[extern lean_strict_or]

def strictOr (b₁ b₂ : Bool) : Bool

strictOr is the same as or, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is true.

Equations

• strictOr b₁ b₂ = (b₁ || b₂)

@[extern lean_strict_and]

def strictAnd (b₁ b₂ : Bool) : Bool

strictAnd is the same as and, but it does not use short-circuit evaluation semantics: both sides are evaluated, even if the first value is false.

Equations

• strictAnd b₁ b₂ = (b₁ && b₂)

@[inline]

def bne {α : Type u} [BEq α] (a b : α) : Bool

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.

Conventions for notations in identifiers:

• The recommended spelling of != in identifiers is bne.

Equations

• (a != b) = !a == b

def «term_!=_» : Lean.TrailingParserDescr

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.

Conventions for notations in identifiers:

• The recommended spelling of != in identifiers is bne.

Equations

• «term_!=_» = Lean.ParserDescr.trailingNode `«term_!=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " != ") (Lean.ParserDescr.cat `term 51))

class LawfulBEq (α : Type u) [BEq α] : Prop

A Boolean equality test coincides with propositional equality.

In other words:

• a == b implies a = b.
• a == a is true.

• eq_of_beq {a b : α} : (a == b) = true → a = b

  If a == b evaluates to true, then a and b are equal in the logic.

• rfl {a : α} : (a == a) = true

  == is reflexive, that is, (a == a) = true.

instance instLawfulBEqBool : LawfulBEq Bool

instance instLawfulBEq {α : Type u_1} [DecidableEq α] : LawfulBEq α

instance instLawfulBEqChar : LawfulBEq Char

instance instLawfulBEqString : LawfulBEq String

Logical connectives and equality

theorem trivial : True

True is true, and True.intro (or more commonly, trivial) is the proof.

theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a

theorem not_false : ¬False

theorem not_not_intro {p : Prop} (h : p) : ¬¬p

theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂

@[macro_inline]

def Eq.mp {α β : Sort u} (h : α = β) (a : α) : β

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

@[macro_inline]

def Eq.mpr {α β : Sort u} (h : α = β) (b : β) : α

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

theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) : p b

@[simp]

theorem cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a

@[reducible]

def Ne {α : Sort u} (a b : α) : Prop

a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

Conventions for notations in identifiers:

• The recommended spelling of ≠ in identifiers is ne.

Equations

• (a ≠ b) = ¬a = b

def «term_≠_» : Lean.TrailingParserDescr

a ≠ b, or Ne a b is defined as ¬ (a = b) or a = b → False, and asserts that a and b are not equal.

Conventions for notations in identifiers:

• The recommended spelling of ≠ in identifiers is ne.

Equations

• «term_≠_» = Lean.ParserDescr.trailingNode `«term_≠_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠ ") (Lean.ParserDescr.cat `term 51))

theorem Ne.intro {α : Sort u} {a b : α} (h : a = b → False) : a ≠ b

theorem Ne.elim {α : Sort u} {a b : α} (h : a ≠ b) : a = b → False

theorem Ne.irrefl {α : Sort u} {a : α} (h : a ≠ a) : False

theorem Ne.symm {α : Sort u} {a b : α} (h : a ≠ b) : b ≠ a

theorem ne_comm {α : Sort u_1} {a b : α} : a ≠ b ↔ b ≠ a

theorem false_of_ne {α : Sort u} {a : α} : a ≠ a → False

theorem ne_false_of_self {p : Prop} : p → p ≠ False

theorem ne_true_of_not {p : Prop} : ¬p → p ≠ True

theorem true_ne_false : ¬True = False

theorem false_ne_true : False ≠ True

theorem Bool.of_not_eq_true {b : Bool} : ¬b = true → b = false

theorem Bool.of_not_eq_false {b : Bool} : ¬b = false → b = true

theorem ne_of_beq_false {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b

theorem beq_false_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false

noncomputable def HEq.ndrec {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : HEq a b) : motive b

Non-dependent recursor for HEq

Equations

• HEq.ndrec m h = HEq.rec m h

noncomputable def HEq.ndrecOn {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : HEq a b) (m : motive a) : motive b

HEq.ndrec variant

Equations

• HEq.ndrecOn h m = HEq.rec m h

noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : HEq a b) (h₂ : p a) : p b

HEq.ndrec variant

Equations

• h₁.elim h₂ = ⋯ ▸ h₂

theorem HEq.subst {α β : Sort u} {a : α} {b : β} {p : (T : Sort u) → T → Prop} (h₁ : HEq a b) (h₂ : p α a) : p β b

Substitution with heterogeneous equality.

theorem HEq.symm {α β : Sort u} {a : α} {b : β} (h : HEq a b) : HEq b a

Heterogeneous equality is symmetric.

theorem heq_of_eq {α : Sort u} {a a' : α} (h : a = a') : HEq a a'

Propositionally equal terms are also heterogeneously equal.

theorem HEq.trans {α β φ : Sort u} {a : α} {b : β} {c : φ} (h₁ : HEq a b) (h₂ : HEq b c) : HEq a c

Heterogeneous equality is transitive.

theorem heq_of_heq_of_eq {α β : Sort u} {a : α} {b b' : β} (h₁ : HEq a b) (h₂ : b = b') : HEq a b'

Heterogeneous equality precomposes with propositional equality.

theorem heq_of_eq_of_heq {α β : Sort u} {a a' : α} {b : β} (h₁ : a = a') (h₂ : HEq a' b) : HEq a b

Heterogeneous equality postcomposes with propositional equality.

theorem type_eq_of_heq {α β : Sort u} {a : α} {b : β} (h : HEq a b) : α = β

If two terms are heterogeneously equal then their types are propositionally equal.

theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a) : HEq (Eq.recOn h p) p

Rewriting inside φ using Eq.recOn yields a term that's heterogeneously equal to the original term.

theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : h₁ ▸ a = b) : HEq a b

If casting a term with Eq.rec to another type makes it equal to some other term, then the two terms are heterogeneously equal.

@[simp]

theorem cast_heq {α β : Sort u} (h : α = β) (a : α) : HEq (cast h a) a

The result of casting a term with cast is heterogeneously equal to the original term.

theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a)

theorem Iff.refl (a : Prop) : a ↔ a

theorem Iff.rfl {a : Prop} : a ↔ a

theorem Iff.of_eq {a b : Prop} (h : a = b) : a ↔ b

theorem Iff.trans {a b c : Prop} (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c

instance instTransIff : Trans Iff Iff Iff

Equations

• instTransIff = { trans := ⋯ }

theorem Eq.comm {α : Sort u_1} {a b : α} : a = b ↔ b = a

theorem eq_comm {α : Sort u_1} {a b : α} : a = b ↔ b = a

theorem HEq.comm {α β : Sort u_1} {a : α} {b : β} : HEq a b ↔ HEq b a

theorem heq_comm {α β : Sort u_1} {a : α} {b : β} : HEq a b ↔ HEq b a

theorem Iff.symm {a b : Prop} (h : a ↔ b) : b ↔ a

theorem Iff.comm {a b : Prop} : (a ↔ b) ↔ (b ↔ a)

theorem iff_comm {a b : Prop} : (a ↔ b) ↔ (b ↔ a)

theorem And.symm {a b : Prop} : a ∧ b → b ∧ a

theorem And.comm {a b : Prop} : a ∧ b ↔ b ∧ a

theorem and_comm {a b : Prop} : a ∧ b ↔ b ∧ a

theorem Or.symm {a b : Prop} : a ∨ b → b ∨ a

theorem Or.comm {a b : Prop} : a ∨ b ↔ b ∨ a

theorem or_comm {a b : Prop} : a ∨ b ↔ b ∨ a

Exists

theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : ∃ (x : α), p x) (h₂ : ∀ (a : α), p a → b) : b

Decidable

@[simp]

theorem decide_true (h : Decidable True) : decide True = true

@[simp]

theorem decide_false (h : Decidable False) : decide False = false

@[reducible, inline, deprecated decide_true (since := "2024-11-05")]

abbrev decide_true_eq_true (h : Decidable True) : decide True = true

Equations

• decide_true_eq_true = decide_true

@[reducible, inline, deprecated decide_false (since := "2024-11-05")]

abbrev decide_false_eq_false (h : Decidable False) : decide False = false

Equations

• decide_false_eq_false = decide_false

@[inline]

def toBoolUsing {p : Prop} (d : Decidable p) : Bool

Similar to decide, but uses an explicit instance

Equations

• toBoolUsing d = decide p

theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) : toBoolUsing d = true

theorem ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) : p

theorem ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p

instance instDecidableTrue : Decidable True

Equations

• instDecidableTrue = isTrue trivial

instance instDecidableFalse : Decidable False

Equations

• instDecidableFalse = isFalse not_false

@[macro_inline]

def Decidable.byCases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q

Construct a q if some proposition p is decidable, and both the truth and falsity of p are sufficient to construct a q.

This is a synonym for dite, the dependent if-then-else operator.

Equations

• Decidable.byCases h1 h2 = h1 h
• Decidable.byCases h1 h2 = h2 h

theorem Decidable.em (p : Prop) [Decidable p] : p ∨ ¬p

theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

theorem Decidable.of_not_not {p : Prop} [Decidable p] : ¬¬p → p

theorem Decidable.not_and_iff_or_not {p q : Prop} [d₁ : Decidable p] [d₂ : Decidable q] : ¬(p ∧ q) ↔ ¬p ∨ ¬q

@[inline]

def decidable_of_decidable_of_iff {p q : Prop} [Decidable p] (h : p ↔ q) : Decidable q

Transfer a decidability proof across an equivalence of propositions.

Equations

• decidable_of_decidable_of_iff h = if hp : p then isTrue ⋯ else isFalse ⋯

@[inline]

def decidable_of_decidable_of_eq {p q : Prop} [Decidable p] (h : p = q) : Decidable q

Transfer a decidability proof across an equality of propositions.

Equations

• decidable_of_decidable_of_eq h = decidable_of_decidable_of_iff ⋯

@[macro_inline]

instance instDecidableForall {p q : Prop} [Decidable p] [Decidable q] : Decidable (p → q)

Equations

• instDecidableForall = if hp : p then if hq : q then isTrue ⋯ else isFalse ⋯ else isTrue ⋯

instance instDecidableIff {p q : Prop} [Decidable p] [Decidable q] : Decidable (p ↔ q)

Equations

• instDecidableIff = if hp : p then if hq : q then isTrue ⋯ else isFalse ⋯ else if hq : q then isFalse ⋯ else isTrue ⋯

if-then-else expression theorems

theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (if c then t else e) = t

theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} : (if c then t else e) = e

def iteInduction {α : Sort u_1} {c : Prop} [inst : Decidable c] {motive : α → Sort u_2} {t e : α} (hpos : c → motive t) (hneg : ¬c → motive e) : motive (if c then t else e)

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

theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} : dite c t e = t hc

theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} : dite c t e = e hnc

theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t e : α) : (if x : c then t else e) = if c then t else e

instance instDecidableIte {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)

Equations

• instDecidableIte = dT
• instDecidableIte = dE

instance instDecidableDite {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : (h : c) → Decidable (t h)] [dE : (h : ¬c) → Decidable (e h)] : Decidable (if h : c then t h else e h)

Equations

• instDecidableDite = dT h
• instDecidableDite = dE h

@[reducible, inline]

abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w

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

@[reducible, inline]

abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) {P : Sort w} {x y : α} (h : x = y) : noConfusionTypeEnum f P x y

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

Inhabited

instance instInhabitedProp : Inhabited Prop

Equations

• instInhabitedProp = { default := True }

instance instInhabitedTrue : Inhabited True

Equations

• instInhabitedTrue = { default := True.intro }

instance instInhabitedPNonScalar : Inhabited PNonScalar

Equations

• instInhabitedPNonScalar = { default := PNonScalar.mk default }

instance instInhabitedNonScalar : Inhabited NonScalar

Equations

• instInhabitedNonScalar = { default := { val := default } }

instance instInhabitedForInStep_1 {a✝ : Type u_1} [Inhabited a✝] : Inhabited (ForInStep a✝)

Equations

• instInhabitedForInStep_1 = { default := ForInStep.done default }

theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : (∃ (x : α), p x) → Nonempty α

Subsingleton

class Subsingleton (α : Sort u) : Prop

A subsingleton is a type with at most one element. It is either empty or has a unique element.

All propositions are subsingletons because of proof irrelevance: false propositions are empty, and all proofs of a true proposition are equal to one another. Some non-propositional types are also subsingletons.

• intro :: (
• allEq (a b : α) : a = b

  Any two elements of a subsingleton are equal.

• )

theorem Subsingleton.elim {α : Sort u} [h : Subsingleton α] (a b : α) : a = b

If a type is a subsingleton, then all of its elements are equal.

theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b

If two types are equal and one of them is a subsingleton, then all of their elements are heterogeneously equal.

instance instSubsingleton (p : Prop) : Subsingleton p

instance instSubsingletonEmpty : Subsingleton Empty

instance instSubsingletonPEmpty : Subsingleton PEmpty

instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] : Subsingleton (α × β)

instance instSubsingletonDecidable (p : Prop) : Subsingleton (Decidable p)

theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.casesOn h h₂ h₁)

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop

An equivalence relation r : α → α → Prop is a relation that is

• reflexive: r x x,
• symmetric: r x y implies r y x, and
• transitive: r x y and r y z implies r x z.

Equality is an equivalence relation, and equivalence relations share many of the properties of equality.

• refl (x : α) : r x x

  An equivalence relation is reflexive: r x x

• symm {x y : α} : r x y → r y x

  An equivalence relation is symmetric: r x y implies r y x

• trans {x y z : α} : r x y → r y z → r x z

  An equivalence relation is transitive: r x y and r y z implies r x z

def emptyRelation {α : Sort u} : α → α → Prop

The empty relation is the relation on α which is always False.

Equations

• emptyRelation x✝¹ x✝ = False

def Subrelation {α : Sort u} (q r : α → α → Prop) : Prop

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

def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) : α → α → Prop

The inverse image of r : β → β → Prop by a function α → β is the relation s : α → α → Prop defined by s a b = r (f a) (f b).

Equations

• InvImage r f a₁ a₂ = r (f a₁) (f a₂)

inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop

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 → TransGen r a b

  If r a b, then TransGen r a b. This is the base case of the transitive closure.

• tail {α : Sort u} {r : α → α → Prop} {a b c : α} : TransGen r a b → r b c → TransGen r a c

  If TransGen r a b and r b c, then TransGen r a c. This is the inductive case of the transitive closure.

theorem Relation.TransGen.trans {α : Sort u} {r : α → α → Prop} {a b c : α} : TransGen r a b → TransGen r b c → TransGen r a c

The transitive closure is transitive.

Subtype

theorem Subtype.existsOfSubtype {α : Type u} {p : α → Prop} : { x : α // p x } → ∃ (x : α), p x

theorem Subtype.eq {α : Type u} {p : α → Prop} {a1 a2 : { x : α // p x }} : a1.val = a2.val → a1 = a2

theorem Subtype.eta {α : Type u} {p : α → Prop} (a : { x : α // p x }) (h : p a.val) : ⟨a.val, h⟩ = a

instance Subtype.instDecidableEq {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq { x : α // p x }

Equations

• ⟨b, h₂⟩.instDecidableEq ⟨b_1, h₂_1⟩ = if h : b = b_1 then isTrue ⋯ else isFalse ⋯

Sum

@[reducible]

def Sum.inhabitedLeft {α : Type u} {β : Type v} [Inhabited α] : Inhabited (α ⊕ β)

If the left type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

Equations

• Sum.inhabitedLeft = { default := Sum.inl default }

@[reducible]

def Sum.inhabitedRight {α : Type u} {β : Type v} [Inhabited β] : Inhabited (α ⊕ β)

If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are inhabited.

Equations

• Sum.inhabitedRight = { default := Sum.inr default }

instance Sum.nonemptyLeft {α : Type u} {β : Type v} [h : Nonempty α] : Nonempty (α ⊕ β)

instance Sum.nonemptyRight {α : Type u} {β : Type v} [h : Nonempty β] : Nonempty (α ⊕ β)

instance instDecidableEqSum {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β)

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

instance instNonemptyProd {α : Type u_1} {β : Type u_2} [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β)

instance instNonemptyMProd {α β : Type u_1} [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β)

instance instNonemptyPProd {α : Sort u_1} {β : Sort u_2} [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α ×' β)

instance instInhabitedProd {α : Type u_1} {β : Type u_2} [Inhabited α] [Inhabited β] : Inhabited (α × β)

Equations

• instInhabitedProd = { default := (default, default) }

instance instInhabitedMProd {α β : Type u_1} [Inhabited α] [Inhabited β] : Inhabited (MProd α β)

Equations

• instInhabitedMProd = { default := ⟨default, default⟩ }

instance instInhabitedPProd {α : Sort u_1} {β : Sort u_2} [Inhabited α] [Inhabited β] : Inhabited (α ×' β)

Equations

• instInhabitedPProd = { default := ⟨default, default⟩ }

instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] : DecidableEq (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance instBEqProd {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : BEq (α × β)

Equations

• instBEqProd = { beq := fun (x x_1 : α × β) => match x with | (a₁, b₁) => match x_1 with | (a₂, b₂) => a₁ == a₂ && b₁ == b₂ }

def Prod.lexLt {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s t : α × β) : Prop

Lexicographical order for products.

Two pairs are lexicographically ordered if their first elements are ordered or if their first elements are equal and their second elements are ordered.

Equations

• s.lexLt t = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)

instance Prod.lexLtDec {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DecidableEq α] [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)] (s t : α × β) : Decidable (s.lexLt t)

Equations

• x✝¹.lexLtDec x✝ = inferInstanceAs (Decidable (x✝¹.fst < x✝.fst ∨ x✝¹.fst = x✝.fst ∧ x✝¹.snd < x✝.snd))

theorem Prod.lexLt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] (s t : α × β) : s.lexLt t = (s.fst < t.fst ∨ s.fst = t.fst ∧ s.snd < t.snd)

theorem Prod.eta {α : Type u_1} {β : Type u_2} (p : α × β) : (p.fst, p.snd) = p

def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂

Transforms a pair by applying functions to both elements.

Examples:

• (1, 2).map (· + 1) (· * 3) = (2, 6)
• (1, 2).map toString (· * 3) = ("1", 6)

Equations

• Prod.map f g (a', b') = (f a', g b')

@[simp]

theorem Prod.map_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α) (y : γ) : map f g (x, y) = (f x, g y)

@[simp]

theorem Prod.map_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (map f g x).fst = f x.fst

@[simp]

theorem Prod.map_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (map f g x).snd = g x.snd

Dependent products

theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} : (x : α) ×' p x → ∃ (x : α), p x

theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} (h₁ : a₁ = a₂) (h₂ : h₁ ▸ b₁ = b₂) : ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

Universe polymorphic unit

theorem PUnit.subsingleton (a b : PUnit) : a = b

theorem PUnit.eq_punit (a : PUnit) : a = unit

instance instSubsingletonPUnit : Subsingleton PUnit

instance instInhabitedPUnit : Inhabited PUnit

Equations

• instInhabitedPUnit = { default := PUnit.unit }

instance instDecidableEqPUnit : DecidableEq PUnit

Equations

• instDecidableEqPUnit a b = isTrue ⋯

Setoid

class Setoid (α : Sort u) : Sort (max 1 u)

A setoid is a type with a distinguished equivalence relation, denoted ≈.

The Quotient type constructor requires a Setoid instance.

• r : α → α → Prop

  x ≈ y is the distinguished equivalence relation of a setoid.

• iseqv : Equivalence r

  The relation x ≈ y is an equivalence relation.

instance instHasEquivOfSetoid {α : Sort u} [Setoid α] : HasEquiv α

Equations

• instHasEquivOfSetoid = { Equiv := Setoid.r }

theorem Setoid.refl {α : Sort u} [Setoid α] (a : α) : a ≈ a

A setoid's equivalence relation is reflexive.

theorem Setoid.symm {α : Sort u} [Setoid α] {a b : α} (hab : a ≈ b) : b ≈ a

A setoid's equivalence relation is symmetric.

theorem Setoid.trans {α : Sort u} [Setoid α] {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c

A setoid's equivalence relation is transitive.

Propositional extensionality

axiom propext {a b : Prop} : (a ↔ b) → a = b

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.

theorem Eq.propIntro {a b : Prop} (h₁ : a → b) (h₂ : b → a) : a = b

instance instDecidableEqOfIff {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q)

Equations

• instDecidableEqOfIff = isTrue ⋯
• instDecidableEqOfIff = isFalse ⋯

theorem Nat.succ.inj {m n : Nat} : m.succ = n.succ → m = n

theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v)

@[simp]

theorem beq_iff_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = true ↔ a = b

Prop lemmas

def Not.elim {a : Prop} {α : Sort u_1} (H1 : ¬a) (H2 : a) : α

Ex falso for negation: from ¬a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the Not namespace so that projection notation can be used.

Equations

• H1.elim H2 = absurd H2 H1

@[reducible, inline]

abbrev And.elim {a b : Prop} {α : Sort u_1} (f : a → b → α) (h : a ∧ b) : α

Non-dependent eliminator for And.

Equations

• And.elim f h = f ⋯ ⋯

def Iff.elim {a b : Prop} {α : Sort u_1} (f : (a → b) → (b → a) → α) (h : a ↔ b) : α

Non-dependent eliminator for Iff.

Equations

• Iff.elim f h = f ⋯ ⋯

theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b

Iff can now be used to do substitutions in a calculation

theorem Not.intro {a : Prop} (h : a → False) : ¬a

theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) : ¬a

theorem not_congr {a b : Prop} (h : a ↔ b) : ¬a ↔ ¬b

theorem not_not_not {a : Prop} : ¬¬¬a ↔ ¬a

theorem iff_of_true {a b : Prop} (ha : a) (hb : b) : a ↔ b

theorem iff_of_false {a b : Prop} (ha : ¬a) (hb : ¬b) : a ↔ b

theorem iff_true_left {a b : Prop} (ha : a) : (a ↔ b) ↔ b

theorem iff_true_right {a b : Prop} (ha : a) : (b ↔ a) ↔ b

theorem iff_false_left {a b : Prop} (ha : ¬a) : (a ↔ b) ↔ ¬b

theorem iff_false_right {a b : Prop} (ha : ¬a) : (b ↔ a) ↔ ¬b

theorem of_iff_true {a : Prop} (h : a ↔ True) : a

theorem iff_true_intro {a : Prop} (h : a) : a ↔ True

theorem eq_iff_true_of_subsingleton {α : Sort u_1} [Subsingleton α] (x y : α) : x = y ↔ True

theorem not_of_iff_false {p : Prop} : (p ↔ False) → ¬p

theorem iff_false_intro {a : Prop} (h : ¬a) : a ↔ False

theorem not_iff_false_intro {a : Prop} (h : a) : ¬a ↔ False

theorem not_true : ¬True ↔ False

theorem not_false_iff : ¬False ↔ True

theorem Eq.to_iff {a b : Prop} : a = b → (a ↔ b)

theorem iff_of_eq {a b : Prop} : a = b → (a ↔ b)

theorem neq_of_not_iff {a b : Prop} : ¬(a ↔ b) → a ≠ b

theorem iff_iff_eq {a b : Prop} : (a ↔ b) ↔ a = b

@[simp]

theorem eq_iff_iff {a b : Prop} : a = b ↔ (a ↔ b)

theorem eq_self_iff_true {α : Sort u_1} (a : α) : a = a ↔ True

theorem ne_self_iff_false {α : Sort u_1} (a : α) : a ≠ a ↔ False

theorem false_of_true_iff_false (h : True ↔ False) : False

theorem false_of_true_eq_false (h : True = False) : False

theorem true_eq_false_of_false : False → True = False

theorem iff_def {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (b → a)

theorem iff_def' {a b : Prop} : (a ↔ b) ↔ (b → a) ∧ (a → b)

theorem true_iff_false : (True ↔ False) ↔ False

theorem false_iff_true : (False ↔ True) ↔ False

@[simp]

theorem iff_not_self {a : Prop} : ¬(a ↔ ¬a)

theorem heq_self_iff_true {α : Sort u_1} (a : α) : HEq a a ↔ True

implies

theorem not_not_of_not_imp {a b : Prop} : ¬(a → b) → ¬¬a

theorem not_of_not_imp {b a : Prop} : ¬(a → b) → ¬b

@[simp]

theorem imp_not_self {a : Prop} : a → ¬a ↔ ¬a

theorem imp_intro {α β : Prop} (h : α) : β → α

theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → c → d

theorem imp_iff_right {b a : Prop} (ha : a) : a → b ↔ b

theorem imp_true_iff (α : Sort u) : α → True ↔ True

theorem false_imp_iff (a : Prop) : False → a ↔ True

theorem true_imp_iff {α : Prop} : True → α ↔ α

@[simp]

theorem imp_self {a : Prop} : a → a ↔ True

@[simp]

theorem imp_false {a : Prop} : a → False ↔ ¬a

theorem imp.swap {a b c : Prop} : a → b → c ↔ b → a → c

theorem imp_not_comm {a b : Prop} : a → ¬b ↔ b → ¬a

theorem imp_congr_left {a b c : Prop} (h : a ↔ b) : a → c ↔ b → c

theorem imp_congr_right {a b c : Prop} (h : a → (b ↔ c)) : a → b ↔ a → c

theorem imp_congr_ctx {a b c d : Prop} (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : a → b ↔ c → d

theorem imp_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) : a → b ↔ c → d

theorem imp_iff_not {a b : Prop} (hb : ¬b) : a → b ↔ ¬a

Quotients

axiom Quot.sound {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → mk r a = mk r b

The quotient axiom, which asserts the equality of elements related by the quotient's relation.

The relation r does not need to be an equivalence relation to use this axiom. When r is not an equivalence relation, the quotient is with respect to the equivalence relation generated by r.

Quot.sound is part of the built-in primitive quotient type:

• Quot is the built-in quotient type.
• Quot.mk places elements of the underlying type α into the quotient.
• Quot.lift allows the definition of functions from the quotient to some other type.
• Quot.ind is used to write proofs about quotients by assuming that all elements are constructed with Quot.mk; it is analogous to the recursor for a structure.

Quotient types are described in more detail in the Lean Language Reference.

theorem Quot.liftBeta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) (a : α) : lift f c (mk r a) = f a

theorem Quot.indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : ∀ (a : α), motive (mk r a)) (a : α) : ⋯ = ⋯

@[reducible, inline]

abbrev Quot.liftOn {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : Quot r) (f : α → β) (c : ∀ (a b : α), r a b → f a = f b) : β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's relation.

Given a relation r : α → α → Prop and a quotient's value q : Quot r, applying a f : α → β requires a proof c that f respects r. In this case, Quot.liftOn q f h : β evaluates to the result of applying f to the underlying value in α from q.

Quot.liftOn is a version of the built-in primitive Quot.lift with its parameters re-ordered.

Quotient types are described in more detail in the Lean Language Reference.

Equations

• q.liftOn f c = Quot.lift f c q

theorem Quot.inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r) (h : ∀ (a : α), motive (mk r a)) : motive q

theorem Quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) : ∃ (a : α), mk r a = q

@[reducible, macro_inline]

def Quot.indep {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (mk r a)) (a : α) : PSigma motive

Auxiliary definition for Quot.rec.

Equations

• Quot.indep f a = ⟨Quot.mk r a, f a⟩

theorem Quot.indepCoherent {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (a b : α) : r a b → Quot.indep f a = Quot.indep f b

theorem Quot.liftIndepPr1 {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (q : Quot r) : (lift (Quot.indep f) ⋯ q).fst = q

@[reducible, inline]

abbrev Quot.rec {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (f : (a : α) → motive (mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) (q : Quot r) : motive q

A dependent recursion principle for Quot. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

• Quot.lift is useful for defining non-dependent functions.
• Quot.ind is useful for proving theorems about quotients.
• Quot.recOnSubsingleton can be used whenever the target type is a Subsingleton.
• Quot.hrecOn uses heterogeneous equality instead of rewriting with Quot.sound.

Quot.recOn is a version of this recursor that takes the quotient parameter first.

Equations

• Quot.rec f h q = Eq.ndrecOn ⋯ (Quot.lift (Quot.indep f) ⋯ q).snd

@[reducible, inline]

abbrev Quot.recOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) : motive q

A dependent recursion principle for Quot that takes the quotient first. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

• Quot.lift is useful for defining non-dependent functions.
• Quot.ind is useful for proving theorems about quotients.
• Quot.recOnSubsingleton can be used whenever the target type is a Subsingleton.
• Quot.hrecOn uses heterogeneous equality instead of rewriting with Quot.sound.

Quot.rec is a version of this recursor that takes the quotient parameter last.

Equations

• Quot.recOn q f h = Quot.rec f h q

@[reducible, inline]

abbrev Quot.recOnSubsingleton {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (mk r a))] (q : Quot r) (f : (a : α) → motive (mk r a)) : motive q

An alternative induction principle for quotients that can be used when the target type is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's relation is trivial, so any function can be lifted.

Quot.rec does not assume that the type is a subsingleton.

Equations

• Quot.recOnSubsingleton q f = Quot.rec (fun (a : α) => f a) ⋯ q

@[reducible, inline]

abbrev Quot.hrecOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (mk r a)) (c : ∀ (a b : α), r a b → HEq (f a) (f b)) : motive q

A dependent recursion principle for Quot that uses heterogeneous equality, analogous to a recursor for a structure.

Quot.recOn is a version of this recursor that uses Eq instead of HEq.

Equations

• Quot.hrecOn q f c = Quot.recOn q f ⋯

def Quotient {α : Sort u} (s : Setoid α) : Sort u

Quotient types coarsen the propositional equality for a type so that terms related by some equivalence relation are considered equal. The equivalence relation is given by an instance of Setoid.

Set-theoretically, Quotient s can seen as the set of equivalence classes of α modulo the Setoid instance's relation s.r. Functions from Quotient s must prove that they respect s.r: to define a function f : Quotient s → β, it is necessary to provide f' : α → β and prove that for all x : α and y : α, s.r x y → f' x = f' y. Quotient.lift implements this operation.

The key quotient operators are:

• Quotient.mk places elements of the underlying type α into the quotient.
• Quotient.lift allows the definition of functions from the quotient to some other type.
• Quotient.sound asserts the equality of elements related by r
• Quotient.ind is used to write proofs about quotients by assuming that all elements are constructed with Quotient.mk.

Quotient is built on top of the primitive quotient type Quot, which does not require a proof that the relation is an equivalence relation. Quotient should be used instead of Quot for relations that actually are equivalence relations.

Equations

• Quotient s = Quot Setoid.r

@[inline]

def Quotient.mk {α : Sort u} (s : Setoid α) (a : α) : Quotient s

Places an element of a type into the quotient that equates terms according to an equivalence relation.

The setoid instance is provided explicitly. Quotient.mk' uses instance synthesis instead.

Given v : α, Quotient.mk s v : Quotient s is like v, except all observations of v's value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

Equations

• Quotient.mk s a = Quot.mk Setoid.r a

def Quotient.mk' {α : Sort u} [s : Setoid α] (a : α) : Quotient s

Places an element of a type into the quotient that equates terms according to an equivalence relation.

The equivalence relation is found by synthesizing a Setoid instance. Quotient.mk instead expects the instance to be provided explicitly.

Given v : α, Quotient.mk' v : Quotient s is like v, except all observations of v's value must respect s.r. Quotient.lift allows values in a quotient to be mapped to other types, so long as the mapping respects s.r.

Equations

• Quotient.mk' a = Quotient.mk s a

theorem Quotient.sound {α : Sort u} {s : Setoid α} {a b : α} : a ≈ b → Quotient.mk s a = Quotient.mk s b

The quotient axiom, which asserts the equality of elements related in the setoid.

Because Quotient is built on a lower-level type Quot, Quotient.sound is implemented as a theorem. It is derived from Quot.sound, the soundness axiom for the lower-level quotient type Quot.

@[reducible, inline]

abbrev Quotient.lift {α : Sort u} {β : Sort v} {s : Setoid α} (f : α → β) : (∀ (a b : α), a ≈ b → f a = f b) → Quotient s → β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's equivalence relation.

Given s : Setoid α and a quotient Quotient s, applying a function f : α → β requires a proof h that f respects the equivalence relation s.r. In this case, the function Quotient.lift f h : Quotient s → β computes the same values as f.

Quotient.liftOn is a version of this operation that takes the quotient value as its first explicit parameter.

Equations

• Quotient.lift f = Quot.lift f

theorem Quotient.ind {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} : (∀ (a : α), motive (Quotient.mk s a)) → ∀ (q : Quotient s), motive q

A reasoning principle for quotients that allows proofs about quotients to assume that all values are constructed with Quotient.mk.

@[reducible, inline]

abbrev Quotient.liftOn {α : Sort u} {β : Sort v} {s : Setoid α} (q : Quotient s) (f : α → β) (c : ∀ (a b : α), a ≈ b → f a = f b) : β

Lifts a function from an underlying type to a function on a quotient, requiring that it respects the quotient's equivalence relation.

Given s : Setoid α and a quotient value q : Quotient s, applying a function f : α → β requires a proof c that f respects the equivalence relation s.r. In this case, the term Quotient.liftOn q f h : β reduces to the result of applying f to the underlying α value.

Quotient.lift is a version of this operation that takes the quotient value last, rather than first.

Equations

• q.liftOn f c = Quot.liftOn q f c

theorem Quotient.inductionOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Prop} (q : Quotient s) (h : ∀ (a : α), motive (Quotient.mk s a)) : motive q

The analogue of Quot.inductionOn: every element of Quotient s is of the form Quotient.mk s a.

theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) : ∃ (a : α), Quotient.mk s a = q

@[inline]

def Quotient.rec {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) (q : Quotient s) : motive q

A dependent recursion principle for Quotient. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

• Quotient.lift is useful for defining non-dependent functions.
• Quotient.ind is useful for proving theorems about quotients.
• Quotient.recOnSubsingleton can be used whenever the target type is a Subsingleton.
• Quotient.hrecOn uses heterogeneous equality instead of rewriting with Quotient.sound.

Quotient.recOn is a version of this recursor that takes the quotient parameter first.

Equations

• Quotient.rec f h q = Quot.rec f h q

@[reducible, inline]

abbrev Quotient.recOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (h : ∀ (a b : α) (p : a ≈ b), ⋯ ▸ f a = f b) : motive q

A dependent recursion principle for Quotient. It is analogous to the recursor for a structure, and can be used when the resulting type is not necessarily a proposition.

While it is very general, this recursor can be tricky to use. The following simpler alternatives may be easier to use:

• Quotient.lift is useful for defining non-dependent functions.
• Quotient.ind is useful for proving theorems about quotients.
• Quotient.recOnSubsingleton can be used whenever the target type is a Subsingleton.
• Quotient.hrecOn uses heterogeneous equality instead of rewriting with Quotient.sound.

Quotient.rec is a version of this recursor that takes the quotient parameter last.

Equations

• Quotient.recOn q f h = Quot.recOn q f h

@[reducible, inline]

abbrev Quotient.recOnSubsingleton {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quotient.mk s a))] (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) : motive q

An alternative recursion or induction principle for quotients that can be used when the target type is a subsingleton, in which all elements are equal.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial, so any function can be lifted.

Quotient.rec does not assume that the target type is a subsingleton.

Equations

• Quotient.recOnSubsingleton q f = Quot.recOnSubsingleton q f

@[reducible, inline]

abbrev Quotient.hrecOn {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f : (a : α) → motive (Quotient.mk s a)) (c : ∀ (a b : α), a ≈ b → HEq (f a) (f b)) : motive q

A dependent recursion principle for Quotient that uses heterogeneous equality, analogous to a recursor for a structure.

Quotient.recOn is a version of this recursor that uses Eq instead of HEq.

Equations

• Quotient.hrecOn q f c = Quot.hrecOn q f c

@[reducible, inline]

abbrev Quotient.lift₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : φ

Lifts a binary function from the underlying types to a binary function on quotients. The function must respect both quotients' equivalence relations.

Quotient.lift is a version of this operation for unary functions. Quotient.liftOn₂ is a version that take the quotient parameters first.

Equations

• Quotient.lift₂ f c q₁ q₂ = Quotient.lift (fun (a₁ : α) => Quotient.lift (f a₁) ⋯ q₂) ⋯ q₁

@[reducible, inline]

abbrev Quotient.liftOn₂ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → φ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) : φ

Lifts a binary function from the underlying types to a binary function on quotients. The function must respect both quotients' equivalence relations.

Quotient.liftOn is a version of this operation for unary functions. Quotient.lift₂ is a version that take the quotient parameters last.

Equations

• q₁.liftOn₂ q₂ f c = Quotient.lift₂ f c q₁ q₂

theorem Quotient.ind₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) (q₁ : Quotient s₁) (q₂ : Quotient s₂) : motive q₁ q₂

theorem Quotient.inductionOn₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (h : ∀ (a : α) (b : β), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) : motive q₁ q₂

theorem Quotient.inductionOn₃ {α : Sort uA} {β : Sort uB} {φ : Sort uC} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid φ} {motive : Quotient s₁ → Quotient s₂ → Quotient s₃ → Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃) (h : ∀ (a : α) (b : β) (c : φ), motive (Quotient.mk s₁ a) (Quotient.mk s₂ b) (Quotient.mk s₃ c)) : motive q₁ q₂ q₃

theorem Quotient.exact {α : Sort u} {s : Setoid α} {a b : α} : Quotient.mk s a = Quotient.mk s b → a ≈ b

If two values are equal in a quotient, then they are related by its equivalence relation.

@[reducible, inline]

abbrev Quotient.recOnSubsingleton₂ {α : Sort uA} {β : Sort uB} {s₁ : Setoid α} {s₂ : Setoid β} {motive : Quotient s₁ → Quotient s₂ → Sort uC} [s : ∀ (a : α) (b : β), Subsingleton (motive (Quotient.mk s₁ a) (Quotient.mk s₂ b))] (q₁ : Quotient s₁) (q₂ : Quotient s₂) (g : (a : α) → (b : β) → motive (Quotient.mk s₁ a) (Quotient.mk s₂ b)) : motive q₁ q₂

An alternative induction or recursion operator for defining binary operations on quotients that can be used when the target type is a subsingleton.

In these cases, the proof that the function respects the quotient's equivalence relation is trivial, so any function can be lifted.

Equations

• Quotient.recOnSubsingleton₂ q₁ q₂ g = Quot.recOnSubsingleton q₁ fun (a : α) => Quot.recOnSubsingleton q₂ fun (a_1 : β) => g a a_1

instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a ≈ b)] : DecidableEq (Quotient s)

Equations

• q₁.decidableEq q₂ = Quotient.recOnSubsingleton₂ q₁ q₂ fun (a₁ a₂ : α) => match d a₁ a₂ with | isTrue h₁ => isTrue ⋯ | isFalse h₂ => isFalse ⋯

Function extensionality

theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = g

Function extensionality. If two functions return equal results for all possible arguments, then they are equal.

It is called “extensionality” because it provides a way to prove two objects equal based on the properties of the underlying mathematical functions, rather than based on the syntax used to denote them. Function extensionality is a theorem that can be proved using quotient types.

instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ (a : α), Subsingleton (β a)] : Subsingleton ((a : α) → β a)

Squash

def Squash (α : Sort u) : Sort u

The quotient of α by the universal relation. The elements of Squash α are those of α, but all of them are equal and cannot be distinguished.

Squash α is a Subsingleton: it is empty if α is empty, otherwise it has just one element. It is the “universal Subsingleton” mapped from α.

Nonempty α also has these properties. It is a proposition, which means that its elements (i.e. proofs) are erased from compiled code and represented by a dummy value. Squash α is a Type u, and its representation in compiled code is identical to that of α.

Consequently, Squash.lift may extract an α value into any subsingleton type β, while Nonempty.rec can only do the same when β is a proposition.

Equations

• Squash α = Quot fun (x x : α) => True

def Squash.mk {α : Sort u} (x : α) : Squash α

Places a value into its squash type, in which it cannot be distinguished from any other.

Equations

• Squash.mk x = Quot.mk (fun (x x : α) => True) x

theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (mk a)) (q : Squash α) : motive q

A reasoning principle that allows proofs about squashed types to assume that all values are constructed with Squash.mk.

@[inline]

def Squash.lift {α : Sort u_1} {β : Sort u_2} [Subsingleton β] (s : Squash α) (f : α → β) : β

Extracts a squashed value into any subsingleton type.

If β is a subsingleton, a function α → β cannot distinguish between elements of α and thus automatically respects the universal relation that Squash quotients with.

Equations

• s.lift f = Quot.lift f ⋯ s

instance instSubsingletonSquash {α : Sort u_1} : Subsingleton (Squash α)

Kernel reduction hints

axiom Lean.trustCompiler : True

Depends on the correctness of the Lean compiler, interpreter, and all [implemented_by ...] and [extern ...] annotations.

opaque Lean.reduceBool (b : Bool) : Bool

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 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.

opaque Lean.reduceNat (n : Nat) : Nat

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).

axiom Lean.ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b

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 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.

axiom Lean.ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b

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 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.

opaque Lean.opaqueId {α : Sort u} (x : α) : α

The term opaqueId x will not be reduced by the kernel.

@[simp]

theorem ge_iff_le {α : Type u_1} [LE α] {x y : α} : x ≥ y ↔ y ≤ x

@[simp]

theorem gt_iff_lt {α : Type u_1} [LT α] {x y : α} : x > y ↔ y < x

theorem le_of_eq_of_le {α : Type u_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c

theorem le_of_le_of_eq {α : Type u_1} {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c

theorem lt_of_eq_of_lt {α : Type u_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) : a < c

theorem lt_of_lt_of_eq {α : Type u_1} {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c

class Std.Associative {α : Sort u} (op : α → α → α) : Prop

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).

class Std.Commutative {α : Sort u} (op : α → α → α) : Prop

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.

class Std.IdempotentOp {α : Sort u} (op : α → α → α) : Prop

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.

class Std.LeftIdentity {α : Sort u} {β : Sort u_1} (op : α → β → β) (o : outParam α) : Prop

LeftIdentify op o indicates o is a left 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.

class Std.LawfulLeftIdentity {α : Sort u} {β : Sort u_1} (op : α → β → β) (o : outParam α) extends Std.LeftIdentity op o : Prop

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.

class Std.RightIdentity {α : Sort u} {β : Sort u_1} (op : α → β → α) (o : outParam β) : Prop

RightIdentify op o indicates o is a right identity o 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.

class Std.LawfulRightIdentity {α : Sort u} {β : Sort u_1} (op : α → β → α) (o : outParam β) extends Std.RightIdentity op o : Prop

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.

class Std.Identity {α : Sort u} (op : α → α → α) (o : outParam α) extends Std.LeftIdentity op o, Std.RightIdentity op o : Prop

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.

class Std.LawfulIdentity {α : Sort u} (op : α → α → α) (o : outParam α) extends Std.Identity op o, Std.LawfulLeftIdentity op o, Std.LawfulRightIdentity op o : Prop

LawfulIdentity op o indicates o is a verified left and right identity of op.

• left_id (a : α) : op o a = a
• right_id (a : α) : op a o = a

class Std.LawfulCommIdentity {α : Sort u} (op : α → α → α) (o : outParam α) [hc : Commutative op] extends Std.LawfulIdentity op o : Prop

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.

• left_id (a : α) : op o a = a
• right_id (a : α) : op a o = a

instance Std.instCommutativeOr : Commutative Or

instance Std.instCommutativeAnd : Commutative And

instance Std.instCommutativeIff : Commutative Iff

class Std.Refl {α : Sort u} (r : α → α → Prop) : Prop

Refl r means the binary relation r is reflexive, that is, r x x always holds.

• refl (a : α) : r a a

  A reflexive relation satisfies r a a.

class Std.Antisymm {α : Sort u} (r : α → α → Prop) : Prop

Antisymm r says that r is antisymmetric, that is, r a b → r b a → a = b.

• antisymm (a b : α) : r a b → r b a → a = b

  An antisymmetric relation r satisfies r a b → r b a → a = b.

@[reducible, inline, deprecated Std.Antisymm (since := "2024-10-16")]

abbrev Antisymm {α : Sort u} (r : α → α → Prop) : Prop

Antisymm r says that r is antisymmetric, that is, r a b → r b a → a = b.

Equations

• Antisymm r = Std.Antisymm r

class Std.Asymm {α : Sort u} (r : α → α → Prop) : Prop

Asymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

• asymm (a b : α) : r a b → ¬r b a

  An asymmetric relation satisfies r a b → ¬ r b a.

class Std.Total {α : Sort u} (r : α → α → Prop) : Prop

Total X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

• total (a b : α) : r a b ∨ r b a

  A total relation satisfies r a b ∨ r b a.

class Std.Irrefl {α : Sort u} (r : α → α → Prop) : Prop

Irrefl r means the binary relation r is irreflexive, that is, r x x never holds.

• irrefl (a : α) : ¬r a a

  An irreflexive relation satisfies ¬ r a a.