Zulip Chat Archive

Stream: lean4

Topic: Decidable proposition

Pavel Shuhray (Mar 21 2022 at 11:17):

variable (a : Prop)
variable (p : a ∨ ¬ a)

How can I define

if  a then 0 else 1

Henrik Böving (Mar 21 2022 at 11:21):

you have to provide an instance [Decidable a]

Henrik Böving (Mar 21 2022 at 11:21):

(can also be done as a variable)

Patrick Johnson (Mar 21 2022 at 11:47):

Try this:

noncomputable def n : Nat :=
  have := Classical.choice $ match p with
    | Or.inl h => ⟨isTrue h⟩
    | Or.inr h => ⟨isFalse h⟩
  if a then 0 else 1

Kyle Miller (Mar 21 2022 at 11:50):

If we're going to pull in Classical.choice, may as well use

noncomputable def n : Nat :=
  have := Classical.propDecidable
  if a then 0 else 1

Kyle Miller (Mar 21 2022 at 11:51):

I think the underlying question might be "if decidability implies LEM, can LEM be used for decidability?" At least, that's the question I had when I read Pavel's question. (I think the answer is "no")

Mario Carneiro (Mar 21 2022 at 11:51):

And the answer to this question is "no"

Mario Carneiro (Mar 21 2022 at 11:52):

The existence of a function if a then 0 else 1 is equivalent to Decidable a which is strictly stronger than a \/ ~a

Pavel Shuhray (Mar 23 2022 at 07:19):

More general question: if we have a proof of

∃! x A(x)

can we extract this unique x? I know problems with strong ∃ in Calculus of Constructions.

Kevin Buzzard (Mar 23 2022 at 07:20):

Not without choice no

Kevin Buzzard (Mar 23 2022 at 07:20):

You can't move from Prop to Type in Lean without magic

Last updated: Dec 20 2023 at 11:08 UTC