Zulip Chat Archive

Stream: new members

Topic: i'm just playing around with lean lol


Huỳnh Trần Khanh (Jun 22 2021 at 15:08):

What does classical.choice x._proof_1 1 = classical.choice x._proof_1 2 mean?

noncomputable def x :   string := classical.choice nonempty_of_inhabited

lemma this_should_be_unprovable_right : x 1 = x 2 := begin
  rw x,
end

Huỳnh Trần Khanh (Jun 22 2021 at 15:11):

like the _proof_1 thing looks really strange to me

Kyle Miller (Jun 22 2021 at 15:22):

If you do

#print x
#print x._proof_1

you can see

noncomputable def x :   string :=
classical.choice x._proof_1

and

theorem x._proof_1 : nonempty (  string) :=
nonempty_of_inhabited

Lean tends to generate many underscore functions when it creates definitions (especially for pattern matching). I'm not sure why it split off this nonempty instance like this.

Mario Carneiro (Jun 22 2021 at 17:22):

And indeed, that theorem is unprovable. What you have done is choose a "random" function ℕ → string using choice, and for such a function we know nothing about its values besides the type, so x 1 : string may or may not be equal to x 2 : string


Last updated: Dec 20 2023 at 11:08 UTC