## Stream: new members

### Topic: construct a term from a nonempty type

#### Luca Seemungal (Apr 14 2020 at 14:50):

Hi, how do I give myself a term a of a nonempty type α? At least that's what I assume nonempty means.
Cheers :)

universe u
example {α : Type u} [nonempty α] : α :=
begin
sorry
end


#### Kevin Buzzard (Apr 14 2020 at 14:51):

nonempty alpha has type Prop, and you want to move from that to type Type, you have to be noncomputable.

#### Kevin Buzzard (Apr 14 2020 at 14:52):

This is why it is more of a kerfuffle than you might think.

#### Luca Seemungal (Apr 14 2020 at 14:53):

how do I become noncomputable? Am I already noncomputable?

oh

#### Kenny Lau (Apr 14 2020 at 14:53):

import logic.basic

#check @classical.choice -- classical.choice : Π {α : Sort u_1}, nonempty α → α


#### Kevin Buzzard (Apr 14 2020 at 14:53):

You're a mathematician, right? Then you're noncomputable :-)

#### Kevin Buzzard (Apr 14 2020 at 14:53):

universe u
noncomputable example {α : Type u} [nonempty α] : α :=
classical.choice _inst_1


#### Kevin Buzzard (Apr 14 2020 at 14:54):

You have to use the computer scientists' axiom of choice :-)

#### Luca Seemungal (Apr 14 2020 at 14:54):

yes hahaha

ok the #check @classical.choice works

#### Luca Seemungal (Apr 14 2020 at 14:55):

oh nice it all works, cheers!

#### Kevin Buzzard (Apr 14 2020 at 14:55):

The difference between nonempty and inhabited is that nonempty is Prop-valued, and inhabited is Type-valued.

#### Kevin Buzzard (Apr 14 2020 at 14:56):

If you proved nonempty alpha but had every intention of occasionally using the element to actually make data (stuff in the Type universe) then you might want to consider using inhabited alpha instead. To a mathematician these are the same thing, but this whole Prop / Type dichotomy is a thing for computer scientists.

#### Luca Seemungal (Apr 14 2020 at 14:57):

does that mean that nonempty tells me that a term exists, whereas inhabited hands me a term?

#### Kevin Buzzard (Apr 14 2020 at 14:58):

Yes that's basically it. People who want everything to be computable can't get from Prop to Type, so they might want not to go into Prop in the first place.

#### Kevin Buzzard (Apr 14 2020 at 15:00):

But if all you ever want to do is prove theorems, then you might never notice the difference.

#### Kevin Buzzard (Apr 14 2020 at 15:03):

import tactic

example (α : Type) : nonempty α → nonempty (α × α) :=
begin
intro h,
cases h with a, -- no problem here because goal is a Prop
use (a,a)
end

example (α : Type) : nonempty α → α :=
begin
intro h, -- goal is a Type
cases h, -- induction tactic failed, recursor 'nonempty.dcases_on' can only eliminate into Prop

end


#### Kevin Buzzard (Apr 14 2020 at 15:04):

Think of it as a bug, not a feature ;-)

#### Kevin Buzzard (Apr 14 2020 at 15:05):

example (α : Type) : inhabited α → α :=
begin
intro h, -- goal is a Type
cases h with a, -- works fine
use a
end


#### Luca Seemungal (Apr 14 2020 at 15:06):

ah right i see

but if i am noncomputable I can solve the second example nonempty alpha -> alpha by using classical.choice h

ok thanks

#### Kevin Buzzard (Apr 14 2020 at 15:08):

There's a catch though:

#### Kevin Buzzard (Apr 14 2020 at 15:09):

noncomputable def thing (α : Type) : nonempty α → α :=
begin
intro h, -- goal is a Type
exact classical.choice h
end

#print axioms thing -- classical.choice


Lean remembers that you used a nonconstructive axiom

#### Luca Seemungal (Apr 14 2020 at 16:52):

how come I can't use contradiction? I've done open classical and local attribute classical.prop_decidable

import logic.basic
open classical
local attribute classical.prop_decidable

universe u

example {α : Type u} (p : α → Prop) [nonempty α] : ¬ (∃ x, p x) ↔ ∀ x, ¬(p x) :=
begin
split,
by_contra, -- tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
end


#### Reid Barton (Apr 14 2020 at 16:58):

Because neither open classical nor local attribute classical.prop_decidable is correct (you opened a namespace, and locally gave classical.prop_decidable no attributes). Try open_locale classical or local attribute [instance] classical.prop_decidable, preferably the former.

#### Luca Seemungal (Apr 14 2020 at 17:04):

ok it seems that my lean installation doesn't know what open_locale is

(having just looked at the docs for the first time in a while), should I be using leanpkg or leanprojectto manage my lean installation?

#### Patrick Massot (Apr 14 2020 at 17:16):

leanproject

#### Luca Seemungal (Apr 14 2020 at 17:19):

ok thanks

i managed to get local attribute [instance] classical.prop_decidable working but not open_locale classical (lean seems to think that I'm trying to import open_locale and classical but I've no idea why)

#### Patrick Massot (Apr 14 2020 at 17:20):

You can't put that right after the imports

#### Patrick Massot (Apr 14 2020 at 17:20):

The Lean parser has no way to know this is not a file name

#### Kevin Buzzard (Apr 14 2020 at 17:20):

until the new PR hits :-)

Yes

#### Kevin Buzzard (Apr 14 2020 at 17:21):

Just write something like "universe u" before open_locale

and is released

#### Luca Seemungal (Apr 14 2020 at 17:21):

ah ok I see, cheers

#### Luca Seemungal (Apr 14 2020 at 17:21):

ah yes, now my lean is lean 3.8.0 rather than lean 3.4.2, this is very nice

#### Kevin Buzzard (Apr 14 2020 at 17:48):

Patrick wrote the tool, it is amazing for beginnerseveryone :-)

#### Kevin Buzzard (Apr 14 2020 at 17:48):

I've had huge success with it at Xena.

#### Kevin Buzzard (Apr 14 2020 at 17:49):

And you should have all olean files as well so no orange bars (or, orange bars which disappear quickly)

Last updated: May 13 2021 at 06:15 UTC