Zulip Chat Archive

Stream: new members

Topic: Cases tactic fails


view this post on Zulip Nicolò Cavalleri (Jul 07 2020 at 16:11):

Suppose I am trying to prove something is a commutative group, and for this I need to build a function add. There is a lemma that tells me that under some hypotheses, that are satisfied in my case, there exists a map with certain properties. I need to use that map to build my add function, however in order to get the map I need to give this lemma the hypotheses it wants and in order to do it I switch into tactic mode. After I give it the hypotheses I get an hypothesis of the forms \esists f, ... and I need to get that f. However, I cannot use cases as my goal is not a prop. What can I do? It is really hard for me to create a mwe now as there's a lot of code in between what I am doing and the current version of Mathlib I think

view this post on Zulip Yakov Pechersky (Jul 07 2020 at 16:16):

obtain ⟨f, hf⟩ := hyp

view this post on Zulip Yakov Pechersky (Jul 07 2020 at 16:17):

where hyp is the hypothesis of the form \ex f, p f, and f will be the function that satisfies hf : p f

view this post on Zulip Nicolò Cavalleri (Jul 07 2020 at 16:21):

It still tells me

induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop

with obtain, I guess you'd need to see the code?

view this post on Zulip Alex J. Best (Jul 07 2020 at 16:29):

Sounds like docs#classical.some is what you want? You can use that to get something from an exists, and docs#classical.some_spec to show that that term has the right property.

view this post on Zulip Reid Barton (Jul 07 2020 at 16:31):

It also sounds like maybe the lemma you use should not have been a lemma at all, but rather a def

view this post on Zulip Nicolò Cavalleri (Jul 08 2020 at 10:21):

It is actually a definition but it there is still an exists in it. It is analogous to the definition of topological fiber bundle:

def is_topological_fiber_bundle : Prop :=
 x : Z, e : bundle_trivialization F proj, x  e.source

I have my x where I want to get my trivialization and I need to use e but I can't manage to extract it. I will try Alex's suggestion

view this post on Zulip Reid Barton (Jul 08 2020 at 10:50):

Perhaps you could explain what it is you want to do?

view this post on Zulip Nicolò Cavalleri (Jul 08 2020 at 14:19):

Reid Barton said:

Perhaps you could explain what it is you want to do?

Actually what I was trying to do was stupid and I changed everything but thanks a lot for the help!


Last updated: May 09 2021 at 20:11 UTC