Zulip Chat Archive

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?

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

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:57):

obligatory link to TPIL

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

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

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)