Expressiveness of inductive types

Stream: Type theory

[Sky Wilshaw]

Lean has a very expressive type theory using inductive types. Suppose that Lean instead didn't have inductive types, but just supported algebraic types, with the sole addition of subtype (using Lean 3 names for things out of familiarity). Does this strictly weaken Lean's expressive power, or is there a way to simulate inductive types just using algebraic types and a subtype operation?

My instinct is that there are certain things that would become impossible to address - quiver.path is one that comes to mind. With this example in mind, I wonder if algebraic types + subtype + inductive Props is equivalent to full inductive types? One could inductively define a proposition on lists saying whether it represents a path between two objects in a quiver, and use a subtype.

[Eric Wieser]

I think the claim I remember hearing before is that you only need docs#W_type and maybe docs#unit/docs#empty to build all other inductive types

[Mario Carneiro]

I have a chapter in #leantt dedicated to the reduction to W types. The short answer is that yes you can reduce all inductive types to 8 specific inductive types: Sum, Sigma, False, (basic algebraic types), ULift (for inductives in a higher universe), W (general inductives), Nonempty (for making small-eliminating props), Acc (large eliminating props), Eq (K-like inductives)

[Sky Wilshaw]

Thank you both, that's perfect!

[Reid Barton]

Is that without choice/LEM?

[Reid Barton]

With LEM (but not choice) you can also construct W types (at least the non-indexed ones, but probably indexed ones are okay too) from the other things you listed plus Nat, (I am assuming subtypes are included under Sigma), and Pi types

[Reid Barton]

for instance Option A = Sum Unit A

[Reid Barton]

then List A = functions f : Nat -> Option A such that if f n = None, then also f (n+1) = None

[Reid Barton]

this also works for other W types, including infinitary ones, though it's considerably less obvious

[Chris Hughes]

Where do you need LEM?

[Reid Barton]

I guess maybe this is somewhat orthogonal to the original question.

[Reid Barton]

Indeed I don't need it for List but I think I will need it in the infinitary case.

[Reid Barton]

Or I could be misremembering at what point it is needed

[Chris Hughes]

In most maths you don't use inductives other than list or nat anyway. I actually checked which inductive Types whose induction principle had an induction hypothesis in the liquid tensor experiment and it was list, nat and something about colimits of abelian groups. I can't think of a single infinitely branching inductive in mathlib.

[Johan Commelin]

Lol, nice little fact. TIL!

[Reid Barton]

OK, actually you don't need LEM for what I said either.

[Reid Barton]

How about docs#measurable_space.generate_measurable

[Reid Barton]

Of course, since it is an inductive predicate it could also have been defined another way.

[Reid Barton]

I think Sebastien had a more serious example somewhere in the Gromov-Hausdorff distance stuff

[Mario Carneiro]

Reid Barton said:

Is that without choice/LEM?

Yes, the reduction does not use any axioms, although I think it does depend on proof irrelevance, at least the way I stated it

[Sky Wilshaw]

Reid Barton said:

How about docs#measurable_space.generate_measurable

I can see how this might be implemented with W types and a predicate, but I don't see how you could express this using Pi types. I'm also not quite sure what you mean about LEM/choice - where would that need to be applied?

[Sky Wilshaw]

It's the potentially-unbounded recursion that I can't see how to encode without doing something weird like assigning a well-founded dependence relation on the set of all sets you use to construct your given measurable set.

[Mario Carneiro]

Here's a worked example for GenerateMeasurable, which reduces the type to primitives in four stages:

import Mathlib.MeasureTheory.MeasurableSpaceDef
import Mathlib.Data.W.Basic

namespace MeasurableSpace

-- Original:
-- inductive GenerateMeasurable (s : Set (Set α)) : Set α → Prop
--   | protected basic : ∀ u ∈ s, GenerateMeasurable s u
--   | protected empty : GenerateMeasurable s ∅
--   | protected compl : ∀ t, GenerateMeasurable s t → GenerateMeasurable s (tᶜ)
--   | protected unionᵢ : ∀ f : ℕ → Set α, (∀ n, GenerateMeasurable s (f n)) →
--       GenerateMeasurable s (⋃ i, f i)

-- Step 1: apply propositional truncation to an inductive in Type
inductive GenerateMeasurable1 {α : Type u} (s : Set (Set α)) : Set α → Type u
  | protected basic : ∀ u ∈ s, GenerateMeasurable1 s u
  | protected empty : GenerateMeasurable1 s ∅
  | protected compl : ∀ t, GenerateMeasurable1 s t → GenerateMeasurable1 s (tᶜ)
  | protected unionᵢ : ∀ f : ℕ → Set α, (∀ n, GenerateMeasurable1 s (f n)) →
      GenerateMeasurable1 s (⋃ i, f i)

def GenerateMeasurable' (s : Set (Set α)) (u : Set α) : Prop :=
  Nonempty (GenerateMeasurable1 s u)

