Implementation of inductive types?

Stream: general

[Josh]

New to Lean and CoC/DTT in general (would it be better to post in #new members ? The description looked like it was for personal introductions.)

Anyway, I'm having some trouble understanding what the inductive type syntax actually does in terms of the most fundamental parts of CoC. Through some partial examples in the earlier parts of the Theorem Proving book, it made sense how the following could be used to axiomatically define what a boolean is:

constant my_bool: Type
namespace my_bool
constant true: my_bool
constant false: my_bool
end my_bool

Following up with #print axioms my_bool.true prints out the two axioms it is dependent on. In contrast, I've seen bool be declared as follows:

inductive bool : Type
| ff : bool
| tt : bool

This requires no axioms, which is what's confusing me at the moment. The Theorem Proving book has a chapter dedicated to this, but it seems focused on descriptions of what inductive types can do and how they can be used. Is there some way I can see what this syntax represents, or is it an extension of CoC which cannot be expressed as more verbose components?

[Kevin Buzzard]

.

[Kevin Buzzard]

Constants and axioms are discouraged because they might add inconsistencies into the system, eg there are none in mathlib. Making bool as an inductive type ensures that the system remains consistent.

[Kevin Buzzard]

The inductive construction does exactly what your constant approach does, but also adds a final constant bool.rec giving you a method to define a function on bool

[Kevin Buzzard]

However it is an acceptable approach because the constants that inductive adds are guaranteed not to add an inconsistency to the system

[Kevin Buzzard]

The thing you don't know with your constant approach is that to define a function on bool it suffices to give its values on true and false

[Jeremy Avigad]

Lean's foundation is a variant of what is known as "the calculus of inductive constructions." Inductive types are built in, so, in a sense, so they are just God-given (or Leo-given) constants and axioms. But, as Kevin says, it is better to stick to the foundation than to extend it on your own.

[Josh]

Thanks, it makes more sense now. I think I got a bit confused having read about the Calculus of Constructions and thinking it was the system Lean is built on, I'll look more into that.

[Jeremy Avigad]

There's a little more information here: https://arxiv.org/pdf/2009.09541.pdf. For a detailed description of Lean's type theory, see Mario's MS thesis: https://github.com/digama0/lean-type-theory/releases.