Zulip Chat Archive

Stream: new members

Topic: Noncomputable Functions


view this post on Zulip Marcus Rossel (Jan 08 2021 at 14:52):

I just noticed that this works:

example (h :  n, n > 9) : classical.some h = classical.some h := refl _

I was kind of surprised by this, because I didn't think that classical.some would always return the same instance, but rather just "some" instance. On the other hand classical.some is a function, so I guess it has to always return the same thing.
So should classical.some be interpreted as always returning the same instance? And if not, then how are noncomputable functions functions at all?

view this post on Zulip Sebastien Gouezel (Jan 08 2021 at 14:54):

Yes, it is a function, so on a given assumption it always returns the same result.

view this post on Zulip Kevin Buzzard (Jan 08 2021 at 15:39):

It is an extraordinary function -- it chooses, once and for all, a "special" element in every nonempty type.

view this post on Zulip Mario Carneiro (Jan 08 2021 at 19:58):

By the way, it is this "function-ness" that is exactly what makes the axiom of choice an actual axiomatic extension of the theory; if you just wanted a random element of the type every time you could do a desugaring that cases on exists x, p x whenever you make reference to this magical nondeterministic constant. This would not satisfy your example, since it's not true that \forall n, n > 9 -> \forall n', n' > 9 -> n = n' (which is roughly what you would get by desugaring your statement under the nondeterministic reading of classical.some).

view this post on Zulip Marcus Rossel (Jan 09 2021 at 10:26):

@Mario Carneiro How would that desugaring that cases on exists x, p x look like?

view this post on Zulip Mario Carneiro (Jan 09 2021 at 10:30):

It's a bit complex in general, you have to lift the cases out to the nearest enclosing proof term, which requires some fairly low level elaborator support to make work. The lean 4 elaboration of (<- tac) in do notation is an example of this kind of transformation

view this post on Zulip Mario Carneiro (Jan 09 2021 at 10:32):

But informally, the idea is pretty simple: for every occurrence of some h and some_spec h, you replace them with new variables x and px, and then at the nearest enclosing proof term you wrap it in exists.cases_on h (\lam x px, _)

view this post on Zulip Mario Carneiro (Jan 09 2021 at 10:35):

For theorem statements, like the example I gave above, you use \forall x px, _ instead as additional arguments to the implication being proved


Last updated: May 15 2021 at 23:13 UTC