Zulip Chat Archive

Stream: new members

Topic: What is `some`?


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 19:50):

I'm learning non-constructive definitions from An Introduction to Lean (p. 25) and the command some h is used -- what does it mean?

view this post on Zulip Kenny Lau (Oct 14 2018 at 19:51):

h : \alpha |- some h : option \alpha

view this post on Zulip Chris Hughes (Oct 14 2018 at 19:51):

It's classical.some. Given a proof that exists x, p x, classical.some will return that x

view this post on Zulip Chris Hughes (Oct 14 2018 at 19:52):

Ignore Kenny, he's talking about option.some which is completely different.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 19:55):

It's classical.some. Given a proof that exists x, p x, classical.some will return that x

Oh nice -- so it's the eliminator for exists? But how is it different from exists.elim, or doing cases on the proof?

view this post on Zulip Patrick Massot (Oct 14 2018 at 19:55):

It's the non-broken one, yes

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 19:56):

exists.elim actually is broken? That explains a lot of problems I've had. Is it broken for finite sets too or only where choice is needed?

view this post on Zulip Chris Hughes (Oct 14 2018 at 19:58):

Almost. If you're trying to make a proof then you don't need it, you can just use cases or exists.elim. It's only if you're trying to make data that you need it. The one difference is between this and other eliminators is that you don't have
classical.some (exists.intro x h) = x, since this would cause contradictions because of proof irrelevance. exists.elim is not actually broken, that's just something people like to say when making fun of constructive mathematics.

view this post on Zulip Kenny Lau (Oct 14 2018 at 20:00):

s/people/Patrick Massot/

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:05):

Count me in too. Some of us don't care about constructive maths because we've spent decades doing normal maths and we're not going to change now. Others are younger and more open to these wacky ideas.

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:06):

Ps Abhi you should never have to ask what anything is. Copy and paste the code into a Lean session, make sure it compiles, and then just right-click on the thing that you want to know about.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 20:08):

Ps Abhi you should never have to ask what anything is. Copy and paste the code into a Lean session, make sure it compiles, and then just right-click on the thing that you want to know about.

Yeah, I didn't realise it was something in the classical library. I thought it was something like have, which you can check, but won't really give anything useful.

view this post on Zulip Chris Hughes (Oct 14 2018 at 20:08):

Sometimes the definitions can be a bit mysterious to a newcomer. classical.some is probably one of those

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:08):

some.png the some you're talking about is in classical.lean. Admittedly its definition is complicated :-/

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 20:09):

On the other hand, the last chapter of TPIL, which no doubt you have read because you've had all of about 8 days to learn about this stuff (;-) ) explains something about the classical stuff.

view this post on Zulip Patrick Massot (Oct 14 2018 at 20:09):

it could be worse (of course you need to understand the {... // ...} notation

view this post on Zulip Mario Carneiro (Oct 14 2018 at 20:12):

Yeah, I wouldn't say that's a particularly complicated definition. The complicated one is epsilon, which is surprisingly rarely used but is basically the same as some except you don't even need to prove existence first


Last updated: May 08 2021 at 18:17 UTC