Zulip Chat Archive

Stream: general

Topic: recursing on mutual inductive types


view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Jakob von Raumer (May 28 2018 at 16:18):

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

view this post on Zulip 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

view this post on Zulip Jakob von Raumer (May 28 2018 at 23:09):

Thanks for the example :)

view this post on Zulip Jakob von Raumer (May 28 2018 at 23:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (May 29 2018 at 16:11):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Jakob von Raumer (May 29 2018 at 19:12):

Oh right... pprod then


Last updated: May 14 2021 at 21:11 UTC