arbitrary nat as output

Stream: new members

[Chris M]

I'm somewhat puzzled by the following function definition: def f: ℕ → ℕ := fun n, arbitrary ℕ . It seems to me that f is not actually a mathematical function. It takes a natural number as input and outputs, ... a term that has type nat but it's not an actual natural number. I'm tempted to say that mathematically speaking, this is an ill-defined function? Should I think of this as essentially "using the axiom of choice"?

[Jalex Stark]

there is in fact a natural number in there

[Shing Tak Lam]

It just outputs the provided default for the inhabited typeclass on that type. For nat, the inhabited instance is

instance : inhabited ℕ :=
⟨nat.zero⟩

so arbitrary ℕ = 0.

[Chris M]

Ohh I see. Does this hold for all arbitrary ...for some type at ...?

[Jalex Stark]

did you try going to the definition of arbitrary?

[Jalex Stark]

there's no magic going on anywhere

[Jalex Stark]

Shing Tak just unfolded the definition into an english sentence of comparable length

[Mario Carneiro]

This should be contrasted with def f: ℕ → ℕ := fun n, @classical.choice ℕ _, which is a function from nat to nat that we can prove is constant but for which we don't know the value

[Jacques Carette]

Is it just me, but while inhabited is a great name, arbitrary is likely to lead to confusion (witness: this thread) ?

[Jalex Stark]

i feel like arbitrary is well-named but needs a docstring. It's very close to the mathematician's "arbitrary".

[Reid Barton]

arbitrary is basically unused anyways

[Reid Barton]

at least, in mathlib

[Jasmin Blanchette]

Since the class is called inhabited, maybe inhabitant or some_inhabitant?

[Jasmin Blanchette]

We used to have arbitrary in Isabelle with the same meaning as in Lean (except that it worked with all types, since all HOL types are inhabited). It was renamed undefined. I never felt this was much of an improvement.

[Andrew Ashworth]

Is arbitrary even going to survive until Lean 4? I think where they are used - they can be replaced with meta constants.

[Reid Barton]

I actually had misremembered how this is set up

[Reid Barton]

arbitrary is basically an irreducible version of default which is the guy from inhabited

[Andrew Ashworth]

I always wondered why more arbitrary wasn't used in mathlib. It was supposed to be the canonical 37 for partial functions.

[Jalex Stark]

obviously anything one can do with arbitrary one can also do with default, but arbitrary is making a promise to the reader that all you need is some inhabited instance, not any particular one

[Reid Barton]

Andrew Ashworth said:

I always wondered why more arbitrary wasn't used in mathlib. It was supposed to be the canonical 37 for partial functions.

If you're going to totalize, it's usually more useful to totalize in a convenient way (normally meaning by 0 and not by 37)

[Reid Barton]

From a mathematician's perspective, inhabited ought to be called "pointed"

[Reid Barton]

or at least the definition of pointed would look exactly the same up to renaming

[Jacques Carette]

pointed is great, but one assumes that if something is pointed, then homomorphisms preserve the given point.

To use HoTT terminology, arbitrary does bring to mind a 'mere inhabitant'. That is indeed quite useful, as it corresponds nicely to the classical notion of inhabitation.

In all my codes, I consider the use of having a default point a "code smell". I have indeed been working to remove that from one of my student's codes in the last week. (inhabited is ok, as I know I can't rely on that mere point in any ways; default is more dangerous, as downstream code has this way of assuming it means pointed when there is in fact no such guarantee). But that is what my experience tells me, I certainly wouldn't make that a hard rule, not without more evidence.

[Reid Barton]

And I guess the point is even when you're in a general setting like option.iget where you can't totalize by something like 0, it's still more useful to pass on the option to know the default value is 0 to your client by using default, rather than using arbitrary which prevents anyone from knowing about the value