Inductive Types / Families: Why not always use indices?

Stream: new members

[Ashish Rao]

Hello! I'm a beginner learning Lean through Theorem Proving in Lean 4, and am currently on chapter 7 (inductive types). From what I understand, the constructors of inductive types are subject to 2 constraints:

1. If the inductive type is I (a1 : α1) (a2 : α2) ... (an : αn), each constructor must return a value of type I (a1 : α1) (a2 : α2) ... (an : αn).
2. If the inductive type is I (a1 : α1) (a2 : α2) ... (an : αn), where a1, ..., an are parameters of the type, then constructors of I can only depend on other values of type I so long as those types also have parameters a1, ..., an. E.g. a constructor for I (a1 : α1) (a2 : α2) ... (an : αn) cannot depend on a value of type I (a1 : α1) (b : α2) ... (an : αn) for b ≠ a2.

We can get around some of these restrictions by using inductive families instead, and conditioning the type on indices instead of parameters.

My question is: why not just always use indices? Is there any benefit to defining inductive types with parameters instead of always defining inductive families with indices?

Consider the example below, which defines List as an inductive type, and BadList as an inductive family. In both cases, it is easy to prove a proposition that all elements in a List Nat / BadList Nat are >= 0. Since it seems equally easy to work with inductive types and inductive families, why not just always use inductive families?

namespace Hidden

inductive BadList : (α : Type u) → Type u where
| nil : BadList α
| cons (h : α) (t : BadList α) : BadList α

def all_badlist_nat_geq_0_prop (l : (BadList Nat)) : Prop :=
  match l with
  | .nil => True
  | .cons head rest => (head ≥ 0) ∧ (all_badlist_nat_geq_0_prop rest)

def all_badlist_nat_geq_0_pf (l : BadList Nat) : all_badlist_nat_geq_0_prop l :=
  match l with
  | .nil => True.intro
  | .cons head rest => ⟨Nat.zero_le head, all_badlist_nat_geq_0_pf rest⟩


inductive List (α : Type u) where
| nil : List α
| cons (h : α) (t : List α) : List α

def all_list_nat_geq_0_prop (l : List Nat) : Prop :=
  match l with
  | .nil => True
  | .cons head rest => (head ≥ 0) ∧ (all_list_nat_geq_0_prop rest)

def all_list_nat_geq_0_pf (l : List Nat) : all_list_nat_geq_0_prop l :=
  match l with
  | .nil => True.intro
  | .cons head rest => ⟨Nat.zero_le head, all_list_nat_geq_0_pf rest⟩

end Hidden

Thanks in advance!

[Niels Voss]

I can't provide a full answer, but please be aware that by default, Lean converts indices to parameters when possible. When you disable this with set_option inductive.autoPromoteIndices false, your definition of BadList no longer works because of a universe issue.

[David Thrane Christiansen]

Indices can be freely instantiated in constructors' types, which means that they need to be restricted a bit in order to not cause issues for the logic. In particular, parameters have to be at most the universe of the inductive type, while indices must be strictly smaller. Manual section with examples.

This is why the error that @Niels Voss pointed out occurs.

[Ashish Rao]

Makes sense, thanks to you both!