Function product

Stream: maths

[Sebastien Gouezel]

I can't find the name of the direct product of two functions. Is it defined somewhere in mathlib?

[Kenny Lau]

what does that mean?

[Johan Commelin]

I guess: given f : X1 → X2 and g : Y1 → Y2 you form (f,g) : X1 × Y1 → X2 × Y2.

[Kenny Lau]

the category theorist comes

[Kenny Lau]

anyway in that case it's probably shortest just to define it manually

[Sebastien Gouezel]

Yes, sorry, that's what I mean. And no, I am definitely not a category theorist :) Of course it can be defined by hand as a lambda, but there are potentially many useful simp lemmas about ranges, preimages and so on for this kind of objects. And it shows up often. So I was gessing it should have a name somewhere in mathlib. Otherwise, I will just use the plain lambda.

[Johan Commelin]

I guess that initially products where avoided as much as possible...

[Johan Commelin]

But Patrick has recently also been needing them.

[Johan Commelin]

So I guess that the API is lacking a bit, but that there might be good reason to develop it.

[Johan Commelin]

I'm not saying you should do that. It might be a nice project for a beginner. Maybe we should file it in a github issue.

[Patrick Massot]

The variant I needed was prod.mk which is already in core (but with the wrong definition).

[Alistair Tucker]

prod.map?
https://github.com/leanprover/lean/blob/ceacfa7445953cbc8860ddabc55407430a9ca5c3/library/init/data/prod.lean#L45
https://github.com/leanprover-community/mathlib/blob/60efaec1b2bae0b6ff22ebd889f26606c8648924/src/data/prod.lean#L19

[Sebastien Gouezel]

Thanks!

[Sebastien Gouezel]

Except that the definition is bad as prod.map f g p is not defeq to (f (p.fst), g (p.snd)). Indeed, it is defined as

def {u₁ u₂ v₁ v₂} prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
| (a, b) := (f a, g b)

which unfolds to something in terms of prod.cases_on. And it is in core...

[Alistair Tucker]

I'm not sure what defeq means, but I remember that before I could use actually prod.map I had to write map_def:
https://github.com/leanprover-community/mathlib/blob/60efaec1b2bae0b6ff22ebd889f26606c8648924/src/data/prod.lean#L36

[Kenny Lau]

just PR core :P

[Sebastien Gouezel]

Yes, that's the way it should be defined. Otherwise, it makes things pointlessly painful. For my use case, direct definition with lambda turns out to be better because of this problem in the definition.

[Patrick Massot]

The file I have in front of me starts with

def prod.map' {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*}
  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂ := λ p : α₁ × β₁, ⟨f p.1, g p.2⟩

local infix `⨯`:90 := prod.map'

[Kevin Buzzard]

@Alistair Tucker

I'm not sure what defeq means, but I remember that before I could use actually prod.map I had to write map_def:
https://github.com/leanprover-community/mathlib/blob/60efaec1b2bae0b6ff22ebd889f26606c8648924/src/data/prod.lean#L36

I could never follow these conversations about this sort of thing, for months and months. And the problem was precisely because I didn't know what definitional equality (defeq) meant. The idea is that sometimes you can prove X = Y by rfl, and sometimes you can't -- sometimes it's a theorem. For example if we define addition on the naturals by a+0:=a and a+S(b):=S(a+b) then x+0=x is true by definition, whereas to prove 0+x=x you need to use induction on x. In the first example, if you simplify both things as much as you can, then you get x=x. Whereas 0+x cannot be simplified; you have to split into the cases x=0 and x=successor before you can simplify the term further (so basically you have to apply the function nat.rec). So 0+x=x but this is not true by definition; the terms are not defeq.

Definitional equality is a super-powerful concept. I've proved [huge term] = [huge term] by rfl before. After a while it gets quite addictive -- if you make your definitions just right then there's more of a chance that rfl will work.

The problem with

def {u₁ u₂ v₁ v₂} prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
  (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
| (a, b) := (f a, g b)

is that the definition is by cases -- like the definition of 0 + x. So prod.map f g x is never going to be defeq to anything other than more complicated things which reduce to it; you can't reduce it any further. The moment you say "well x has type alpha x beta so WLOG it's of the form (a,b)" you are applying a function, probably called something like prod.map.rec or prod.map.cases_on, and changing the term.
This can be avoided by defining prod.map f g x to be (f x.fst, g x.snd). Now we don't have to do cases on x, these things are equal by definition.