Zulip Chat Archive

Stream: new members

Topic: construct a term from a nonempty type


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

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 14:52):

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

view this post on Zulip Luca Seemungal (Apr 14 2020 at 14:53):

how do I become noncomputable? Am I already noncomputable?

view this post on Zulip Luca Seemungal (Apr 14 2020 at 14:53):

oh

view this post on Zulip Kenny Lau (Apr 14 2020 at 14:53):

import logic.basic

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 14:54):

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

view this post on Zulip Luca Seemungal (Apr 14 2020 at 14:54):

yes hahaha

ok the #check @classical.choice works

view this post on Zulip Luca Seemungal (Apr 14 2020 at 14:55):

oh nice it all works, cheers!

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

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

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 14:57):

obligatory link to TPIL

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

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

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 15:04):

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

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

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

view this post on Zulip Luca Seemungal (Apr 14 2020 at 15:06):

ok thanks

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 15:08):

There's a catch though:

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

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

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

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

view this post on Zulip Patrick Massot (Apr 14 2020 at 17:16):

leanproject

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

view this post on Zulip Patrick Massot (Apr 14 2020 at 17:20):

You can't put that right after the imports

view this post on Zulip Patrick Massot (Apr 14 2020 at 17:20):

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 17:20):

until the new PR hits :-)

view this post on Zulip Patrick Massot (Apr 14 2020 at 17:20):

Yes

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 17:21):

Just write something like "universe u" before open_locale

view this post on Zulip Patrick Massot (Apr 14 2020 at 17:21):

and is released

view this post on Zulip Luca Seemungal (Apr 14 2020 at 17:21):

ah ok I see, cheers

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 17:48):

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

view this post on Zulip Kevin Buzzard (Apr 14 2020 at 17:48):

I've had huge success with it at Xena.

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