Zulip Chat Archive

Stream: new members

Topic: cannot find case names for induction


view this post on Zulip Reuben Rowe (Nov 27 2019 at 14:00):

Why do I get the error "could not find open goal of given case" with the following code?

universe u

variables { α : Type u } { size : α   }

include size
example : α  Prop
  :=
    begin
      assume a : α,
      let n := size a,
      induction n,
      case nat.zero {
        sorry,
      },
      case nat.succ {
        sorry,
      },
      done
    end

view this post on Zulip Patrick Massot (Nov 27 2019 at 14:05):

The error message is weird, but it's clearly Lean's answer to you trying to do something weird. Could you give more context? What are you actually trying to do?

view this post on Zulip Marc Huisinga (Nov 27 2019 at 14:12):

changing let to have works, but i am not sure what is going on either

view this post on Zulip Reuben Rowe (Nov 27 2019 at 14:22):

I want to prove a property about some relation on elements of an inductive type α\alpha, but it doesn't hold by structural induction because the definition of the relation uses an operation that changes the elements, but which does preserve the size, so my induction must be on the size of the elements.

view this post on Zulip Reuben Rowe (Nov 27 2019 at 14:23):

trying to do something weird

Why is this weird?

view this post on Zulip Patrick Massot (Nov 27 2019 at 14:30):

It will be very difficult to help you without a clearer explanation, or some code actually illustrating your use case. In the mean time, maybe reading https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Induction.20on.20minimum.20.22length.22 could help (what you wrote sounds vaguely similar to that old thread).

view this post on Zulip Sebastien Gouezel (Nov 27 2019 at 14:31):

At the beginning of your proof, you have chosen an element a. Now, it is fixed forever, so you can not do an induction on its size. The naive way to do this would be to prove a statement of the form : "for all n, for all elements a of sizen, then something holds", by induction over n. The non-naive way would be to generalize something.

view this post on Zulip Reuben Rowe (Nov 27 2019 at 14:41):

Ah yes, of course. I see - thanks! Sorry for all the stupid questions ;-)

view this post on Zulip Patrick Massot (Nov 27 2019 at 14:41):

Don't worry about asking "stupid" questions.

view this post on Zulip Marc Huisinga (Nov 27 2019 at 14:44):

especially not with error messages like these. i still find it strange that it only fails when case is used wheras you just can't prove it if you don't use case.

view this post on Zulip Kevin Buzzard (Nov 27 2019 at 16:04):

Error messages are not Lean's strong point. After a while you get used to them although I've not seen this one before


Last updated: May 12 2021 at 04:19 UTC