## Stream: new members

### Topic: why a \in s doesn't work in an "if" clause

#### Kevin Lacker (Jun 13 2020 at 18:40):

This fails with "failed to synthesize class instance":

def one_iff_member (a : ℕ) (s : set ℕ) := if (a ∈ s) then 1 else 0

It seems like a \in s can't be used in this position, but a clause like "a < b" can be. What's the difference?

#### Kevin Buzzard (Jun 13 2020 at 18:41):

You don't say the crucial thing -- you don't say which instance it fails to synthesize.

#### Kevin Buzzard (Jun 13 2020 at 18:41):

⊢ decidable (a ∈ s)

#### Kevin Buzzard (Jun 13 2020 at 18:42):

Lean by default uses constructive logic, and because there is no algorithm for figuring out whether a is in your set, which could be for example nat if the Riemann Hypothesis is true and the empty set if it's false, Lean can't handle the if statement.

#### Kevin Lacker (Jun 13 2020 at 18:43):

hmm, that is strange to me, but ok. isn't the function one_iff_member definable regardless? i guess not

#### Kevin Buzzard (Jun 13 2020 at 18:43):

I'm a mathematician and I start most of my lean files with

import tactic

open_locale classical


and now Lean will ignore the fact that there's no algorithm.

#### Kevin Buzzard (Jun 13 2020 at 18:43):

if needs an algorithm for decidability, by default. It's as simple as that.

#### Kevin Lacker (Jun 13 2020 at 18:43):

ah, ok. this is similar to not being able to use em(something) by default then

Right.

#### Kevin Lacker (Jun 13 2020 at 18:44):

how does open_locale classical differ from open classical? i am already doing the latter

#### Kevin Buzzard (Jun 13 2020 at 18:44):

open_locale classical makes all propositions decidable.

#### Kevin Buzzard (Jun 13 2020 at 18:44):

open classical just gives you access to the functions in the classical namespace

#### Kevin Buzzard (Jun 13 2020 at 18:46):

If you have a maths background and don't know anything about decidability and computability (like me) then you just basically learn the tricks mathematicians use to switch all this constructive/computational stuff off, because to do normal maths as presented to undergraduate mathematicians it needs to be off sometimes.

#### Kevin Lacker (Jun 13 2020 at 18:46):

it still errors with "one_iff_member is noncomputable, it depends on classical.prop_decidable"

#### Kevin Buzzard (Jun 13 2020 at 18:46):

Yes, that's your next problem. So you have to mark the function noncomputable def one_iff_member...

#### Kevin Buzzard (Jun 13 2020 at 18:46):

or alternatively, if you get sick of writing noncomputable in front of half your functions, you can just write noncomputable theory at the top of your file.

#### Kevin Buzzard (Jun 13 2020 at 18:47):

import tactic

open_locale classical

noncomputable theory

-- you have now gone full classical mathematician

def one_iff_member (a : ℕ) (s : set ℕ) := if (a ∈ s) then 1 else 0

-- no errors


#### Kevin Lacker (Jun 13 2020 at 18:48):

ok thanks. i am aware of decidability and computability, i just dont think I care about them in this context

#### Kevin Buzzard (Jun 13 2020 at 18:48):

Now you can't "run your function", because you are doing classical mathematics so you're in a domain where the "proofs = programs" paradigm doesn't hold.

#### Kevin Lacker (Jun 13 2020 at 18:48):

is there some alternative where I can demonstrate that "a \in s" is computable

#### Kevin Buzzard (Jun 13 2020 at 18:49):

Yes, you can tell Lean that s is decidable, hang on, I'll try to remember how to do it

#### Kevin Buzzard (Jun 13 2020 at 18:49):

import tactic

def one_iff_member (a : ℕ) (s : set ℕ) [decidable_pred s] :=
if (a ∈ s) then 1 else 0


#### Kevin Lacker (Jun 13 2020 at 18:51):

thanks!

Last updated: May 08 2021 at 19:11 UTC