fin.find

Stream: general

[Chris Hughes]

I wrote this function

def fin.find {n : ℕ} {p : fin n → Prop} [decidable_pred p] (h : ∃ a : fin n, p a) : fin n :=
have h : ∃ a, ∃ h : a < n, p ⟨a, h⟩, from let ⟨⟨a, han⟩, ha⟩ := h in ⟨a, han, ha⟩,
⟨nat.find h, (nat.find_spec h).fst⟩

But then it occured to me, that this will be slower than necessary because it will be checking whether a bunch of natural numbers are < n unnecessarily. What's the fastest way to write this?

[Kevin Buzzard]

You sound like my son. He was complaining yesterday that (a/hcf(a,b),b/hcf(a,b)) was slow in his home-made C++ rationals class because one had to evaluate the hcf twice (this was part of some C++ constructor syntax where you didn't have to space to evaluate the function and store the result, apparently). I'm like "why does anyone even care? Just reason about the objects, don't actually compute them!". But each to their own, I suppose.

[Kevin Buzzard]

Chris, you're basically asking how to write a for loop in functional programming I guess.

[Kevin Buzzard]

Coincidentally I just wrote another fin function:

inductive xfin : ℕ → Type
| zero : ∀ n, xfin (nat.succ n)
| succ : ∀ n, xfin n → xfin (nat.succ n)

[Chris Hughes]

Coincidentally I just wrote another fin function:

inductive xfin : ℕ → Type
| zero : ∀ n, xfin (nat.succ n)
| succ : ∀ n, xfin n → xfin (nat.succ n)

Isn't that fin2?

[Kevin Buzzard]

Oh maybe. I never think about these things; as far as I'm concerned we have a term of type equiv (fin n) (xfin n) so they're the same. I've never heard of fin2 I don't think.

[Kevin Buzzard]

Obviously number_theory/dioph.lean is the natural place to put that fundamental construction ;-)

[Kevin Buzzard]

I got the definition from Leroy's lecture.

[Mario Carneiro]

We should incorporate fin2 and vector2 in a better way. They are indeed rewritten every once in a while

[Mario Carneiro]

Re: fin.find, I don't think there is a way to write it in terms of nat.find without the bounds check. You will probably have to write your own version, but actually it's a lot easier when you have an upper bound on the witness already

[Floris van Doorn]

We should incorporate fin2 and vector2 in a better way. They are indeed rewritten every once in a while

vector2 does not exist in mathlib. The file data.vector2 just adds some stuff about ordinary vectors (presumably the name is to avoid a nameclash with data.vector in core).

[Mario Carneiro]

right, hence the need for better integration

[Mario Carneiro]

I have held to the position that the definition doesn't matter as long as we have an appropriate interface, but the equation compiler cares so it's tricky to completely make defeq stuff go away