One implies Inhabited

Stream: Is there code for X?

[Snir Broshi]

Is there an instance of Inhabited for One or Zero?

import Mathlib

@[to_additive]
instance {α : Type*} [One α] : Inhabited α := ⟨1⟩

I couldn't find it on Loogle/LeanSearch, but a lot of structures have an Inhabited instance that just uses their Zero.
Is there a reason to not have such a "blanket" instance for all of them?

Here's an example using a new type:

import Mathlib

structure Foo where
  a : ℕ

instance : Zero Foo := ⟨⟨0⟩⟩

def foo : Foo := 0

#synth Inhabited Foo -- fails

@[to_additive]
instance {α : Type*} [One α] : Inhabited α := ⟨1⟩

#synth Inhabited Foo -- works

[Damiano Testa]

I think that this one specifically is not an instance, since a ring would have both a 0 and a 1 and the two instances would be (usually) different.

[Damiano Testa]

To expand, implicit in what I said above is the fact that docs#Inhabited actually comes with the specific "inhabiting" element (this is sometimes referred to by saying that Inhabited carries data). This is different from docs#Nonempty that only says that an element exists, but does not commit to a specific one (this is sometimes referred to by saying that Nonempty is a proposition -- and it really is in Prop!).

[Damiano Testa]

import Mathlib

variable {R} [Ring R]
#synth Inhabited R  -- failed to synthesize
#synth Nonempty R  -- works

[Kyle Miller]

Yeah, Inhabited is supposed to be whatever makes sense as the "default" element for a type. It's more of a programming concept than a mathematical concept.

Damiano mentions why there's no theoretic issue adding many Nonempty instances. There can be a practical issue though, since there's a temptation to try to turn Nonempty into a whole automated theorem prover (in the sense of the correspondence between nonempty types and true propositions) and all the instances could slow typeclass inference.