cannot find case names for induction

Stream: new members

[Reuben Rowe]

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

[Patrick Massot]

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?

[Marc Huisinga]

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

[Reuben Rowe]

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.

[Reuben Rowe]

trying to do something weird

Why is this weird?

[Patrick Massot]

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).

[Sebastien Gouezel]

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.

[Reuben Rowe]

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

[Patrick Massot]

Don't worry about asking "stupid" questions.

[Marc Huisinga]

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.

[Kevin Buzzard]

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