Nat.find

Stream: general

[Scott Morrison]

I am about to move docs#Nat.find from Mathlib to Std, and I would like to do a quick :bike: :house: on naming. Currently the docs say:

* `Nat.find_spec` is the proof that `Nat.find hp` satisfies `p`.
* `Nat.find_min` is the proof that if `m < Nat.find hp` then `m` does not satisfy `p`.
* `Nat.find_min'` is the proof that if `m` does satisfy `p` then `Nat.find hp ≤ m`.

I think find_min is an unhelpful name, and the fact that the other half of the specification is then called find_min' is especially unhelpful.

[Scott Morrison]

Is everyone happy with find_not_of_lt and find_le?

[Mario Carneiro]

find_min and find_min' are not two halves of the specification, they are the same spec written in contrapositive

[Scott Morrison]

Oops, indeed! Still, the prime is unhelpful?

[Mario Carneiro]

find_spec is the other half of the spec

[Mario Carneiro]

I think it should have a name better than find, this does not give an indication that it is finding the minimum element

[Scott Morrison]

Nat.findMin?

[Mario Carneiro]

makes sense

[Mario Carneiro]

is Nat.minimum used? Or is there precedent?

[Scott Morrison]

It doesn't seem to be used.

[Mario Carneiro]

not even in other namespaces?

[Scott Morrison]

An approximate precedent would be List.findIdx and List.findIdx?.

[Scott Morrison]

There is List.minimum.

[Mario Carneiro]

also WellFounded.min

[Mario Carneiro]

what's the ordinal one called

[Mario Carneiro]

I think it used to be omin but now it's just an Inf instance

[Mario Carneiro]

what is your interest in this function?

[Mario Carneiro]

I think there should also be a version of the function which starts the search at a given point

[Scott Morrison]

I wanted a def idx_of_mem [DecidableEq α] (xs : List α) (w : y ∈ xs) : Nat := ... and was going to define it via Nat.find.

[Mario Carneiro]

isn't that just findIdx?

[Scott Morrison]

Well, that returns an Option Nat, but yes, I could also define it in terms of that.

[Mario Carneiro]

I would not use Nat.find as a building block unless there wasn't any other structure in the problem. It's not very computationally efficient compared to almost any other strategy

[Mario Carneiro]

You said List.findIdx before, is that a thing? I would expect it to have that signature

[Scott Morrison]

I guess that does have the right signature. It doesn't take a y \mem xs argument and just returns the length of the list if there's nothing to find.

[Mario Carneiro]

it takes a predicate though, the std naming convention would call it findIdxP

[Mario Carneiro]

well actually I guess they all do

[Scott Morrison]

Oh, yes.

[Scott Morrison]

The place I'm using this is only for proving a property, I don't really care about the computational behaviour. I will just replace the implementation of idx_of_mem with something in terms of findIdx?, and not think any further about Nat.find.

[Scott Morrison]

Still the names of the lemmas are bad. :-)

[Yaël Dillies]

What does Idx even mean? That sounds unhelpfully obscure.

[Yaël Dillies]

Anyway, I would go for Nat.find_spec, Nat.of_lt_find, Nat.find_le.

[Damiano Testa]

I think that Idx stands for Index, but I also have to remind myself of this every time I see it.