Zulip Chat Archive

Stream: general

Topic: tprod


view this post on Zulip Johan Commelin (Dec 16 2020 at 06:56):

there are currently two PRs that introduce tprod:

  • #5311 for indexed tensor products
  • #5385 for finite products of types

I don't have a strong opinion. But it would be good to resolve the conflict before merging.
cc: @Floris van Doorn @Frédéric Dupuis

view this post on Zulip Eric Wieser (Dec 16 2020 at 08:31):

tprod seems like a natural extension of tmul to me, so I'd favor letting 5311 keep the name and renaming the other.

view this post on Zulip Floris van Doorn (Dec 16 2020 at 10:09):

Ok, I'll rename it. How about typeprod? (I prefer a name without underscore, because I'm planning to have lemmas with names like typeprod_typeprod.)

view this post on Zulip Mario Carneiro (Dec 16 2020 at 10:11):

list.tprod?

view this post on Zulip Mario Carneiro (Dec 16 2020 at 10:12):

I would also like to see if we can avoid it entirely

view this post on Zulip Floris van Doorn (Dec 16 2020 at 20:30):

I'm happy with list.tprod, then I will also define set.tprod and measure.tprod.
I think this is the most convenient way to do things, see comment in #5385

view this post on Zulip Mario Carneiro (Dec 16 2020 at 20:32):

That seems fine to me, as long as the use is limited to these kind of proofs and isn't some new "vocabulary type" that we want to prove all sorts of things about

view this post on Zulip Yakov Pechersky (Dec 16 2020 at 20:39):

A question about #5385, defining using foldr places a punit at the end of the product. Why not a foldr1, so that the list of two elements is more directly equivalent to the regular Cartesian product, etc?

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:00):

that makes the inductive arguments more complicated, especially here where defeq is important

view this post on Zulip Mario Carneiro (Dec 16 2020 at 21:01):

using foldr1 would mean that pempty is either a special case or not included at all

view this post on Zulip Floris van Doorn (Dec 16 2020 at 22:57):

Indeed, I care more about simple proofs than a superfluous × punit, so I prefer foldr.


Last updated: May 11 2021 at 13:22 UTC