-- Step 2 (translate inductive families by defining a skeleton type + predicate)
inductive GenerateMeasurable2 {α : Type u} (s : Set (Set α)) : Type u
  | protected basic : ∀ u ∈ s, GenerateMeasurable2 s
  | protected empty : GenerateMeasurable2 s
  | protected compl : ∀ _t : Set α, GenerateMeasurable2 s → GenerateMeasurable2 s
  | protected unionᵢ : ∀ _f : ℕ → Set α, (∀ _n : ℕ, GenerateMeasurable2 s) →
      GenerateMeasurable2 s

def GenerateMeasurable2.good {α : Type u} {s : Set (Set α)} :
    GenerateMeasurable2 s → Set α → Prop
  | .basic u _h, a => a = u
  | .empty, a => a = ∅
  | .compl t ih, a => a = (tᶜ) ∧ ih.good t
  | .unionᵢ f ih, a => a = (⋃ i, f i) ∧ ∀ n, (ih n).good (f n)

def GenerateMeasurable1' {α : Type u} (s : Set (Set α)) : Set α → Type u :=
  fun a => { x : GenerateMeasurable2 s // x.good a }

-- Step 3 (translate simple inductive types to W types)
inductive GenerateMeasurable3Dom {α : Type u} (s : Set (Set α)) : Type u
  | protected basic : ∀ u ∈ s, GenerateMeasurable3Dom s
  | protected empty : GenerateMeasurable3Dom s
  | protected compl : ∀ t : Set α, GenerateMeasurable3Dom s
  | protected unionᵢ : ∀ f : ℕ → Set α, GenerateMeasurable3Dom s

def GenerateMeasurable3Dom.branch : GenerateMeasurable3Dom s → Type
  | .basic _ _ => Empty
  | .empty => Empty
  | .compl _ => Unit
  | .unionᵢ _ => Nat

def GenerateMeasurable2' {α : Type u} (s : Set (Set α)) : Type u :=
  @WType (GenerateMeasurable3Dom s) GenerateMeasurable3Dom.branch

-- Step 4 (translate nonrecursive inductive types to primitives)
def GenerateMeasurable3Dom' {α : Type u} (s : Set (Set α)) : Type u :=
  (Σ' u, u ∈ s) ⊕
  Unit ⊕
  Set α ⊕
  (ℕ → Set α)

[Mario Carneiro]

And here's an end to end proof of equivalence. I take back what I said, the proof does require choice to prove that the inductive in Prop is equivalent to the truncation of an inductive in Type. I think you would need a PropW type to avoid this dependency.

import Mathlib.MeasureTheory.MeasurableSpaceDef
import Mathlib.Data.W.Basic

namespace MeasurableSpace

inductive GenerateMeasurable' (s : Set (Set α)) : Set α → Prop
  | protected basic : ∀ u ∈ s, GenerateMeasurable' s u
  | protected empty : GenerateMeasurable' s ∅
  | protected compl : ∀ t, GenerateMeasurable' s t → GenerateMeasurable' s t.compl
  | protected unionᵢ : ∀ f : ℕ → Set α, (∀ n, GenerateMeasurable' s (f n)) →
      GenerateMeasurable' s (⋃ i, f i)

def Dom {α : Type u} (s : Set (Set α)) : Type u :=
  (Σ' u, u ∈ s) ⊕ Unit ⊕ Set α ⊕ (ℕ → Set α)

def Dom.branch {α : Type u} (s : Set (Set α)) : Dom s → Type :=
  fun
  | .inl _ | .inr (.inl _) => Empty
  | .inr (.inr (.inl _)) => Unit
  | .inr (.inr (.inr _)) => Nat

def Base {α : Type u} (s : Set (Set α)) : Type u := WType (Dom.branch s)

def Base.good {α : Type u} (s : Set (Set α)) : Base s → Set α → Prop
  | ⟨.inl ⟨u, _⟩, _⟩, a => a = u
  | ⟨.inr (.inl _), _⟩, a => a = ∅
  | ⟨.inr (.inr (.inl t)), ih⟩, a => a = t.compl ∧ good s (ih ()) t
  | ⟨.inr (.inr (.inr f)), ih⟩, a => a = (⋃ i, f i) ∧ ∀ n, good s (ih n) (f n)

def Main {α : Type u} (s : Set (Set α)) (a : Set α) : Prop := ∃ b : Base s, b.good s a

theorem ltr : ∀ a (b : Base s), b.good s a → GenerateMeasurable' s a
  | _, ⟨.inl ⟨u, h⟩, _⟩, rfl => .basic u h
  | _, ⟨.inr (.inl _), _⟩, rfl => .empty
  | _, ⟨.inr (.inr (.inl _)), _⟩, ⟨rfl, h⟩ => .compl _ (ltr _ _ h)
  | _, ⟨.inr (.inr (.inr _)), _⟩, ⟨rfl, h⟩ => .unionᵢ _ fun n => ltr _ _ (h n)

theorem rtl : ∀ a, GenerateMeasurable' s a → Main s a
  | _, .basic u h => ⟨⟨.inl ⟨u, h⟩, fun.⟩, rfl⟩
  | _, .empty => ⟨⟨.inr (.inl ()), fun.⟩, rfl⟩
  | _, .compl t ih =>
    ⟨⟨.inr (.inr (.inl t)), fun _ => (rtl _ ih).choose⟩, rfl, (rtl _ ih).choose_spec⟩
  | _, .unionᵢ f ih =>
    ⟨⟨.inr (.inr (.inr f)), fun n => (rtl _ (ih n)).choose⟩,
      rfl, fun n => (rtl _ (ih n)).choose_spec⟩

theorem is_equiv : Main s a ↔ GenerateMeasurable' s a :=
  ⟨fun ⟨b, h⟩ => ltr _ b h, rtl _⟩

[Mario Carneiro]

Here's a version of the reduction to the indexed version of W (which I wanted to avoid in the original paper), which does not need choice for the equivalence proof.

import Mathlib.MeasureTheory.MeasurableSpaceDef
import Mathlib.Data.W.Basic

namespace MeasurableSpace

inductive GenerateMeasurable' (s : Set (Set α)) : Set α → Prop
  | protected basic : ∀ u ∈ s, GenerateMeasurable' s u
  | protected empty : GenerateMeasurable' s ∅
  | protected compl : ∀ t, GenerateMeasurable' s t → GenerateMeasurable' s t.compl
  | protected unionᵢ : ∀ f : ℕ → Set α, (∀ n, GenerateMeasurable' s (f n)) →
      GenerateMeasurable' s (⋃ i, f i)

inductive PropW (α : Type _) (β : α → Type _) (p : ∀ a, β a → γ) (q : α → γ) : γ → Prop
  | mk (a : α) (f : ∀ b, PropW α β p q (p a b)) : PropW α β p q (q a)

def Dom {α : Type u} (s : Set (Set α)) : Type u :=
  (Σ' u, u ∈ s) ⊕ Unit ⊕ Set α ⊕ (ℕ → Set α)

def Dom.branch {s : Set (Set α)} : Dom s → Type :=
  fun
  | .inl _ | .inr (.inl _) => Empty
  | .inr (.inr (.inl _)) => Unit
  | .inr (.inr (.inr _)) => Nat

def Dom.target {s : Set (Set α)} : Dom s → Set α
  | .inl ⟨u, _⟩ => u
  | .inr (.inl _) => ∅
  | .inr (.inr (.inl t)) => t.compl
  | .inr (.inr (.inr f)) => (⋃ i, f i)

def Dom.dep {s : Set (Set α)} : ∀ a : Dom s, a.branch → Set α
  | .inr (.inr (.inl t)), _ => t
  | .inr (.inr (.inr f)), n => f n

def Main {α : Type u} (s : Set (Set α)) : Set α → Prop :=
  PropW (Dom s) Dom.branch Dom.dep Dom.target

theorem is_equiv : Main s a ↔ GenerateMeasurable' s a := by
  refine ⟨fun h => ?_, rtl _⟩
  · induction h with | _ h _ ih =>
    exact match h, ih with
    | .inl ⟨u, h⟩, _ => .basic u h
    | .inr (.inl _), _ => .empty
    | .inr (.inr (.inl _)), ih => .compl _ (ih ())
    | .inr (.inr (.inr _)), ih => .unionᵢ _ fun n => ih n
where
  rtl : ∀ a, GenerateMeasurable' s a → Main s a
  | _, .basic u h => ⟨(.inl ⟨u, h⟩ : Dom s), fun.⟩
  | _, .empty => ⟨(.inr (.inl ()) : Dom s), fun.⟩
  | _, .compl t ih => ⟨(.inr (.inr (.inl t)) : Dom s), fun _ => rtl _ ih⟩
  | _, .unionᵢ f ih => ⟨(.inr (.inr (.inr f)) : Dom s), fun n => rtl _ (ih n)⟩

#print axioms is_equiv
-- 'MeasurableSpace.is_equiv' does not depend on any axioms

[Mario Carneiro]

This issue only arises for small-eliminating Prop families, so there is some hope of an alternative implementation using impredicativity, by simply defining it as the intersection of all relations closed under the constructors. (This is the standard mathematical definition for such predicates.)

[Mario Carneiro]

Here's a proof that the PropW inductive type above can be defined without inductive types at all:

variable (α : Type _) (β : α → Type _) (p : ∀ a, β a → γ) (q : α → γ)
inductive PropW : γ → Prop
  | mk (a : α) (f : ∀ b, PropW (p a b)) : PropW (q a)

def PropW' (i : γ) : Prop :=
  ∀ R : γ → Prop, (∀ a, (∀ b, R (p a b)) → R (q a)) → R i

theorem is_equiv : PropW α β p q i ↔ PropW' α β p q i := by
  refine ⟨fun h R ih => ?_, fun h => h _ .mk⟩
  induction h with | _ a _ IH => exact ih _ IH

#print axioms is_equiv -- 'is_equiv' does not depend on any axioms

[Sky Wilshaw]

Thanks for this detailed example - I'll work through it later!