## Stream: lean4

### Topic: arbitrary is a constant

#### Kenny Lau (Jan 05 2021 at 21:25):

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 (Jan 05 2021 at 21:25):

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

#### Kenny Lau (Jan 05 2021 at 21:25):

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

#### Kenny Lau (Jan 05 2021 at 21:26):

or am I completely misunderstanding how constant works?

#### Leonardo de Moura (Jan 05 2021 at 21:26):

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 (Jan 05 2021 at 21:28):

So the following code I wrote is not advisable?

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


#### Leonardo de Moura (Jan 05 2021 at 21:28):

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 (Jan 05 2021 at 21:30):

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 (Jan 05 2021 at 21:33):

I was porting mathlib logic.basic whose L53 reads:

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


#### Leonardo de Moura (Jan 05 2021 at 21:40):

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

#### Mario Carneiro (Jan 06 2021 at 00:53):

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 (Jan 06 2021 at 00:57):

(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 (Jan 06 2021 at 05:27):

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

#### Mario Carneiro (Jan 06 2021 at 09:36):

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

#### Eric Wieser (Jan 06 2021 at 12:35):

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

#### Eric Wieser (Jan 06 2021 at 12:36):

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 (Jan 06 2021 at 12:51):

Maybe also add export Inhabited (default)

Last updated: May 07 2021 at 13:21 UTC