Zulip Chat Archive

Stream: lean4

Topic: Unfold fail & LazyList nested induction issue


James Gallicchio (Mar 10 2022 at 10:22):

On further poking it looks like the second issue is because it tries to generalize h, but then the motive for the nested induction is left as a meta-variable and thus doesn't have the (h : _) -> binder it expects to have

James Gallicchio (Mar 10 2022 at 10:24):

which, actually, is still the case if h is moved into the return type:

theorem rotate_inv {F : LazyList α} {R} {S}
  : (h : _)  (rotate F R S h).toList = F.toList ++ R.reverse
  := by
  induction F
  case mk fn ih =>
    intro h
    exact ih ()
  repeat {sorry}

The intro raises the same error.

James Gallicchio (Mar 11 2022 at 08:23):

(Cleaned up the MWE above quite a bit; this seems to be as simple as I can get it)

Leonardo de Moura (Mar 11 2022 at 20:55):

Thanks for the MWE. I am working on it.


Last updated: Dec 20 2023 at 11:08 UTC