Zulip Chat Archive

Stream: general

Topic: tprod

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

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.

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.)

Mario Carneiro (Dec 16 2020 at 10:11):


Mario Carneiro (Dec 16 2020 at 10:12):

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

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

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

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?

Mario Carneiro (Dec 16 2020 at 21:00):

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

Mario Carneiro (Dec 16 2020 at 21:01):

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

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: Dec 20 2023 at 11:08 UTC