Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:41):

⊢ decidable (a ∈ s)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:43):

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

view this post on Zulip Kevin Lacker (Jun 13 2020 at 18:43):

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

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:43):

Right.

view this post on Zulip Kevin Lacker (Jun 13 2020 at 18:44):

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

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:44):

open_locale classical makes all propositions decidable.

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 18:44):

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

view this post on Zulip 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.

view this post on Zulip Kevin Lacker (Jun 13 2020 at 18:46):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Lacker (Jun 13 2020 at 18:48):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Lacker (Jun 13 2020 at 18:51):

thanks!


Last updated: May 08 2021 at 19:11 UTC