Proposal: Triple

Stream: mathlib4

[Kenny Lau]

I propose the following definition:

universe u

structure Triple (α : Type u) : Type u where
  (fst : α)
  (snd : α)
  (thd : α)

The context is that when @David Ang was working with elliptic curves (which are defined with three coordinates x y z), he found that Fin 3 → R was a bit tricky to work with, and R × R × R while being better also had problems (mainly because of the idiom x.2.1 and x.2.2 instead of x.2 and x.3... so I propose Triple to solve this problem.

(I guess this doesn't have to be low in the hierarchy, I suppose David and I can just have this defined customly in the elliptic curve files.)

What do yall think?

[Kevin Buzzard]

Will this be useful for curves in $\mathbb{P}^2$ more generally?

[Damiano Testa]

Does α need to be the same for all three factors?

[Kenny Lau]

Kevin Buzzard said:

Will this be useful for curves in $\mathbb{P}^2$ more generally?

I'm doing experiments. I'll find out later.

[Kenny Lau]

Damiano Testa said:

Does α need to be the same for all three factors?

Maybe HTriple for that?

[Jireh Loreaux]

Maybe I'm wrong because it will be isolated enough (to elliptic curves), but this seems like a bad idea to me. All of a sudden you can't easily translate between α × α × α and this triple or Fin 3 → α and this triple (or you have to write dedicated API to do so). Basically anything you end up needing related to Prod you then have to duplicate for Triple. Why not just add some specialized API for Fin 3 → α (or α × α × α, whichever is used in elliptic curves)?

[Jireh Loreaux]

I think I saw a proposal to define foo.x, foo.y and foo.z for foo : α × β × γ. That seems reasonable.

[Jovan Gerbscheid]

I remember in Haskell, they have a separate tuple type for all the different sizes, which would lead to a lot of duplication. How about the following:

abbrev Tripple (α : Type*) := α × α × α

variable {α : Type*}

def Tripple.snd (t : Tripple α) : α := t.2.1
def Tripple.thd (t : Tripple α) : α := t.2.2

variable (t : Tripple α)

#check t.snd -- t.snd : α

[Jireh Loreaux]

Jovan Gerbscheid said:

I remember in Haskell, they have a separate tuple type for all the different sizes

This is because Haskell can't have Fin n (at least not without several language extensions which give you an approximation of dependent types).

[Jovan Gerbscheid]

Yes, that's true, but what I meant was that instead of writing α × β × γ as α × (β × γ) (which is also possible in Haskell), they have a separate "Tuple 3" to represent α × β × γ

[Jovan Gerbscheid]

My suggestion above keeps the advantages of using R × R × R, but replaces the idiom x.2.1 by x.snd and x.2.2 by x.thd.

[Edward van de Meent]

i'd just like to say that imo x.2.1 should basically never occur anyway, since writing x.snd.fst is more explicit about what's going on.

[Notification Bot]

53 messages were moved from this topic to #mathlib4 > bikeshed: mp and mpr by Johan Commelin.