## Stream: general

### Topic: recursing on mutual inductive types

#### Jakob von Raumer (May 28 2018 at 16:10):

What's the best way to prove a theorem about a mutual type where the induction should use both types?

#### Jakob von Raumer (May 28 2018 at 16:17):

I know that there is mutual def but that's really not good to work with when you're not into pattern matching but instead use tactics...

#### Jakob von Raumer (May 28 2018 at 16:18):

There must be a recursion theorem somewhere that does what mutual def does, right?

#### Mario Carneiro (May 28 2018 at 20:19):

The usual approach is to use mutual def. Internally it is implemented by well founded recursion, so you can also do that yourself but the equation compiler does all the hard work. If you must do it manually (or if the default well founded recursion is not strong enough), you will probably want to state a custom induction principle, and prove it by unfolding the underlying ._mut_ type. Here's an example:

mutual inductive even, odd
with even : ℕ → Prop
| zero : even 0
| succ {n} : odd n → even (n+1)
with odd : ℕ → Prop
| succ {n} : even n → odd (n+1)

theorem even_mut_induction {E : ℕ → Prop} {O : ℕ → Prop}
(H0 : E 0)
(H1 : ∀ n, odd n → O n → E (n+1))
(H2 : ∀ n, even n → E n → O (n+1)) :
(∀ n, even n → E n) ∧ (∀ n, odd n → O n) :=
begin
suffices : ∀ i, even._mut_ i →
(match i with
| psum.inl ⟨n, ()⟩ := E n
| psum.inr ⟨n, ()⟩ := O n
end : Prop),
{ exact ⟨λ n, this _, λ n, this _⟩ },
intros i h,
induction h with n h IH n h IH,
{ exact H0 },
{ exact H1 n h IH },
{ exact H2 n h IH }
end


#### Jakob von Raumer (May 28 2018 at 23:09):

Thanks for the example :)

#### Jakob von Raumer (May 28 2018 at 23:10):

Too bad that the recursor you're proving there is not generated automatically

#### Mario Carneiro (May 28 2018 at 23:27):

I don't think we have a good story for what mutual induction principles look like in general

#### Mario Carneiro (May 28 2018 at 23:29):

There is some weak induction principle generated by default,

#print even.rec
-- protected def even.rec : ∀ (C : Π (a : ℕ), even a → Prop),
--  C 0 even.zero → (∀ {n : ℕ} (a : odd n), C (n + 1) _) → ∀ (a : ℕ) (x : even a), C a x
#print odd.rec
-- protected def odd.rec : ∀ (C : Π (a : ℕ), odd a → Prop),
--  (∀ {n : ℕ} (a : even n), C (n + 1) _) → ∀ (a : ℕ) (x : odd a), C a x


but as you can see they are non-mutual

#### Mario Carneiro (May 28 2018 at 23:29):

lean 4 will have mutual inductives built in the kernel, so this problem will have to be addressed

#### Jakob von Raumer (May 29 2018 at 16:10):

I'm not sure how to best express the induction principle (using and seems a bit of a hack)

#### Jakob von Raumer (May 29 2018 at 16:11):

What do you mean by "good story"? I don't have a reference at hand, but I'm pretty sure that problem is solved in theory

#### Sebastian Ullrich (May 29 2018 at 16:11):

That's how it's done in Isabelle, no? Except they have a nice meta and.

#### Jakob von Raumer (May 29 2018 at 19:09):

One could argue that since we got propositions as types, Lean's normal and is at least as nice as Isabelles meta and :grinning:

#### Mario Carneiro (May 29 2018 at 19:11):

there isn't really any dichotomy between ands in lean, so it's not a big problem. The one thing is that and only works on Props, while mutual inductions in general are mutual recursion, in which case you want a data type like pprod

#### Jakob von Raumer (May 29 2018 at 19:12):

Oh right... pprod then

Last updated: May 14 2021 at 21:11 UTC