Noncomputable Functions

Stream: new members

[Marcus Rossel]

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?

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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).

[Marcus Rossel]

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

[Mario Carneiro]

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

[Mario Carneiro]

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, _)

[Mario Carneiro]

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