arbitrary is a constant

Stream: lean4

[Kenny Lau]

src/Init/Prelude.lean LL187-197:

class Inhabited (α : Sort u) where
  mk {} :: (default : α)

constant arbitrary [Inhabited α] : α :=
  Inhabited.default

instance : Inhabited (Sort u) where
  default := PUnit

instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
  default := fun _ => arbitrary

[Kenny Lau]

Why is arbitrary a constant? Won't this cause the definition to be inaccessible?

[Kenny Lau]

and why does the Inhabited (α → β) instance use the opaque arbitrary?

[Kenny Lau]

or am I completely misunderstanding how constant works?

[Leonardo de Moura]

Kenny Lau said:

Why is arbitrary a constant? Won't this cause the definition to be inaccessible?

It is to make sure your proof doesn't depend on the actual value of arbitrary.

[Kenny Lau]

So the following code I wrote is not advisable?

instance instSortInhabited' : Inhabited (Inhabited.default : Sort u) := ⟨PUnit.unit⟩

[Leonardo de Moura]

Kenny Lau said:

or am I completely misunderstanding how constant works?

A constant should be viewed as an opaque definition. It is like Lean 3 [irreducible], but it is enforced by the Kernel too.

[Leonardo de Moura]

So the following code I wrote is not advisable?

Not sure what you are trying to do. Happy to chat tomorrow on Zoom or gather.com :)

[Kenny Lau]

I was porting mathlib logic.basic whose L53 reads:

instance sort.inhabited' : inhabited (default (Sort*)) := ⟨punit.star⟩

[Leonardo de Moura]

Not sure where people use this instance, but the code you posted before is a faithful translation of L53.

[Mario Carneiro]

I think we need

instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
  default := fun _ => Inhabited.default

instead of arbitrary, because there are a decent number of uses of the inhabited instance that go via default instead of arbitrary, and expect it to be defined as the constant function (for example, we need the zero of the function space to be the constant function 0 and not some arbitrary thing). With the arbitrary definition on function types we get that

example : (Inhabited.default : Nat) = 0 := rfl -- this works
example : (Inhabited.default : Nat → Nat) 0 = 0 := rfl -- this fails

[Mario Carneiro]

(In fact, I think that arbitrary is almost never used in mathlib. In most uses we aren't assuming that the value doesn't matter, although it seems fine to opt into this by using arbitrary explicitly.)

[Johan Commelin]

arguably we are giving it different semantics... so maybe we can distinguish between arbitrary and default.

[Mario Carneiro]

As in having a separate typeclass for supplying arbitrary vs default? Perhaps we should call the former nonempty...

[Eric Wieser]

Isn't one typeclass enough, combined with the rule "never implement inhabited using arbitrary"?

[Eric Wieser]

Because then you can always fully unfold default, and it doesn't matter that arbitrary is implemented with default because you never unfold it

[Gabriel Ebner]

Maybe also add export Inhabited (default)