Type def in kernel

Stream: new members

[Patrick Johnson]

How does Lean translate type definitions to the logic kernel? According to the Reference Manual, the kernel is very minimal and recognizes only Π, λ, Sort u and let in. It also says (in section 4.4, page 26, last paragraph): "The type former, constructors, and eliminator are all part of Lean's axiomatic foundation, which is to say, they are part of the trusted kernel." How exactly is that achieved?

I see two possible explanations. The first one is that kernel defines new axioms for each type (axioms regarding no_confusion and rec) and then Lean defines the rest of the type lemmas in terms of those two. The second explanation is that the kernel is aware of some primordial types (such as ℕ and subtype) and defines any other type in terms of those two (uses Π to increase the cardinality by incrementally constructing powersets, and then uses subtype to fine-tune the cardinality to match the actual type).

Which of those two is closer to the actual implementation?

[Kevin Buzzard]

Lean defines new axioms for each type -- but not no_confusion! This is proved using rec -- try e.g. #print nat.no_confusion to see a sample proof. However #print nat.rec shows that there is no proof -- it's just marked as eliminator.

[Kevin Buzzard]

inductive foo
| bar

#print foo.rec -- new constant in the theory, no definition

[Kevin Buzzard]

I think that the complete list of constants added in the above example is foo, foo.bar and foo.rec. However #print prefix foo shows all the other things which magically appear, and you can check to see that all the other things have definitions by #printing them separately.

[Mario Carneiro]

Patrick Johnson said:

How does Lean translate type definitions to the logic kernel? According to the Reference Manual, the kernel is very minimal and recognizes only Π, λ, Sort u and let in.

An important (class of) things missing from your list are axiomatic constants. These are denoted by names like nat and each one is declared with a particular type and "nothing more", that is, nat : Type is true, nat : Type 1 is false, and reducing nat yields nat again. Inductive types, quotient types, and definitions are also known to the kernel, and add some reduction rules in addition to adding constants with known types.