## Stream: new members

### Topic: cannot find case names for induction

#### 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


#### 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?

#### Marc Huisinga (Nov 27 2019 at 14:12):

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

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

#### Reuben Rowe (Nov 27 2019 at 14:23):

trying to do something weird

Why is this weird?

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

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

#### Reuben Rowe (Nov 27 2019 at 14:41):

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

#### Patrick Massot (Nov 27 2019 at 14:41):

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.