Prop-valued "I have one term"

Stream: Is there code for X?

[Kevin Buzzard]

We have unique but it's Type-valued. I think I want to say "I have one element" in a Prop-valued way. I went for the definition of is_singleton below (and proved the lemmas I need for the application in LTE), but is this not the sort of thing I should be doing? Is this in the library already and I just missed it? If not, is there a reason it's not there?

import tactic

def is_singleton (X : Sort*) : Prop :=
nonempty (unique X)

noncomputable def is_singleton.default {X : Sort*} (hx : is_singleton X) :
  X := (nonempty.some hx).default

def punit.is_singleton : is_singleton (punit) :=
⟨punit.unique⟩

def is_singleton.to_subsingleton {X : Sort*} (hX : is_singleton X) :
  subsingleton X :=
begin
  unfreezingI {rcases hX with ⟨x, hx⟩},
  exact ⟨λ a b, (hx a).trans (hx b).symm⟩,
end


theorem is_singleton_iff_forall_bijective_to_punit (X : Sort*) :
  is_singleton X ↔ ∀ f : X → punit, function.bijective f :=
begin
  split,
  { rintro ⟨⟨x⟩, hx⟩ f,
    exact ⟨λ a b h, (hx a).trans (hx b).symm, λ s, ⟨x, subsingleton.elim _ _⟩⟩ },
  { intro h,
    cases h (λ x, punit.star) with finj fsurj,
    choose g hg using fsurj,
    refine ⟨⟨⟨g punit.star⟩, λ x, finj rfl⟩⟩ }
end

theorem is_singleton_iff_forall_bijective_to_is_singleton (X : Sort*) :
  is_singleton X ↔ ∀ (Y : Type*) (hY : is_singleton Y)
  (f : X → Y), function.bijective f :=
begin
  split,
  { rintro ⟨⟨x⟩, hx⟩ Y hY f,
    haveI := hY.to_subsingleton,
    exact ⟨λ a b h, (hx a).trans (hx b).symm, λ s, ⟨x, subsingleton.elim _ _⟩⟩ },
  { intro h,
    cases h punit punit.is_singleton (λ x, punit.star) with finj fsurj,
    choose g hg using fsurj,
    refine ⟨⟨⟨g punit.star⟩, λ x, finj rfl⟩⟩ }
end

theorem is_singleton_iff_exists_bijective_to_punit (X : Sort*) :
  is_singleton X ↔ ∃ f : X → punit, function.bijective f :=
begin
  split,
  { rintro ⟨⟨x⟩, hx⟩,
    use (λ x, punit.star),
    refine ⟨λ a b _, (hx a).trans (hx b).symm,
      λ a, ⟨x, subsingleton.elim _ _⟩⟩ },
  { rintro ⟨f, finj, fsurj⟩,
    choose g hg using fsurj,
    refine ⟨⟨⟨g punit.star⟩, λ x, finj $ subsingleton.elim _ _⟩⟩ },
end

theorem is_singleton_iff_exists_bijective_to_is_singleton (X : Sort*) :
  is_singleton X ↔ ∃ (Y : Sort*) (hY : is_singleton Y) (f : X → Y), function.bijective f :=
begin
  split,
  { rintro ⟨⟨x⟩, hx⟩,
    use [punit, punit.is_singleton, (λ x, punit.star)],
    refine ⟨λ a b _, (hx a).trans (hx b).symm,
      λ a, ⟨x, subsingleton.elim _ _⟩⟩ },
  { rintro ⟨Y, hY, f, finj, fsurj⟩,
    choose g hg using fsurj,
    haveI := hY.to_subsingleton,
    refine ⟨⟨⟨g hY.default⟩, λ x, finj $ subsingleton.elim _ _⟩⟩ },
end

[Yakov Pechersky]

Can't you just use [subsingleton X] [nonempty X]?

[Kevin Buzzard]

Oh that's maybe why it's not there.

[Yakov Pechersky]

The one thing I don't know how to do is conjure a term x : X, without doing cases on the nonempty hyp. Probably doing it on id h, to retain it in the TC cache.

[Yakov Pechersky]

Use "arbitrary", I guess

[Eric Wieser]

obtain ⟨x⟩ := id ‹nonempty α› is probably reasonable idiomatic

[Eric Wieser]

Do we have the lemma that conjures nonempty (unique X) from [subsingleton X] [nonempty X]?

[Yakov Pechersky]

We have the defn that makes a unique X from data and subsingleton X. Probably not yet what you're asking about.

[Eric Wieser]

What's that def?

[Eric Wieser]

Ah found it:

casesI ‹nonempty X›.map unique_of_subsingleton,  -- put `unique X` in the context

[Johan Commelin]

I think it would be nice to have a variant of tactic#inhabit that allows you to specify an alias for the default element.

[Johan Commelin]

inhabit X with x

[Johan Commelin]

This could be as simple as being a shortcut for

inhabit X,
let x := default X

[Reid Barton]

Why do you have all this unfreezingI/haveI/etc. stuff if is_singleton is not a class?

[Kevin Buzzard]

You mean in is_singleton.to_subsingleton? I have no idea. I tried doing cases and I got the *frozen local instance" error

[Kevin Buzzard]

MWE (note that nonempty is a class):

import tactic

def is_singleton (X : Sort*) : Prop :=
nonempty (unique X)

def is_singleton.to_subsingleton {X : Sort*} (hX : is_singleton X) :
  subsingleton X :=
begin
  -- cases hX, -- "failed to revert 'hX', it is a frozen local instance "
  unfreezingI {rcases hX with ⟨x, hx⟩},
  exact ⟨λ a b, (hx a).trans (hx b).symm⟩,
end

[Eric Rodriguez]

this does seem like a bug, right? as it shouldn't be in the instance cache at all

[Eric Rodriguez]

yeah, it's definitely a bug:

import tactic

def is_singleton (X : Sort*) : Prop :=
nonempty (unique X)

def is_singleton.to_subsingleton {X : Sort*} (hX : is_singleton X) :
  subsingleton X :=
begin
  --rw is_singleton at hX ; works if you do this!
  --have := classical.arbitrary (unique X) ; no instance error
  cases hX,
end

[Eric Wieser]

I think lean is seeing through is_singleton and finding the class attribute on nonempty

[Eric Rodriguez]

but if you rw it to the nonempty term you don't get the issue

[Eric Rodriguez]

I am confused how because the code seems pretty bulletproof