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

Stream: general

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

I am using it all the time

[Mario Carneiro]

then make it a lemma

[Kevin Buzzard]

fair do's

[Kevin Buzzard]

what's it called?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I don't understand this

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but here it's never true

[Mario Carneiro]

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

[Kevin Buzzard]

right

[Kevin Buzzard]

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

[Kevin Buzzard]

all I ever use is the universal property

[Kevin Buzzard]

which is a real relief

[Kevin Buzzard]

because the localised ring is a quotient type

[Kevin Buzzard]

and they are awkward to use

[Mario Carneiro]

So when do you actually need the x?

[Kevin Buzzard]

no idea

[Kevin Buzzard]

I am not sure I do

[Mario Carneiro]

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

[Mario Carneiro]

which theorems are most likely candidates for this?

[Kevin Buzzard]

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

[Kevin Buzzard]

I think I am the only user at the minute

[Mario Carneiro]

hence the quotes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Patrick Massot]

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