Inductive constructions

Stream: general

[Patrick Johnson]

Is it true that only a small number of inductive types is enough to implement all other inductive types? I was playing with this idea, and I managed to use only false, nat and psigma to re-implement all inductive types and props from core.lean. Is there a type that can't be implemented using those three types? If there's no such type, why do we have inductive constructions as a part of the kernel?

[Yaël Dillies]

Set theory would tell you that docs#pSet is enough to reimplement everything. :wink:

[Chris B]

The part of the kernel that handles inductives implements general rules for checking inductives and constructing recursors. If you're willing to trust them (and the theory) to handle false, nat, and psigma, it seems like you've already bought and paid for the underlying theory, so you might as well use it. The post-mortem on e.g. Lean 3's mutual inductives seems to suggest that the "implement complex constructions as machine-generated compositions of simpler elements" is not without tradeoffs. Inductive types are pretty central to the user experience in Lean; in terms of getting actionable feedback and communicating with users and stuff, I would assume a direct implementation is much better.

[Reid Barton]

How did you make eq?

[Patrick Johnson]

Set theory would tell you that docs#pSet is enough to reimplement everything.

Maybe I don't understand the Lean type theory enough, but as far as I can tell, you can't implement nat using only pSet without any other inductive types. Being able to inductively construct an infinite type (such as nat) using Lean inductive constructions basically implies the ZFC axiom of infinity.

Inductive types are pretty central to the user experience in Lean; in terms of getting actionable feedback and communicating with users and stuff, I would assume a direct implementation is much better.

Of course. But I'm not talking about the user interface at all. When you define an inductive type, all that you get back from the kernel are some constants and their types. The meta level code then proves other things, noconfusion, induction, dcases, and similar lemmas. My point is that we can only have a small number of builtin constants and define everything other in terms of that. User would not see any difference (except that a recursor of a type will actually have a concrete definition).

How did you make eq?

Here is my definition:

def eq {α} (x y : α) := ∀ (P : α → Prop), iff (P x) (P y)

