Inductive families and mutual induction

Stream: new members

[Andrea Berlingieri]

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

universe u
open nat

inductive odd_even : nat → bool → Prop
| zero_even: odd_even 0 true
| odd_even {n:nat} {b:bool} (o:odd_even n b): odd_even (succ n) (not b)

lemma odd_or_even (n : nat) : (odd_even n true) ∨ (odd_even n false) :=
begin
  induction n,
  case zero: {left, exact odd_even.zero_even},
  case succ: n ih {
    cases ih,
    { right, exact odd_even.odd_even ih},
    left, exact odd_even.odd_even ih }
end

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]

That's the correct answer to the puzzle

[Mario Carneiro]

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]

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

inductive even_odd : bool → ℕ → Prop
| even_zero : even_odd tt 0
| even_succ : ∀ n, even_odd ff n → even_odd tt (n + 1)
| odd_succ : ∀ n, even_odd tt n → even_odd ff (n + 1)

def even := even_odd tt
def odd := even_odd ff

[Andrea Berlingieri]

Thank you for your answer Mario :smile: