Zulip Chat Archive

Stream: general

Topic: f circ g = h or forall x, f (g x) = h x?


view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:05):

I am constantly proving that various functions are equal because they are both the unique function with some property. A lot of my proofs naturally prove f circ g = h. However Kenny often writes such goals as forall x, f (g x) = h x. Normally in Lean I would prove f circ g = h by applying funext and then intro x. However in the kind of mathematics I'm currently doing this is not the way to prove things -- in fact I hardly ever get my hands dirty with explicit terms, I'm just chasing around universal properties.

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:06):

Kenny set up a structure with things like function.left_inverse g f and function.right_inverse g f and I had assumed these would unravel to g circ f = id etc but even these core functions evaluate to forall x, g (f x) = x

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:07):

The left inverse thing is convenient because that way you can write function.left_inverse g f x

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:07):

What's a nice convenient way to deduce "forall x, g (f x) = h x" from "g circ f = h" ? I keep having to enter tactic mode and then rewriting the goal with rw, and usually rw \l.

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:08):

Is there a proof of g circ f = h -> forall x, g (f x) = h x?

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:08):

I am using it all the time

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:08):

then make it a lemma

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:09):

fair do's

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:09):

what's it called?

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:09):

it's a bit too specific for my taste, but if you fold it in with one of your definitions I'm sure it will work well

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:09):

I think what I'd rather do is to rewrite all the definitions which we have which involve the x

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:10):

however I am concerned that end users might need the "explicit" versions

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:10):

then have a special constructor for your more user-facing theorems that accepts the explicit version

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:10):

I don't understand this

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:10):

I would make that lemma a biconditional BTW, you will want both directions

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:10):

I know that 9 times out of 10 when i'm trying to prove f = g the first thing I do is apply funext

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:11):

but here it's never true

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:11):

My initial thought on this is to use functions, you are basically doing category theory lite

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:11):

right

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

I don't care about my actual definition of a localised ring

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

all I ever use is the universal property

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

which is a real relief

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

because the localised ring is a quotient type

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

and they are awkward to use

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:12):

So when do you actually need the x?

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:12):

no idea

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:13):

I am not sure I do

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:13):

At the very least you have some notion of a "user" that will use one of the theorems and prove a hypothesis by funext

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:13):

which theorems are most likely candidates for this?

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:13):

I am not sure I have a clear notion of a user

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:13):

I think I am the only user at the minute

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:14):

hence the quotes

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:14):

Maybe if Kenny does more exercises in Atiyah-Macdonald he'll become another user

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:14):

Maybe I'll just rip out all the x's.

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:14):

or maybe your theorem has a conclusion that is a function equality, and the mythical user wants to congr_fun that equality

view this post on Zulip Mario Carneiro (Apr 22 2018 at 23:15):

you should identify the most outward-facing of your theorems and make them as pleasant to use as you can

view this post on Zulip Kevin Buzzard (Apr 22 2018 at 23:22):

This exercise (wanting a theory of localization because I have a use for it, but asking Kenny to prove the theorems) has really clarified for me how this whole process of writing a library works.

view this post on Zulip Patrick Massot (Apr 23 2018 at 07:57):

by applying funext and then intro x

Side remark: you can write funext x instead of funext, intro x. Soon you'll even be able to write ext x without thinking about whether you deal with an actual function or any other object for which extensionality makes sense


Last updated: May 10 2021 at 00:31 UTC