Primitive built-ins

Stream: new members

[Lauri Oksanen]

Can I find somewhere a list of primitives that are not constructed using inductive types or other means? I would like to have this on an informal level. Something like

• Universes (Sort u)
• Function types (→)
• Lambda abstraction (λ x ↦ ...)
• Inductive type mechanism (inductive)

[Eric Wieser]

Does the list of constructors for docs#Lean.Expr help? That covers your first three items, and I think after that only inductive types and Quot are the remaining primitives

[Niels Voss]

In that list, note that .mvar and .fvar only exists for terms that are currently being constructed, once a proof is finished it won't contain any .mvar or .fvar expressions. Also, .mdata, .lit, and .proj aren't really that important.

So, if you just care about what Lean's expressions are made of, all that's left is

• Universes (Sort u)
• Dependent function types, aka forall types, aka pi types. Function types (→) are a special case
• Function application (i.e. if f is a function and x is a term then f x is a term)
• Lambda abstractions
• References to the variables bound by lambda abstractions (these use de Bruijn indices)
• References to constants, i.e. terms previously defined with def, theorem, inductive, structure, axiom, etc.
• Let expressions (i.e. let x := a; b)

[Lauri Oksanen]

Thanks a lot!

A slightly tangential follow-up question: I am thinking theorem as a special case of def, and structure as a special case of inductive. Is there any reason not to?

[Louis Cabarion]

Structures are a special case of inductive types, distinguished by having exactly one constructor.

[Robin Arnez]

theorem is basically a def and structure and inductive, yes. But you could still argue that non-recursive inductive types with exactly one are actually special cased in that they have the eta rule:

inductive Example where
  | mk (a : Nat) (b : Int)

example (x : Example) : ⟨x.1, x.2⟩ = x := rfl

Because of this the recursor can also be reduced:

Example.rec mk t ≡ Example.rec mk ⟨t.1, t.2⟩ ≡ mk t.1 t.2

In this sense you can also think of projections to be the primitive instead of the recursor for "structure" inductives.

[Robin Arnez]

So these are all builtins:

• Universes (Sort u : Sort (u + 1))
• Pi types ((a : α) → β(a) : Sort (imax u v) for α : Sort u and β(a) : Sort v)
• Function application (f x : β(a) for f : (a : α) → β(a) and x : α)
• Lambda abstractions (fun x : α => f(x) : (a : α) → β(a) for f(x) : β(x))
• Let expressions (let x : α := a; b(x) : β for b(a) : β) (optional because equivalent to substitution)
• References to bound variables from lets and lambda abstractions and pi types
• Inductive types (e.g. Nat : Sort (0 + 1))
• Constructors of inductive types (e.g. Nat.zero : Nat / Nat.succ : Nat → Nat)
• Projections for non-recursive inductive types with one constructor (e.g. x.1 : α for x : Prod α β)
• Recursors of other inductive types (e.g. Nat.rec.{u} : {motive : Nat → Sort u} → motive Nat.zero → ((n : Nat) → motive n → motive (Nat.succ n)) → (n : Nat) → motive n)
• Definitions (e.g. Nat.add : Nat → Nat → Nat) (optional because equivalent to substitution)
• Quotient primitives (Quot.{u} : {α : Sort u} → (α → α → Sort 0) → Sort u, Quot.mk.{u} : {α : Sort u} → (r : α → α → Sort 0) → α → Quot r, Quot.ind.{u} : {α : Sort u} → {r : α → α → Sort 0} → {β : Quot r → Sort 0} → ((a : α) → β (Quot.mk r a)) → (q : Quot r) → β q, Quot.lift.{u, v} : {α : Sort u} → {r : α → α → Sort 0} → {β : Sort v} → (f : α → β) → ((a : α) → (b : α) → r a b → Eq (f a) (f b)) → Quot r → β)
• Axioms (e.g. propext : {p : Sort 0} → {q : Sort 0} → Iff p q → Eq p q)

And then Prop ≡ Sort 0, Type u ≡ Sort (u + 1), "theorem ≡ def", "structure ≡ inductive" and so on

[Lauri Oksanen]

Thanks a lot! This is very helpful. I would have two questions.

1. When you say "optional because equivalent to substitution" what do you mean more precisely?
2. Dependent Type Theory section of Theorem Proving in Lean 4 mentions dependent function types and dependent Cartesian product types (or sigma types). What is the relation between these and Pi types?

[Aaron Liu]

Lauri Oksanen said:

2. Dependent Type Theory section of Theorem Proving in Lean 4 mentions dependent function types and dependent Cartesian product types (or sigma types). What is the relation between these and Pi types?

In Lean, Pi types are a built-in primitive, and Sigma types (docs#Sigma) are an inductive. "dependent function type" is another name for Pi type.