Zulip Chat Archive

Stream: lean4

Topic: arbitrary is a constant


view this post on Zulip Kenny Lau (Jan 05 2021 at 21:25):

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

view this post on Zulip Kenny Lau (Jan 05 2021 at 21:25):

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

view this post on Zulip Kenny Lau (Jan 05 2021 at 21:25):

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

view this post on Zulip Kenny Lau (Jan 05 2021 at 21:26):

or am I completely misunderstanding how constant works?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Jan 06 2021 at 05:27):

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

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Jan 06 2021 at 12:35):

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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jan 06 2021 at 12:51):

Maybe also add export Inhabited (default)


Last updated: May 07 2021 at 13:21 UTC