Zulip Chat Archive

Stream: general

Topic: Extract value from fin.find

Jure Taslak (Slovenia) (Sep 30 2021 at 10:07):

I have the following problem:
I'm trying to use the fin.find function to extract a value k : fin n for which p k holds. Together with that I would like a proof that this indeed holds, of the form pk : p k.
However if I use the cases tactic on fin.find p in the some k case I only get the k : fin n but no proof. I tried to get this proof using fin.find_spec but I got to the point I have to show fin.find p = some k, from where I don't really know where to go, as I thought this was the assumption of the case we are in.

Mario Carneiro (Sep 30 2021 at 10:08):

You probably need to match on docs#fin.find and docs#fin.find_spec together

Mario Carneiro (Sep 30 2021 at 10:08):

actually, looking at the definition of fin.find_spec it seems that cases e : fin.find p should work

Jure Taslak (Slovenia) (Sep 30 2021 at 10:10):

Aha you're right, I just had to specify e to have it as an assumption.
Thank you very much.

Last updated: Dec 20 2023 at 11:08 UTC