Mutual def

Stream: general

[Markus Himmel]

On a high level, the proof that in a category with enough projectives every object admits a projective resolution works as follows: We start with a map f₀ : α₁ → α₂ and we have functions that look like the following (except that we're in category-land, but that shouldn't matter here):

def next_type {α β : Type u} (f : α → β) : Type u := sorry
def next_fun {α β : Type u} (f : α → β) : next_type f → α := sorry

We now construct an infinite sequence of maps ... → next_type (next_fun (next_fun f₀)) → next_type (next_fun f₀) → next_type f₀ → α₁, where the arrows are next_fun applied to f₀ the correct number of times. I would like to have two functions T : ℕ → Type u and f : Π (n : ℕ), T (n + 1) → T n giving the ith type and function in that sequence, respectively. To me, this sounds like mutual induction. I tried the following:

mutual def T, f
with T : ℕ → Type u
| 0 := α₁
| 1 := next_type f₀
| (n + 2) := next_type (f n)
with f : Π (n : ℕ), T (n + 1) → T n
| 0 := next_fun f₀
| (n + 1) := next_fun (f n)

but it produces multiple errors: "ill-formed match/equations expression" as well as "equation type mismatch, term next_fun f₀ has type next_type f₀ → α₁ : Type ? but is expected to have type T (0 + 1) → T 0 : Type u". Full MWE:

universe u

def α₁ : Type u := sorry
def α₂ : Type u := sorry
def f₀ : α₁ → α₂ := sorry

def next_type {α β : Type u} (f : α → β) : Type u := sorry
def next_fun {α β : Type u} (f : α → β) : next_type f → α := sorry

mutual def T, f
with T : ℕ → Type u
| 0 := α₁
| 1 := next_type f₀
| (n + 2) := next_type (f n)
with f : Π (n : ℕ), T (n + 1) → T n
| 0 := next_fun f₀
| (n + 1) := next_fun (f n)

I'm not sure whether I just got the syntax wrong or whether mutual induction is not the right tool for this kind of thing. @Kevin Buzzard, I recall you saying that you never need mutual induction when formalizing math. What would you use here?

[Sebastien Gouezel]

You can use a structure putting together all the things you need at step n, and then define inductively the full structures.

[Markus Himmel]

That worked like a charm. Thanks!

[Kevin Buzzard]

Nice! My observation was that in the perfectoid project we just used a bunch of structures and this had led me to believe that inductive types with more than one constructor were not particularly useful to me (other than the basic ones like nat and list and option). However I don't know to what extent this remains true across mathematics. How many inductive types which aren't structures appear in the foundations of manifolds in Lean, for example?

Sebastien's Lean Together 2020 talk shows a very nice example where an inductive type is used to prove a theorem of Bonk and Schramm

[Patrick Massot]

We have a couple of things like docs#topological_space.generate_open

[Sebastien Gouezel]

Kevin Buzzard said:

How many inductive types which aren't structures appear in the foundations of manifolds in Lean, for example?

Exactly 0, of course.

[Yury G. Kudryashov]

Patrick Massot said:

We have a couple of things like docs#topological_space.generate_open

I prefer the src#submonoid.closure approach (e.g., because you don't have to repeat the definition of submonoid/topological_space/... once more) but of course this is a matter of taste.

[Kevin Buzzard]

So these two approaches give the same answer but please don't assume that my observation (that inductive types which aren't structures can often be avoided in my work) means that it's always a good idea to avoid them