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

Stream: new members

[Kevin Lacker]

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]

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

[Kevin Buzzard]

⊢ decidable (a ∈ s)

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Lacker]

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

[Kevin Buzzard]

Right.

[Kevin Lacker]

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

[Kevin Buzzard]

open_locale classical makes all propositions decidable.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

import tactic

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

[Kevin Lacker]

thanks!