Documentation

Init.Core

source
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
source
theorem id_def {α : Sort u} (a : α) :
id a = a
source
@[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
Instances For
source
@[simp]
theorem Function.const_apply {β : Sort u_1} {α : Sort u_2} {y : β} {x : α} :
const α y x = y
source
@[simp]
theorem Function.comp_apply {β : Sort u_1} {δ : Sort u_2} {α : Sort u_3} {f : β → δ} {g : α → β} {x : α} :
(f ∘ g) x = f (g x)
source
theorem Function.comp_def {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} (f : β → δ) (g : α → β) :
f ∘ g = fun (x : α) => f (g x)
source
@[simp]
theorem Function.const_comp {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {c : γ} :
const β c ∘ f = const α c
source
@[simp]
theorem Function.comp_const {β : Sort u_1} {γ : Sort u_2} {α : Sort u_3} {f : β → γ} {b : β} :
f ∘ const α b = const α (f b)
source
@[simp]
theorem Function.true_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} :
(fun (x : β) => true) ∘ f = fun (x : α) => true
source
@[simp]
theorem Function.false_comp {α : Sort u_1} {β : Sort u_2} {f : α → β} :
(fun (x : β) => false) ∘ f = fun (x : α) => false
source
@[simp]
theorem Function.comp_id {α : Sort u_1} {β : Sort u_2} (f : α → β) :
f ∘ id = f
source
@[simp]
theorem Function.id_comp {α : Sort u_1} {β : Sort u_2} (f : α → β) :
id ∘ f = f
source
@[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
source
instance instDecidableEqEmpty :
DecidableEq Empty

Decidable equality for Empty

Equations
source
@[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.

Equations
    source
    instance instDecidableEqPEmpty :
    DecidableEq PEmpty

    Decidable equality for PEmpty

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

    Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[simp]
    theorem Thunk.sizeOf_eq {α : Type u_1} [SizeOf α] (a : Thunk α) :
    sizeOf a = 1 + sizeOf a.get
    source
    instance thunkCoe {α : Type u_1} :
    CoeTail α (Thunk α)
    Equations

    definitions #

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

    • )
    Instances For
    source
    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
    source
    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
    source
    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 α ⊕ β.

    Instances For
    source
    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
    source
    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 α ⊕' β.

    Instances For
    source
    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
    source
    @[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
    source
    @[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
    source
    instance PSum.nonemptyLeft {α : Sort u_1} {β : Sort u_2} [h : Nonempty α] :
    Nonempty (α ⊕' β)
    source
    instance PSum.nonemptyRight {β : Sort u_1} {α : Sort u_2} [h : Nonempty β] :
    Nonempty (α ⊕' β)
    source
    @[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.

    Instances For
    source
    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.

    Instances For
    source
    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.

    Instances For
    source
    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.

    Instances For
    source
    instance instInhabitedForInStep {a✝ : Type u_1} [Inhabited a✝] :
    Inhabited (ForInStep a✝)
    Equations
    source
    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.

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

    Instances
    source
    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

    source
    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

    source
    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

    source
    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

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

    set notation #

    source
    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.
    Instances
    source
    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.
    Instances
    source
    @[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
    source
    @[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
    source
    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.
    Instances
    source
    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.
    Instances
    source
    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.
    Instances
    source
    def «term_⊆_» :
    Lean.TrailingParserDescr

    Subset relation: a ⊆ b

    Conventions for notations in identifiers:

    • The recommended spelling of ⊆ in identifiers is subset.
    Equations
    source
    def «term_⊂_» :
    Lean.TrailingParserDescr

    Strict subset relation: a ⊂ b

    Conventions for notations in identifiers:

    • The recommended spelling of ⊂ in identifiers is ssubset.
    Equations
    source
    def «term_⊇_» :
    Lean.TrailingParserDescr

    Superset relation: a ⊇ b

    Conventions for notations in identifiers:

    • The recommended spelling of ⊇ in identifiers is superset (prefer ⊆ over ⊇).
    Equations
    source
    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
    source
    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
    source
    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
    source
    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

    collections #

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

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

    Instances
    source
    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.
    Instances
    source
    class LawfulSingleton (α : Type u) (β : Type v) [EmptyCollection β] [Insert α β] [Singleton α β] :
    Prop

    insert x ∅ = {x}

    Instances
    source
    @[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}
    source
    @[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}
    source
    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 }.

    Instances
      source
      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. In particular, calling Task.get in a task continuation with (sync := true) will panic as the continuation is decidedly not "cheap" in this case and deadlocks may otherwise occur. The waited-upon task should instead be returned and unwrapped using Task.bind/IO.bindTask.

      • )
      Instances For
      source
      instance instInhabitedTask {a✝ : Type u_1} [Inhabited a✝] :
      Inhabited (Task a✝)
      Equations
      source
      instance instNonemptyTask {α✝ : Type u_1} [Nonempty α✝] :
      Nonempty (Task α✝)
      source
      @[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
      source
      def Task.Priority.default :
      Priority

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

      Equations
      source
      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
      source
      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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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

      Instances For
      source
      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.

      Instances For
      source
      @[simp]
      theorem Nat.add_zero (n : Nat) :
      n + 0 = n
      source
      theorem optParam_eq (α : Sort u) (default : α) :
      optParam α default = α

      Boolean operators #

      source
      @[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
      source
      @[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
      source
      @[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
      source
      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
      source
      class ReflBEq (α : Type u_1) [BEq α] :
      Prop

      ReflBEq α says that the BEq implementation is reflexive.

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

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

      Instances
      source
      @[simp]
      theorem BEq.rfl {α : Type u_1} [BEq α] [ReflBEq α] {a : α} :
      (a == a) = true
      source
      theorem BEq.refl {α : Type u_1} [BEq α] [ReflBEq α] (a : α) :
      (a == a) = true
      source
      theorem beq_of_eq {α : Type u_1} [BEq α] [ReflBEq α] {a b : α} :
      a = b → (a == b) = true
      source
      theorem not_eq_of_beq_eq_false {α : Type u_1} [BEq α] [ReflBEq α] {a b : α} (h : (a == b) = false) :
      ¬a = b
      source
      class LawfulBEq (α : Type u) [BEq α] extends ReflBEq α :
      Prop

      A Boolean equality test coincides with propositional equality.

      In other words:

      • a == b implies a = b.
      • a == a is true.
      • rfl {a : α} : (a == a) = 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.

      Instances
      source
      instance instLawfulBEqBool :
      LawfulBEq Bool
      source
      instance instLawfulBEq {α : Type u_1} [DecidableEq α] :
      LawfulBEq α
      source
      def instDecidableEqOfLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] :
      DecidableEq α

      Non-instance for DecidableEq from LawfulBEq. To use this, add attribute [local instance 5] instDecidableEqOfLawfulBEq at the top of a file.

      Equations
      source
      instance instLawfulBEqChar :
      LawfulBEq Char
      source
      instance instLawfulBEqString :
      LawfulBEq String

      Logical connectives and equality #

      source
      theorem trivial :
      True

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

      source
      theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) :
      ¬a
      source
      theorem not_false :
      ¬False
      source
      theorem not_not_intro {p : Prop} (h : p) :
      ¬¬p
      source
      theorem proof_irrel {a : Prop} (h₁ h₂ : a) :
      h₁ = h₂
      source
      @[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
      source
      @[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
      source
      theorem Eq.substr {α : Sort u} {p : α → Prop} {a b : α} (h₁ : b = a) (h₂ : p a) :
      p b
      source
      @[simp]
      theorem cast_eq {α : Sort u} (h : α = α) (a : α) :
      cast h a = a
      source
      @[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
      Instances For
      source
      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
      source
      theorem Ne.intro {α : Sort u} {a b : α} (h : a = b → False) :
      a ≠ b
      source
      theorem Ne.elim {α : Sort u} {a b : α} (h : a ≠ b) :
      a = b → False
      source
      theorem Ne.irrefl {α : Sort u} {a : α} (h : a ≠ a) :
      False
      source
      theorem Ne.symm {α : Sort u} {a b : α} (h : a ≠ b) :
      b ≠ a
      source
      theorem ne_comm {α : Sort u_1} {a b : α} :
      a ≠ b ↔ b ≠ a
      source
      theorem false_of_ne {α : Sort u} {a : α} :
      a ≠ a → False
      source
      theorem ne_false_of_self {p : Prop} :
      p → p ≠ False
      source
      theorem ne_true_of_not {p : Prop} :
      ¬p → p ≠ True
      source
      theorem true_ne_false :
      ¬True = False
      source
      theorem false_ne_true :
      False ≠ True
      source
      theorem Bool.of_not_eq_true {b : Bool} :
      ¬b = true → b = false
      source
      theorem Bool.of_not_eq_false {b : Bool} :
      ¬b = false → b = true
      source
      theorem ne_of_beq_false {α : Type u_1} [BEq α] [ReflBEq α] {a b : α} (h : (a == b) = false) :
      a ≠ b
      source
      theorem beq_false_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) :
      (a == b) = false
      source
      noncomputable def HEq.ndrec {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≍ b) :
      motive b

      Non-dependent recursor for HEq

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

      HEq.ndrec variant

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

      HEq.ndrec variant

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

      Substitution with heterogeneous equality.

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

      Heterogeneous equality is symmetric.

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

      Propositionally equal terms are also heterogeneously equal.

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

      Heterogeneous equality is transitive.

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

      Heterogeneous equality precomposes with propositional equality.

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

      Heterogeneous equality postcomposes with propositional equality.

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

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

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

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

      source
      theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v} {b : α} {refl : motive a ⋯} {h : a = b} {c : motive b h} :
      h ▸ refl ≍ c ↔ refl ≍ c

      Heterogeneous equality with an Eq.rec application on the left is equivalent to a heterogeneous equality on the original term.

      source
      theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v} {b : α} {refl : motive a ⋯} {h : a = b} {c : motive b h} :
      c ≍ h ▸ refl ↔ c ≍ refl

      Heterogeneous equality with an Eq.rec application on the right is equivalent to a heterogeneous equality on the original term.

      source
      theorem apply_eqRec {β : Sort u_1} {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort v) {b : α} {h : a = b} {c : motive a ⋯ → β} {d : motive b h} :
      Eq.rec (motive := fun (b : α) (h : a = b) => motive b h → β) c h d = c ((fun (h_1 : b = a) => Eq.ndrec (motive := fun {a : α} => (motive : (b : α) → a = b → Sort v) → {h : a = b} → {c : motive a ⋯ → β} → {d : motive b h} → motive a ⋯) (fun (motive : (b_1 : α) → b = b_1 → Sort v) {h : b = b} {c : motive b ⋯ → β} {d : motive b h} => d) h_1 motive) ⋯)

      Moves an cast using Eq.rec from the function to the argument. Note: because the motive isn't reliably detected by unification, it needs to be provided as an explicit parameter.

      source
      theorem heq_of_eqRec_eq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ : h₁ ▸ a = b) :
      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.

      source
      @[simp]
      theorem cast_heq {α β : Sort u} (h : α = β) (a : α) :
      cast h a ≍ a

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

      source
      theorem iff_iff_implies_and_implies {a b : Prop} :
      (a ↔ b) ↔ (a → b) ∧ (b → a)
      source
      theorem Iff.refl (a : Prop) :
      a ↔ a
      source
      theorem Iff.rfl {a : Prop} :
      a ↔ a
      source
      theorem Iff.of_eq {a b : Prop} (h : a = b) :
      a ↔ b
      source
      theorem Iff.trans {a b c : Prop} (h₁ : a ↔ b) (h₂ : b ↔ c) :
      a ↔ c
      source
      instance instTransIff :
      Trans Iff Iff Iff
      Equations
      source
      theorem Eq.comm {α : Sort u_1} {a b : α} :
      a = b ↔ b = a
      source
      theorem eq_comm {α : Sort u_1} {a b : α} :
      a = b ↔ b = a
      source
      theorem HEq.comm {α β : Sort u_1} {a : α} {b : β} :
      a ≍ b ↔ b ≍ a
      source
      theorem heq_comm {α β : Sort u_1} {a : α} {b : β} :
      a ≍ b ↔ b ≍ a
      source
      theorem Iff.symm {a b : Prop} (h : a ↔ b) :
      b ↔ a
      source
      theorem Iff.comm {a b : Prop} :
      (a ↔ b) ↔ (b ↔ a)
      source
      theorem iff_comm {a b : Prop} :
      (a ↔ b) ↔ (b ↔ a)
      source
      theorem And.symm {a b : Prop} :
      a ∧ b → b ∧ a
      source
      theorem And.comm {a b : Prop} :
      a ∧ b ↔ b ∧ a
      source
      theorem and_comm {a b : Prop} :
      a ∧ b ↔ b ∧ a
      source
      theorem Or.symm {a b : Prop} :
      a ∨ b → b ∨ a
      source
      theorem Or.comm {a b : Prop} :
      a ∨ b ↔ b ∨ a
      source
      theorem or_comm {a b : Prop} :
      a ∨ b ↔ b ∨ a

      Exists #

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

      Decidable #

      source
      @[simp]
      theorem decide_true (h : Decidable True) :
      decide True = true
      source
      @[simp]
      theorem decide_false (h : Decidable False) :
      decide False = false
      source
      @[inline]
      def toBoolUsing {p : Prop} (d : Decidable p) :
      Bool

      Similar to decide, but uses an explicit instance

      Equations
      source
      theorem toBoolUsing_eq_true {p : Prop} (d : Decidable p) (h : p) :
      toBoolUsing d = true
      source
      theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) :
      p
      source
      theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) :
      ¬p
      source
      @[reducible, inline, deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
      abbrev ofBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d = true) :
      p
      Equations
      source
      @[reducible, inline, deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
      abbrev ofBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) :
      ¬p
      Equations
      source
      instance instDecidableTrue :
      Decidable True
      Equations
      source
      instance instDecidableFalse :
      Decidable False
      Equations
      source
      @[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
      source
      theorem Decidable.em (p : Prop) [Decidable p] :
      p ∨ ¬p
      source
      theorem Decidable.byContradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) :
      p
      source
      theorem Decidable.of_not_not {p : Prop} [Decidable p] :
      ¬¬p → p
      source
      theorem Decidable.not_and_iff_or_not {p q : Prop} [d₁ : Decidable p] [d₂ : Decidable q] :
      ¬(p ∧ q) ↔ ¬p ∨ ¬q
      source
      @[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
      source
      @[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
      source
      @[macro_inline]
      instance instDecidableForall {p q : Prop} [Decidable p] [Decidable q] :
      Decidable (p → q)
      Equations
      source
      instance instDecidableIff {p q : Prop} [Decidable p] [Decidable q] :
      Decidable (p ↔ q)
      Equations

      if-then-else expression theorems #

      source
      theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} :
      (if c then t else e) = t
      source
      theorem if_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t e : α} :
      (if c then t else e) = e
      source
      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
      source
      theorem dif_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t : c → α} {e : ¬c → α} :
      dite c t e = t hc
      source
      theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c → α} {e : ¬c → α} :
      dite c t e = e hnc
      source
      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
      source
      instance instDecidableIte {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] :
      Decidable (if c then t else e)
      Equations
      source
      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
      source
      @[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
      source
      @[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

      Inhabited #

      source
      instance instInhabitedProp :
      Inhabited Prop
      Equations
      source
      instance instInhabitedPNonScalar :
      Inhabited PNonScalar
      Equations
      source
      instance instInhabitedNonScalar :
      Inhabited NonScalar
      Equations
      source
      instance instInhabitedTrue :
      Inhabited True
      Equations

      Subsingleton #

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

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

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

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

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

      source
      instance instSubsingleton (p : Prop) :
      Subsingleton p
      source
      instance instSubsingletonEmpty :
      Subsingleton Empty
      source
      instance instSubsingletonPEmpty :
      Subsingleton PEmpty
      source
      instance instSubsingletonProd {α : Type u_1} {β : Type u_2} [Subsingleton α] [Subsingleton β] :
      Subsingleton (α × β)
      source
      instance instSubsingletonDecidable (p : Prop) :
      Subsingleton (Decidable p)
      source
      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₁)
      source
      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

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

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

      Equations
      source
      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
      source
      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
      Instances For
      source
      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.

      Instances For
      source
      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 #

      source
      theorem Subtype.exists_of_subtype {α : Type u} {p : α → Prop} :
      ∀ (a : { x : α // p x }), ∃ (x : α), p x
      source
      @[reducible, inline, deprecated Subtype.exists_of_subtype (since := "2025-04-04")]
      abbrev Subtype.existsOfSubtype {α : Type u_1} {p : α → Prop} :
      ∀ (a : { x : α // p x }), ∃ (x : α), p x
      Equations
      source
      theorem Subtype.eq {α : Type u} {p : α → Prop} {a1 a2 : { x : α // p x }} :
      a1.val = a2.val → a1 = a2
      source
      theorem Subtype.eta {α : Type u} {p : α → Prop} (a : { x : α // p x }) (h : p a.val) :
      ⟨a.val, h⟩ = a
      source
      instance Subtype.instBEq {α : Type u} {p : α → Prop} [BEq α] :
      BEq { x : α // p x }
      Equations
      source
      instance Subtype.instReflBEq {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] :
      ReflBEq { x : α // p x }
      source
      instance Subtype.instLawfulBEq {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] :
      LawfulBEq { x : α // p x }
      source
      instance Subtype.instDecidableEq {α : Type u} {p : α → Prop} [DecidableEq α] :
      DecidableEq { x : α // p x }
      Equations

      Sum #

      source
      @[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
      source
      @[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
      source
      instance Sum.nonemptyLeft {α : Type u} {β : Type v} [h : Nonempty α] :
      Nonempty (α ⊕ β)
      source
      instance Sum.nonemptyRight {α : Type u} {β : Type v} [h : Nonempty β] :
      Nonempty (α ⊕ β)
      source
      instance instDecidableEqSum {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] :
      DecidableEq (α✝ ⊕ β✝)
      Equations

      Product #

      source
      instance instNonemptyProd {α : Type u_1} {β : Type u_2} [h1 : Nonempty α] [h2 : Nonempty β] :
      Nonempty (α × β)
      source
      instance instNonemptyMProd {α β : Type u_1} [h1 : Nonempty α] [h2 : Nonempty β] :
      Nonempty (MProd α β)
      source
      instance instNonemptyPProd {α : Sort u_1} {β : Sort u_2} [h1 : Nonempty α] [h2 : Nonempty β] :
      Nonempty (α ×' β)
      source
      instance instInhabitedProd {α : Type u_1} {β : Type u_2} [Inhabited α] [Inhabited β] :
      Inhabited (α × β)
      Equations
      source
      instance instInhabitedMProd {α β : Type u_1} [Inhabited α] [Inhabited β] :
      Inhabited (MProd α β)
      Equations
      source
      instance instInhabitedPProd {α : Sort u_1} {β : Sort u_2} [Inhabited α] [Inhabited β] :
      Inhabited (α ×' β)
      Equations
      source
      instance instDecidableEqProd {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] :
      DecidableEq (α × β)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      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₂ }
      source
      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
      Instances For
      source
      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
      source
      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)
      source
      theorem Prod.eta {α : Type u_1} {β : Type u_2} (p : α × β) :
      (p.fst, p.snd) = p
      source
      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
      source
      @[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)
      source
      @[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
      source
      @[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 #

      source
      theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} :
      ∀ (a : (x : α) ×' p x), ∃ (x : α), p x
      source
      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 #

      source
      theorem PUnit.subsingleton (a b : PUnit) :
      a = b
      source
      theorem PUnit.eq_punit (a : PUnit) :
      a = unit
      source
      instance instSubsingletonPUnit :
      Subsingleton PUnit
      source
      instance instInhabitedPUnit :
      Inhabited PUnit
      Equations
      source
      instance instDecidableEqPUnit :
      DecidableEq PUnit
      Equations

      Setoid #

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

      Instances
      source
      instance instHasEquivOfSetoid {α : Sort u} [Setoid α] :
      HasEquiv α
      Equations
      source
      theorem Setoid.refl {α : Sort u} [Setoid α] (a : α) :
      a ≈ a

      A setoid's equivalence relation is reflexive.

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

      A setoid's equivalence relation is symmetric.

      source
      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 #

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

      source
      theorem Eq.propIntro {a b : Prop} (h₁ : a → b) (h₂ : b → a) :
      a = b
      source
      instance instDecidableEqOfIff {p q : Prop} [d : Decidable (p ↔ q)] :
      Decidable (p = q)
      Equations
      source
      theorem Nat.succ.inj {m n : Nat} :
      m.succ = n.succ → m = n
      source
      theorem Nat.succ.injEq (u v : Nat) :
      (u.succ = v.succ) = (u = v)
      source
      @[simp]
      theorem beq_iff_eq {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} :
      (a == b) = true ↔ a = b

      Prop lemmas #

      source
      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
      source
      @[reducible, inline]
      abbrev And.elim {a b : Prop} {α : Sort u_1} (f : a → b → α) (h : a ∧ b) :
      α

      Non-dependent eliminator for And.

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

      Non-dependent eliminator for Iff.

      Equations
      source
      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

      source
      theorem Not.intro {a : Prop} (h : a → False) :
      ¬a
      source
      theorem Not.imp {a b : Prop} (H2 : ¬b) (H1 : a → b) :
      ¬a
      source
      theorem not_congr {a b : Prop} (h : a ↔ b) :
      ¬a ↔ ¬b
      source
      theorem not_not_not {a : Prop} :
      ¬¬¬a ↔ ¬a
      source
      theorem iff_of_true {a b : Prop} (ha : a) (hb : b) :
      a ↔ b
      source
      theorem iff_of_false {a b : Prop} (ha : ¬a) (hb : ¬b) :
      a ↔ b
      source
      theorem iff_true_left {a b : Prop} (ha : a) :
      (a ↔ b) ↔ b
      source
      theorem iff_true_right {a b : Prop} (ha : a) :
      (b ↔ a) ↔ b
      source
      theorem iff_false_left {a b : Prop} (ha : ¬a) :
      (a ↔ b) ↔ ¬b
      source
      theorem iff_false_right {a b : Prop} (ha : ¬a) :
      (b ↔ a) ↔ ¬b
      source
      theorem of_iff_true {a : Prop} (h : a ↔ True) :
      a
      source
      theorem iff_true_intro {a : Prop} (h : a) :
      a ↔ True
      source
      theorem eq_iff_true_of_subsingleton {α : Sort u_1} [Subsingleton α] (x y : α) :
      x = y ↔ True
      source
      theorem not_of_iff_false {p : Prop} :
      (p ↔ False) → ¬p
      source
      theorem iff_false_intro {a : Prop} (h : ¬a) :
      a ↔ False
      source
      theorem not_iff_false_intro {a : Prop} (h : a) :
      ¬a ↔ False
      source
      theorem not_true :
      ¬True ↔ False
      source
      theorem not_false_iff :
      ¬False ↔ True
      source
      theorem Eq.to_iff {a b : Prop} :
      a = b → (a ↔ b)
      source
      theorem iff_of_eq {a b : Prop} :
      a = b → (a ↔ b)
      source
      theorem neq_of_not_iff {a b : Prop} :
      ¬(a ↔ b) → a ≠ b
      source
      theorem iff_iff_eq {a b : Prop} :
      (a ↔ b) ↔ a = b
      source
      @[simp]
      theorem eq_iff_iff {a b : Prop} :
      a = b ↔ (a ↔ b)
      source
      theorem eq_self_iff_true {α : Sort u_1} (a : α) :
      a = a ↔ True
      source
      theorem ne_self_iff_false {α : Sort u_1} (a : α) :
      a ≠ a ↔ False
      source
      theorem false_of_true_iff_false (h : True ↔ False) :
      False
      source
      theorem false_of_true_eq_false (h : True = False) :
      False
      source
      theorem true_eq_false_of_false :
      False → True = False
      source
      theorem iff_def {a b : Prop} :
      (a ↔ b) ↔ (a → b) ∧ (b → a)
      source
      theorem iff_def' {a b : Prop} :
      (a ↔ b) ↔ (b → a) ∧ (a → b)
      source
      theorem true_iff_false :
      (True ↔ False) ↔ False
      source
      theorem false_iff_true :
      (False ↔ True) ↔ False
      source
      @[simp]
      theorem iff_not_self {a : Prop} :
      ¬(a ↔ ¬a)
      source
      theorem heq_self_iff_true {α : Sort u_1} (a : α) :
      a ≍ a ↔ True

      implies #

      source
      theorem not_not_of_not_imp {a b : Prop} :
      ¬(a → b) → ¬¬a
      source
      theorem not_of_not_imp {b a : Prop} :
      ¬(a → b) → ¬b
      source
      @[simp]
      theorem imp_not_self {a : Prop} :
      a → ¬a ↔ ¬a
      source
      theorem imp_intro {α β : Prop} (h : α) :
      β → α
      source
      theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) :
      (a → b) → c → d
      source
      theorem imp_iff_right {b a : Prop} (ha : a) :
      a → b ↔ b
      source
      theorem imp_true_iff (α : Sort u) :
      (∀ (a : α), True) ↔ True
      source
      theorem false_imp_iff (a : Prop) :
      False → a ↔ True
      source
      theorem true_imp_iff {α : Prop} :
      True → α ↔ α
      source
      @[simp]
      theorem imp_self {a : Prop} :
      a → a ↔ True
      source
      @[simp]
      theorem imp_false {a : Prop} :
      a → False ↔ ¬a
      source
      theorem imp.swap {a b c : Prop} :
      a → b → c ↔ b → a → c
      source
      theorem imp_not_comm {a b : Prop} :
      a → ¬b ↔ b → ¬a
      source
      theorem imp_congr_left {a b c : Prop} (h : a ↔ b) :
      a → c ↔ b → c
      source
      theorem imp_congr_right {a b c : Prop} (h : a → (b ↔ c)) :
      a → b ↔ a → c
      source
      theorem imp_congr_ctx {a b c d : Prop} (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) :
      a → b ↔ c → d
      source
      theorem imp_congr {a b c d : Prop} (h₁ : a ↔ c) (h₂ : b ↔ d) :
      a → b ↔ c → d
      source
      theorem imp_iff_not {a b : Prop} (hb : ¬b) :
      a → b ↔ ¬a

      Quotients #

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

      source
      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
      source
      theorem Quot.indBeta {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (p : ∀ (a : α), motive (mk r a)) (a : α) :
      ⋯ = ⋯
      source
      @[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
      Instances For
      source
      theorem Quot.inductionOn {α : Sort u} {r : α → α → Prop} {motive : Quot r → Prop} (q : Quot r) (h : ∀ (a : α), motive (mk r a)) :
      motive q
      source
      theorem Quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) :
      ∃ (a : α), mk r a = q
      source
      @[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
      source
      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
      source
      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
      source
      @[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.recOn is a version of this recursor that takes the quotient parameter first.

      Equations
      source
      @[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.rec is a version of this recursor that takes the quotient parameter last.

      Equations
      source
      @[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
      source
      @[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 → 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
      source
      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
      Instances For
      source
      @[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
      source
      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
      source
      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.

      source
      @[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
      Instances For
      source
      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.

      source
      @[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
      Instances For
      source
      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.

      source
      theorem Quotient.exists_rep {α : Sort u} {s : Setoid α} (q : Quotient s) :
      ∃ (a : α), Quotient.mk s a = q
      source
      @[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.recOn is a version of this recursor that takes the quotient parameter first.

      Equations
      source
      @[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.rec is a version of this recursor that takes the quotient parameter last.

      Equations
      source
      @[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
      source
      @[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 → 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
      source
      @[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
      Instances For
      source
      @[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
      Instances For
      source
      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₂
      source
      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₂
      source
      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₃
      source
      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.

      source
      @[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
      source
      instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : (a b : α) → Decidable (a ≈ b)] :
      DecidableEq (Quotient s)
      Equations

      Function extensionality #

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

      source
      @[reducible, inline]
      abbrev Quot.pliftOn {β : Sort u_1} {α : Sort u} {r : α → α → Prop} (q : Quot r) (f : (a : α) → q = mk r a → β) (h : ∀ (a b : α) (h : q = mk r a) (h' : q = mk r b), r a b → f a h = f b h') :
      β

      Like Quot.liftOn q f h but allows f a to "know" that q = Quot.mk r a.

      Equations
      source
      @[reducible, inline]
      abbrev Quotient.pliftOn {β : Sort u_1} {α : Sort u} {s : Setoid α} (q : Quotient s) (f : (a : α) → q = Quotient.mk s a → β) (h : ∀ (a b : α) (h : q = Quotient.mk s a) (h' : q = Quotient.mk s b), a ≈ b → f a h = f b h') :
      β

      Like Quotient.liftOn q f h but allows f a to "know" that q = Quotient.mk s a.

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

      Squash #

      source
      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
      Instances For
      source
      def Squash.mk {α : Sort u} (x : α) :
      Squash α

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

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

      source
      @[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
      source
      instance instSubsingletonSquash {α : Sort u_1} :
      Subsingleton (Squash α)

      Kernel reduction hints #

      source
      axiom Lean.trustCompiler :
      True

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

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

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

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

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

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

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

      source
      @[simp]
      theorem ge_iff_le {α : Type u_1} [LE α] {x y : α} :
      x ≥ y ↔ y ≤ x
      source
      @[simp]
      theorem gt_iff_lt {α : Type u_1} [LT α] {x y : α} :
      x > y ↔ y < x
      source
      theorem le_of_eq_of_le {α : Type u_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) :
      a ≤ c
      source
      theorem le_of_le_of_eq {α : Type u_1} {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) :
      a ≤ c
      source
      theorem lt_of_eq_of_lt {α : Type u_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) :
      a < c
      source
      theorem lt_of_lt_of_eq {α : Type u_1} {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) :
      a < c
      source
      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).

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

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

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

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

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

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

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

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

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

                      Instances
                      source
                      instance Std.instCommutativeOr :
                      Commutative Or
                      source
                      instance Std.instCommutativeAnd :
                      Commutative And
                      source
                      instance Std.instCommutativeIff :
                      Commutative Iff
                      source
                      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.

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

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

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

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

                      Instances