Zulip Chat Archive

Stream: new members

Topic: Inductive families and mutual induction


Andrea Berlingieri (Feb 01 2021 at 10:22):

Hi everybody. It's my first time posting, so I'll briefly introduce myself. My name is Andrea, I have a bachelor in Computer Science and I'm currently studying Logic at the ILLC in Amsterdam. I've been playing with other proof assistants in the past, but lately I've decided to start working with Lean (mostly thanks to Kevin Buzzard's presentations). It's nice to meet you all :)

I've been reading the book "Theorem proving in Lean" and I've been trying to wrap my head around inductive families (both the concept and the Lean implementation of it) ever since the weekend. In particular, I was a little puzzled about exercise 5 in chapter 7, which says: "Simulate the mutual inductive definition of even and odd described in Section 7.9 with an ordinary inductive type, using an index to encode the choice between them in the target type" (quick link to the chapter in question). I've come up with this solution and also proved a quick lemma with it:

Don't want to spoil it for others

Do you think this is a good "simulation" for the corresponding mutual induction? I've been trying to define the inductive type with all sorts of combinations of putting nat and bool before and after the semicolon, but they led to nothing interesting. The only way I see right now is to index the type on both nat and bool.

Mario Carneiro (Feb 01 2021 at 11:39):

That's the correct answer to the puzzle

Mario Carneiro (Feb 01 2021 at 11:40):

In fact, if you dig a little into how mutual inductive types are implemented in lean you will find out that this trick of adding an extra index storing which inductive type we're inhabiting is used in practice

Mario Carneiro (Feb 01 2021 at 11:44):

Here's a version that should make it clear how this generalizes:

Andrea Berlingieri (Feb 01 2021 at 12:37):

Thank you for your answer Mario :smile:


Last updated: Dec 20 2023 at 11:08 UTC