Zulip Chat Archive

Stream: general

Topic: Mutual def


Markus Himmel (Sep 23 2020 at 06:39):

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 (Sep 23 2020 at 06:46):

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

Markus Himmel (Sep 23 2020 at 06:55):

That worked like a charm. Thanks!

Kevin Buzzard (Sep 23 2020 at 07:06):

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 (Sep 23 2020 at 07:12):

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

Sebastien Gouezel (Sep 23 2020 at 07:14):

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 (Sep 23 2020 at 07:22):

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 (Sep 23 2020 at 07:25):

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


Last updated: Dec 20 2023 at 11:08 UTC