Zulip Chat Archive

Stream: general

Topic: list.prod

Kenny Lau (Jun 19 2018 at 23:30):

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

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?

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

Kenny Lau (Jun 19 2018 at 23:59):

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

Kenny Lau (Jun 20 2018 at 00:00):

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

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

Kenny Lau (Jun 20 2018 at 00:01):

how do I do that?

Simon Hudon (Jun 20 2018 at 00:01):

Do you use emacs and magit?

Kenny Lau (Jun 20 2018 at 00:02):

eh... not really

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

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

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

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.

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?

Gabriel Ebner (Jun 20 2018 at 13:35):

If you want to patch Lean, then yes.

Simon Hudon (Jun 20 2018 at 13:38):

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

Reid Barton (Jun 20 2018 at 14:18):

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

Simon Hudon (Jun 20 2018 at 14:22):

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

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.

Eric Wieser (Dec 09 2021 at 23:47):

I found myself wanting the foldr definition for #10674, as there the definitional equality is important. I ended up having to define a foldr version of sum there for my recursor's type to work

Eric Wieser (Dec 16 2021 at 12:33):

(xref #161 for reference)

Last updated: Dec 20 2023 at 11:08 UTC