Zulip Chat Archive

Stream: maths

Topic: Function product


view this post on Zulip Sebastien Gouezel (Jun 25 2019 at 19:30):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:32):

what does that mean?

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:34):

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

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:37):

the category theorist comes

view this post on Zulip Kenny Lau (Jun 25 2019 at 19:37):

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

view this post on Zulip Sebastien Gouezel (Jun 25 2019 at 19:39):

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.

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:45):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:46):

But Patrick has recently also been needing them.

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:46):

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

view this post on Zulip Johan Commelin (Jun 25 2019 at 19:46):

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.

view this post on Zulip Patrick Massot (Jun 25 2019 at 20:28):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 00:01):

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

view this post on Zulip Sebastien Gouezel (Jun 26 2019 at 06:21):

Thanks!

view this post on Zulip Sebastien Gouezel (Jun 26 2019 at 06:48):

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

view this post on Zulip Alistair Tucker (Jun 26 2019 at 07:52):

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

view this post on Zulip Kenny Lau (Jun 26 2019 at 08:19):

just PR core :P

view this post on Zulip Sebastien Gouezel (Jun 26 2019 at 09:07):

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.

view this post on Zulip Patrick Massot (Jun 26 2019 at 09:08):

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'

view this post on Zulip Kevin Buzzard (Jun 26 2019 at 10:33):

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



Last updated: May 12 2021 at 07:17 UTC