recursing on mutual inductive types

Stream: general

[Jakob von Raumer]

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

[Jakob von Raumer]

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]

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

[Mario Carneiro]

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]

Thanks for the example :)

[Jakob von Raumer]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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]

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

[Jakob von Raumer]

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]

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]

Oh right... pprod then