Zulip Chat Archive

Stream: general

Topic: fin.find


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

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

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 09:11):

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

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

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

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

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 09:17):

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

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 09:17):

I got the definition from Leroy's lecture.

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

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

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

view this post on Zulip Mario Carneiro (Jul 01 2019 at 12:30):

right, hence the need for better integration

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