## Stream: general

### Topic: fin.find

#### Chris Hughes (Jun 28 2019 at 08:30):

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 (Jun 28 2019 at 09:10):

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 (Jun 28 2019 at 09:11):

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

#### Kevin Buzzard (Jun 28 2019 at 09:12):

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 (Jun 28 2019 at 09:14):

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 (Jun 28 2019 at 09:15):

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 (Jun 28 2019 at 09:17):

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

#### Kevin Buzzard (Jun 28 2019 at 09:17):

I got the definition from Leroy's lecture.

#### Mario Carneiro (Jun 28 2019 at 09:34):

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

#### Mario Carneiro (Jun 28 2019 at 09:40):

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 (Jul 01 2019 at 11:12):

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 (Jul 01 2019 at 12:30):

right, hence the need for better integration

#### Mario Carneiro (Jul 01 2019 at 12:32):

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

Last updated: May 13 2021 at 19:20 UTC