Ordered pair in type of result

Stream: general

[Praneeth Kolichala]

Let's say we have a function whose type is

def test (a : α) (b : β) (h : p a b) : p' (a, b) := sorry

Here, α and β are types, and p and p' have types α → β → Prop and α × β → Prop respectively.
The ordered pair (a, b) is in the product. This is a little annoying because c is not definitionally equal to (c.1, c.2).

Another way to write this function would be

def test' (c : α × β) (h : p c.1 c.2) : p' c := test c.1 c.2 h

Unfortunately, this definition of test' doesn't seem to work, because of the above problem with unifying c with (c.1, c.2).

On the other hand, it does work the other way around:

-- Everything type checks
def test' (c : α × β) (h : p c.1 c.2) : p' c := sorry
def test (a : α) (b : β) (h : p a b) : p' (a, b) := test' (a, b) h

Does this mean writing in the second format -- so that ordered pairs do not appear in types -- is preferable? Or is there an easy way to get from test to test'?

My use case is path.prod, which has type

def prod {a₁ b₁ : X} {a₂ b₂ : Y} (γ₁ : path a₁ b₁) (γ₂ : path a₂ b₂) : path (a₁, a₂) (b₁, b₂)

whereas I want to use it in a situation where the paths go from c₁.1 to c₂.1 and c₁.2 to c₂.2 for some c₁ and c₂.

Would it be preferable if the type was

def prod {c₁ c₂ : X × Y} (γ₁ : path c₁.1 c₂.1) (γ₂ : path c₁.2 c₂.2) : path c₁ c₂

[Eric Rodriguez]

can you make a mwe? it seems to me that everything should typecheck

[Praneeth Kolichala]

Here's a toy case that doesn't type check:

variables {α β : Type*} {p : α → β → Prop} {p' : α × β → Prop}
def test (a : α) (b : β) (h : p a b) : p' (a, b) := sorry
def test' (c : α × β) (h : p c.1 c.2) : p' c := test c.1 c.2 h

[Eric Rodriguez]

ahh, I see. I guess the "correct" way to do this is with the equation compiler:

variables {α β : Type*} {p : α → β → Prop} {p' : α × β → Prop}
def test (a : α) (b : β) (h : p a b) : p' (a, b) := sorry
def test' : ∀ (c : α × β) (h : p c.1 c.2), p' c
| (a, b) h := test _ _ h

but I'm really not sure what's preferrable

[Eric Rodriguez]

(or if you don't wanna mess with indices match and so on)

[Adam Topaz]

You can use the equation compiler, or since you have a prop, you can use tactic mode and case split your c.

[Adam Topaz]

Or you can switch to lean4 where c should be defeq to (c.fst,c.snd) (I think?)

[Eric Rodriguez]

woah, I didn't know we had eta in lean4!

[Eric Wieser]

If we do that's news to me. I thought we were just asking for it

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/262462713

[Reid Barton]

Praneeth Kolichala said:

Would it be preferable if the type was

def prod {c₁ c₂ : X × Y} (γ₁ : path c₁.1 c₂.1) (γ₂ : path c₁.2 c₂.2) : path c₁ c₂

I think so. You can also think of it as a backwards-style "how to build a path in a product of spaces", rather than a forwards-style "what can I do with a pair of paths".
If we indulge in a bit of free association, the type of docs#prod.ext is analogous.