Stream: new members
Topic: Noncomputable Functions
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.
classical.some be interpreted as always returning the same instance? And if not, then how are
noncomputable functions functions at all?
Sebastien Gouezel (Jan 08 2021 at 14:54):
Yes, it is a function, so on a given assumption it always returns the same result.
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.
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
Marcus Rossel (Jan 09 2021 at 10:26):
@Mario Carneiro How would that desugaring that cases on
exists x, p x look like?
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
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
px, and then at the nearest enclosing proof term you wrap it in
exists.cases_on h (\lam x px, _)
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