Zulip Chat Archive

Stream: general

Topic: list.prod


view this post on Zulip Kenny Lau (Jun 19 2018 at 23:30):

Was there any point in time where list.prod [t] was definitionally equivalent to t * 1?

view this post on Zulip Kenny Lau (Jun 19 2018 at 23:57):

and was there any point in time where list.prod (x :: L) = x * list.prod L was rfl?

view this post on Zulip Simon Hudon (Jun 19 2018 at 23:59):

I think not. The foldl implementation is faster and Leo has been pretty aggressive with optimization from the start

view this post on Zulip Kenny Lau (Jun 19 2018 at 23:59):

interesting. my category repo seems to answer yes to my questions

view this post on Zulip Kenny Lau (Jun 20 2018 at 00:00):

i.e. a code worked some time ago, and now it doesn't

view this post on Zulip Simon Hudon (Jun 20 2018 at 00:00):

You can have an even clearer answer and use git blame on the definition of list.product

view this post on Zulip Kenny Lau (Jun 20 2018 at 00:01):

how do I do that?

view this post on Zulip Simon Hudon (Jun 20 2018 at 00:01):

Do you use emacs and magit?

view this post on Zulip Kenny Lau (Jun 20 2018 at 00:02):

eh... not really

view this post on Zulip Simon Hudon (Jun 20 2018 at 00:02):

You can get the instructions on using git blame by typing man git-blame in a terminal

view this post on Zulip Johan Commelin (Jun 20 2018 at 06:31):

Alternatively, you go to GitHub, and lookup the relevant line: https://github.com/leanprover/mathlib/blob/e1f795d0d929fa6b5458a04bd6bb5889e503b0bf/data/list/basic.lean#L1054
Then you click on the ... to the left of that line, and choose git blame. That gives you https://github.com/leanprover/mathlib/blob/e1f795d0d929fa6b5458a04bd6bb5889e503b0bf/data/list/basic.lean#L1054

view this post on Zulip Johan Commelin (Jun 20 2018 at 06:32):

But I don't see an easy option to walk through the history of that line. On the command line you can do that, with git log and some options. See also https://flummox-engineering.blogspot.com/2016/05/view-specific-lines-of-source-code-in-git-history.html

view this post on Zulip Johannes Hölzl (Jun 20 2018 at 13:24):

I traced it back, it was always foldl. I ported the definition from Lean2's library. I think we should change it to foldr then we get the expected equalities.

view this post on Zulip Simon Hudon (Jun 20 2018 at 13:35):

Is there a way to use foldr as the definition but run foldl implementation in the VM?

view this post on Zulip Gabriel Ebner (Jun 20 2018 at 13:35):

If you want to patch Lean, then yes.

view this post on Zulip Simon Hudon (Jun 20 2018 at 13:38):

That sounds less trivial than the "yes" suggests :stuck_out_tongue_closed_eyes:

view this post on Zulip Reid Barton (Jun 20 2018 at 14:18):

{-# RULES #-}with a proof obligation would be neat...

view this post on Zulip Simon Hudon (Jun 20 2018 at 14:22):

you could probably write it @[rule] before a lemma

view this post on Zulip Chris Hughes (Jun 20 2018 at 15:34):

and was there any point in time where list.prod (x :: L) = x * list.prod L was rfl?

I don't think it was even equal to that with non commutative multiplication, list.prod (x :: L) = list.prod L * xat the moment.


Last updated: May 12 2021 at 23:13 UTC