Stream: new members

Topic: cases and rcases won't eliminate hypothesis

Robin Carlier (May 30 2020 at 15:16):

Hey, I'm in a situation that I suspect that is a bug, but It may be as well that I'm missing something obvious. Unfortunately, this is part of some bigger code chunk, with a few dependencies, so I can't post a MWE. Also I don't even know how to reproduce this behaviour.

I am writing a proof and I have some hypothesis with an existential quantifier, When I try to cases or rcases this hypothesis, I get the following error message: induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop. Now what is really weird is that in an earlier proof, with exactly the same hypothesis (when I say exactly, I mean I compared the two hypothesis with set_option pp.all true and they were really exactly the same) , and cases worked just fine.
Now even weirder: if I tidy? in my proof, and follow the first few instructions (a few fsplit and work_on_goal), tidy then suggests some cases is done on this hypothesis, and it works. I tried a bunch of things: if I open some subgoal, then it starts working as well.

here is what my exists statement looks like with pprint.all :

@Exists.{u+1} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(λ (R : set.{u} (@category_theory.over.{u u} C 𝒞 X)),
@Exists.{0}
(@has_mem.mem.{u u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(set.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
(@set.has_mem.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
R
(K X))
(λ
(H :
@has_mem.mem.{u u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(set.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
(@set.has_mem.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X)))
R
(K X)),
@has_subset.subset.{u} (set.{u} (@category_theory.over.{u u} C 𝒞 X))
(@set.has_subset.{u} (@category_theory.over.{u u} C 𝒞 X))
R
(@category_theory.sieve.arrows.{u u} C 𝒞 X S)))


Any idea how one would find a work-around for this kind of things? I can classical.some one the hypothesis but I'd rather avoid. Also, what kind of debug options (further than pp.print_all) would be usefull there to try to understand what's going on?

Johan Commelin (May 30 2020 at 15:19):

It means that your goal is not a Prop

Johan Commelin (May 30 2020 at 15:19):

So even though the hypothesis is the same, the rest of your context isn't

Robin Carlier (May 30 2020 at 15:19):

Oh well that explains everything

Johan Commelin (May 30 2020 at 15:21):

You'll have to either work your way around it (by doing stuff that makes your goal a Prop) or use choose.

Johan Commelin (May 30 2020 at 15:21):

For example, if you want to use exfalso, do that first, and afterwards the cases will work.

Robin Carlier (May 30 2020 at 15:22):

Well I guess I'll just use choose. Makes sense since the goal is to give some object.

Robin Carlier (May 30 2020 at 15:26):

Well thank you a lot, I was going mad over this!

No worries

Johan Commelin (May 30 2020 at 15:27):

Asking questions here is an encouraged method of solving problems

Kevin Buzzard (May 30 2020 at 16:20):

If you're using tactic mode to make something that isn't a proof, you might be doing it wrong.

Sometimes you can get around things not eliminating to Type by using classical. some

Last updated: May 11 2021 at 23:11 UTC