Is "choice ⟨1⟩" equal to "1"?

Stream: new members

[Deming Xu]

I would like to know whether one of the following two theorems, "yes" and "no", can be proved, or neither of them can be proved?

open Classical

#print Nonempty

#check choice

noncomputable def x : Nat := choice ⟨ 1 ⟩

#print x.proof_1

theorem yes : x = 1 := by
  rw [x]
  -- ⊢ choice x.proof_1 = 1
  rfl -- error

theorem no : x ≠ 1 := by
  rw [x]
  -- ⊢ choice x.proof_1 ≠ 1
  rfl -- error

According to my understanding, this code means that I know there is an element 1 in the natural number type, so I can use ⟨ 1 ⟩ to prove Nonempty Nat. Then according to the axiom of choice, I can pick out some element from this non-empty natural number type, and call it x.

So, can I still judge whether x is 1? Is x=1 a proposition that cannot be proved or falsified?

[Yakov Pechersky]

Since docs#Classical.choice (a function into Sort) is axiomatized with no partner specification axiom, then no, you can never prove either of the statements. The only thing I think you might be able to prove is that example : Classical.choice (Nonempty.intro 1) = Classical.choice (Nonempty.intro 0) := congrArg _ rfl thanks to Nonempty being a Prop

[Yakov Pechersky]

Compare docs#Classical.choice to the pair of docs#Classical.choose and docs#Classical.choose_spec

[Edward van de Meent]

note that these are also available as docs#Exists.choose and docs#Exists.choose_spec , enabeling dot notation