cases and rcases won't eliminate hypothesis

Stream: new members

[Robin Carlier]

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]

It means that your goal is not a Prop

[Johan Commelin]

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

[Robin Carlier]

Oh well that explains everything

[Johan Commelin]

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

[Johan Commelin]

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

[Robin Carlier]

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

[Robin Carlier]

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

[Johan Commelin]

No worries

[Johan Commelin]

Asking questions here is an encouraged method of solving problems

[Kevin Buzzard]

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