# Zulip Chat Archive

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

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 (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 `classical.some`

).

#### 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 `x`

and `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