Here are other definitions (there may be some mistake, I haven't formally proved they are equivalent to the actual definitions from core.lean):

Definitions

import tactic

noncomputable theory
open_locale classical

namespace test

def true := false → false
def true.intro := λ (x : false), x

def not (p : Prop) := p → false
local prefix `¬`:40 := not
lemma not_not (p : Prop) (h : ¬¬p) : p :=
dite p id (λ h₁, (h h₁).elim)

def or (p q : Prop) := ¬p → q
def or.inl {p q : Prop} (h : p) : or p q := λ h₁, (h₁ h).elim
def or.inr {p q : Prop} (h : q) : or p q := λ h₁, h

def and (p q : Prop) := ¬(p → ¬q)
def and.intro {p q : Prop} (h₁ : p) (h₂ : q) : and p q := λ h, h h₁ h₂
def and.left {p q : Prop} (h : and p q) : p :=
dite p id (λ h₁, (h (λ h₂ h₃, h₁ h₂)).elim)
def and.right {p q : Prop} (h : and p q) : q :=
dite q id (λ h₁, (h (λ h₂ h₃, h₁ h₃)).elim)

def iff (p q : Prop) := and (p → q) (q → p)
def iff.intro {p q : Prop} (h₁ : p → q) (h₂ : q → p) : iff p q :=
and.intro h₁ h₂
def iff.mp {p q : Prop} (h : iff p q) : p → q := h.left
def iff.mpr {p q : Prop} (h : iff p q) : q → p := h.right

def eq {α} (x y : α) := ∀ (P : α → Prop), iff (P x) (P y)
local infix ` = `:50 := eq
def eq.refl {α} (x : α) : x = x := λ P, and.intro id id
def eq.subst {α} {x y : α} {P : α → Prop} (h₁ : x = y) (h₂ : P x) : P y :=
(h₁ P).mp h₂

def {u} unit : Type u := Sort u
def punit : Prop := true

def bool := Prop
def tt := true
def ff := false

def subtype {α} (β : α → Prop) := psigma β
def subtype.val {α} {β : α → Prop} (x : subtype β) := x.fst
def subtype.property {α} {β : α → Prop} (x : subtype β) := x.snd

def prod (α β : Type*) := psigma (λ (x : α), β)
def prod.fst {α β : Type*} (x : prod α β) : α := x.fst
def prod.snd {α β : Type*} (x : prod α β) : β := x.snd

def option (α : Type*) := Σ' (p : Prop), p → α
def option.none {α : Type*} : option α := ⟨false, false.elim⟩
def option.some {α : Type*} (x : α) : option α := ⟨true, λ h, x⟩
def option.is_some {α : Type*} (x : option α) : Prop := x.fst

def le : ℕ → ℕ → Prop
| 0 y := true
| (nat.succ x) 0 := false
| (nat.succ x) (nat.succ y) := le x y

def lt (x y : ℕ) : Prop := and (le x y) ¬(x = y)

def list (α : Type*) := Σ' (f : ℕ → option α) (n : ℕ),
∀ (k : ℕ), iff (f k).is_some (lt k n)
def list.length {α : Type*} (xs : list α) := xs.snd.fst
def list.nil {α : Type*} : list α := ⟨λ i, option.none, 0, sorry⟩
def list.cons {α : Type*} (x : α) (xs : list α) : list α :=
⟨λ i, ite (i = xs.length) (option.some x) (xs .fst i),
xs.length.succ, sorry⟩

end test

[Mario Carneiro]

This is covered in #leantt, chapter 5.

[Mario Carneiro]

Specifically, you need 8 inductive types:

• false
• psigma
• psum
• ulift
• nonempty
• W_type (docs#W_type)
• eq
• acc (docs#acc)

[Mario Carneiro]

The main one is W_type, but then you need all the others to actually put stuff together into the form needed by W_type

[Mario Carneiro]

Regarding your constructions:

• The true construction works as a type that is bijective with true, but it doesn't have all the right defeqs. The W-type reduction includes all the same defeqs as a genuine inductive type.
• Same thing for and and or, and in particular those constructions are not intuitionistic, they require LEM to prove the recursor and such
• Your definition of eq is not strong enough: in lean you can prove eq.subst when P : A -> Sort u, not just Prop. I believe your construction is equivalent to lean's eq, but you need to use lean's eq to prove the equivalence...
• The unit construction is wrong, Sort u is not a singleton type
• punit isn't actually universe polymorphic like lean's
• The bool model will make bool.cases noncomputable
• The option model makes option.cases noncomputable

[Trebor Huang]

I think it's worth reading how all the (non-dependent) inductive types can be encoded in an impredicative type theory like the Calculus of Constructions -- It doesn't even have any built-in inductive types!

However, with Lean, you have universe level problems, and also defeqs and computability will break. eq doesn't work as Carneiro points out, and I think (handwavingly) that this is connected to the fact that to make a category finitely complete, you need a terminal object, binary products and equalizers.

[Mario Carneiro]

You should also check out Church encodings, which are a general mechanism for encoding inductive types in lambda calculus or System F (i.e. a haskell-like type theory). Unfortunately it doesn't work properly in the presence of a universe hierarchy, which is why CIC builds it in instead

[Chris B]

Patrick Johnson said:

Of course. But I'm not talking about the user interface at all. When you define an inductive type, all that you get back from the kernel are some constants and their types. The meta level code then proves other things, noconfusion, induction, dcases, and similar lemmas. My point is that we can only have a small number of builtin constants and define everything other in terms of that. User would not see any difference (except that a recursor of a type will actually have a concrete definition).

Recursors are already given a concrete definition by the kernel, they get lambda/value-level term(s) in the form of a reduction rule.

The point of the lean 3 mutual inductives example was that the introduction of an intermediate mapping between what's going on in the kernel and what the user sees has a high chance of bleeding through into the UX. Giving users feedback or letting them look at lower level information about their inductive now requires you to go back and forth through this translation layer in a manner that's completely transparent.

If the idea was that users would write their inductives explicitly in terms of the primitives you (or Mario) mentioned then that wouldn't be the case, but you would have a different proof assistant at that point.

[Eric Wieser]

Note that by using dite in your definitions above, you're using another inductive type, docs#decidable