Why some results require both Unique and Fintype

Stream: mathlib4

[Jz Pan]

A search through loogle reveals that some results in mathlib requires both Unique and Fintype. What is the reason behind that? There is already an instance Unique -> Fintype in mathlib. So I think providing both will lead to a diamond, isn't it? If I define something which requires Fintype, and want to state some results of it requiring Unique, should I add both of Unique and Fintype as assumptions?

[Ruben Van de Velde]

It seems more likely that this is to avoid "diamonds" (not quite diamonds in this case). I can try to make an example in a bit

[Edward van de Meent]

@loogle Unique, Fintype

[loogle]

:search: Finset.univ_unique, Unique.fintype, and 46 more

[Edward van de Meent]

ah, but these say different things nope, i thought Unique was a Prop, but it isn't

[Aaron Liu]

The Prop-version is Nonempty + Subsingleton

[Ruben Van de Velde]

Hmm, I thought this would fail, but it doesn't.

import Mathlib

inductive I | a

instance : Unique I where
  default := I.a
  uniq x := by cases x; rfl

instance : Fintype I where
  elems := {I.a}
  complete x := by cases x; simp

lemma test {α : Type*} [Unique α] : Fintype.card α = 1 := by -- this is about Unique.fintype
  sorry

example : Fintype.card I = 1 := by
  rw [test]

[Edward van de Meent]

there is extra support for definitionally subsingleton types, i think...

[Edward van de Meent]

possibly a simple fix: add a falso : Empty -> I branch

[Edward van de Meent]

this should demonstrate the possible diamond i think:

import Mathlib

inductive I
  | a
  | falso (_:False) : I

instance : Unique I where
  default := I.a
  uniq x := by
    cases x
    · rfl
    · contradiction

noncomputable def i : I := Classical.choice ⟨.a⟩

noncomputable instance noninstance_fintype : Fintype I where
  elems := {i}
  complete x := by
    simp only [Finset.mem_singleton,Unique.eq_default]

lemma test {α : Type*} [Unique α] : Fintype.card α = 1 := by -- this is about Unique.fintype
  rfl -- not important

example : Fintype.card I = 1 := by
  rw [test]

[Edward van de Meent]

the funny thing is that this is no longer an issue when you remove the | falso branch and the . contradiction proof, demonstrating leans internal check for subsingleton types

[Edward van de Meent]

this issue can also occur without using Classical i think, let me see if i can cook up an example

[Aaron Liu]

Edward van de Meent said:

there is extra support for definitionally subsingleton types, i think...

They get structure-eta expanded into a structure with no fields, so any pair is equal.

[Edward van de Meent]

here's an example which uses Quot.sound instead, in a way that the concrete value is still reducible and computable:

import Mathlib

inductive I'
  | a
  | b

def I := Quot (fun (_ : I') _ => True)

instance : Unique I where
  default := Quot.mk _ I'.a
  uniq x := by
    apply Quot.ind _ x
    intro _
    exact Quot.sound trivial

noncomputable def i : I := Quot.mk _ I'.b

noncomputable instance bad_instance : Fintype I where
  elems := {i}
  complete x := by
    simp only [Finset.mem_singleton,Unique.eq_default]

lemma test {α : Type*} [Unique α] : Fintype.card α = 1 := by -- this is about Unique.fintype
  rfl -- not important

example : Fintype.card I = 1 := by
  rw [test]

[Aaron Liu]

Edward van de Meent said:

there is extra support for definitionally subsingleton types, i think...

You can get definitionally subsingleton types that don't have the property that any pair is defeq (for example, build a type version of docs#Acc)

[Ruben Van de Velde]

Nice tricks!