## Stream: general

### Topic: is_X_hom

#### Scott Morrison (Apr 09 2019 at 06:54):

Thanks, @Johan Commelin, for starting to clean these up in #911.

#### Scott Morrison (Apr 09 2019 at 06:55):

I've long been sad that is_ring_hom.map_one cannot be a simp lemma, because there's no fixed symbol for it to catch on.

#### Scott Morrison (Apr 09 2019 at 06:57):

For other lemmas, each map_mul and map_add, it's less clear that they should be simp lemmas. It depends whether you're trying to push all the ring homomorphisms down (in order to use ring, presumably), or pull them all up (hoping to get to a single homomorphism application).

#### Scott Morrison (Apr 09 2019 at 06:58):

We probably should have a tactic, however, for doing these rewrites.

#### Scott Morrison (Apr 09 2019 at 06:58):

I'm imagining hom by default would just push all homomorphisms down through algebraic operations.

#### Scott Morrison (Apr 09 2019 at 06:59):

It should probably take an argument, so for example hom ring would use the laws for ring homomorphisms.

#### Scott Morrison (Apr 09 2019 at 07:00):

An arrow might suffice for the mode where we want to pull the homomorphism out: either hom ← or hom ←monoid.

#### Johan Commelin (Apr 09 2019 at 07:00):

@Scott Morrison I think such a tactic is a very good idea.

#### Johan Commelin (Apr 09 2019 at 07:04):

Would it be hard to write such a tactic?

Let's do it. :-)

#### Scott Morrison (Apr 09 2019 at 07:04):

First of all, however, note the following:

#### Scott Morrison (Apr 09 2019 at 07:05):

the category theory library gives you an easy way to make these simp lemmas work with the simplifier directly! Observe the following:

#### Scott Morrison (Apr 09 2019 at 07:05):

@[simp] lemma map_mul {R S : Mon} (f : R ⟶ S) (x y : R) : f (x * y) = f x * f y :=
by rw is_monoid_hom.map_mul f

example {R S : Mon} (f : R ⟶ S) (x y : R) : f (x * y) = f x * f y :=
by simp --- Lo!


#### Scott Morrison (Apr 09 2019 at 07:06):

What's going on here? In (x y : R), R is being coerced automatically to its underlying type.

#### Scott Morrison (Apr 09 2019 at 07:06):

In f (x * y), the bundled ring morphism f is being coerced to its underlying function.

#### Scott Morrison (Apr 09 2019 at 07:06):

However, because the coercion is still sitting there, simp has something to hang on to now!

#### Johan Commelin (Apr 09 2019 at 07:07):

Yep. Bundled homs make simp work

#### Johan Commelin (Apr 09 2019 at 07:07):

With linear_map and alg_hom this has been quite pleasant.

#### Johan Commelin (Apr 09 2019 at 07:07):

The problem is that it seems to be non-trivial to make a bundled ring_hom also act as an add_group_hom and as a monoid_hom etc...

#### Scott Morrison (Apr 09 2019 at 07:08):

But really what I hope might happen is that everyone will stop talking about explicit functions, decorated is is_X_hom typeclasses, and just write R ⟶ S (with the \hom arrow)... :-)

#### Johan Commelin (Apr 09 2019 at 07:08):

Chris tried unification hints. That didn't work. I don't know if plain coercions would work...

#### Johan Commelin (Apr 09 2019 at 07:09):

Bundling and mixing are fighting with each other...

#### Scott Morrison (Apr 09 2019 at 07:09):

Can we define coercions along forget.obj and forget.map, for all the different forgetful functors?

#### Scott Morrison (Apr 09 2019 at 07:11):

(if they work, they could all be generated by @[derive] at the moment that each forget is defined)

#### Scott Morrison (Apr 09 2019 at 07:11):

Anyway, that's something to think about later.

#### Scott Morrison (Apr 09 2019 at 07:11):

How would we write the hom tactic?

#### Johan Commelin (Apr 09 2019 at 07:11):

Can we define coercions along forget.obj and forget.map, for all the different forgetful functors?

I've been meaning to experiment with that. But haven't had the time to do so yet.

#### Patrick Massot (Apr 09 2019 at 07:12):

I think you can take inspiration from https://github.com/leanprover-community/mathlib/commit/5fe470bb216e7b3fb6639d3b964c4eee36b88713

#### Patrick Massot (Apr 09 2019 at 07:12):

Which is a stuff pushing tactic

#### Johan Commelin (Apr 09 2019 at 07:15):

@Scott, how hard is it to gather all symbols from the context that have an is_X_hom instance?

#### Scott Morrison (Apr 09 2019 at 07:15):

do you mean local hypotheses that have an is_X_hom instance?

#### Scott Morrison (Apr 09 2019 at 07:16):

or just subexpressions of the goal?

#### Johan Commelin (Apr 09 2019 at 07:16):

I guess we only care about values of X in (add_) {semigroup, monoid, group}.

either is doable

#### Johan Commelin (Apr 09 2019 at 07:16):

The latter. The instance might not be a local hyp.

#### Johan Commelin (Apr 09 2019 at 07:16):

Maybe we need to infer it.

#### Scott Morrison (Apr 09 2019 at 07:17):

No -- the instance of course we'll find by inference. I was asking about the actual function.

#### Scott Morrison (Apr 09 2019 at 07:17):

By the way, the following works:

example (R S : CommRing) (f : R ⟶ S) : is_monoid_hom (f : R → S) := by apply_instance


#### Johan Commelin (Apr 09 2019 at 07:18):

After we have that list, we can start trying to erw (<-) along is_X_hom.map_Y the_symbol for Y in {zero, one, add, mul, pow, smul, gpow, sub, gsmul, gpow, sum, prod}.

Yes.

#### Scott Morrison (Apr 09 2019 at 07:19):

That example is an interesting combination of bundling and mixing getting along!

#### Scott Morrison (Apr 09 2019 at 07:19):

@Johan Commelin, do you want to try out the new VS Code live share mode and write this tactic? I have ~40 minutes now.

#### Johan Commelin (Apr 09 2019 at 07:20):

Cool. Let me grab a bigger screen.

#### Kevin Buzzard (Apr 09 2019 at 08:02):

How is this done in Coq?

#### Kevin Buzzard (Apr 09 2019 at 08:02):

I am spending the next few days with Gonthier but I do not understand the issues in this thread well enough to be able to ask him :-(

#### Kevin Buzzard (Apr 09 2019 at 08:03):

If people want to teach me, that would work. We could start with "there's no fixed symbol for it to catch on". I am already lost. I don't know how simp works and I don't know what a symbol is.

#### Scott Morrison (Apr 09 2019 at 08:59):

Johan, the code we wrote is on the hom-tactic branch. That was fun. :-) We need to write lots more porcelain, but the minimal plumbing is running!

#### Keeley Hoek (Apr 09 2019 at 10:54):

example (R S : CommRing) (f : R ⟶ S) : is_monoid_hom (f : R → S) := by apply_instance

(For my information) why does everyone do this instead of ... := infer_instance?

#### Johan Commelin (Apr 09 2019 at 10:56):

I've had cases where by apply_instance worked and infer_instance didn't. Don't remember the details though...

#### Mario Carneiro (Apr 09 2019 at 10:56):

I think by apply_instance predates the other one

#### Mario Carneiro (Apr 09 2019 at 10:57):

also infer_instance appears literally in the result term while by apply_instance only does instance search, just like inference for [] variables

#### Mario Carneiro (Apr 09 2019 at 10:58):

I think infer_instance is best used for #check and example things

#### Keeley Hoek (Apr 09 2019 at 10:59):

Cool, good to know

#### Sebastian Ullrich (Apr 09 2019 at 15:01):

I introduced infer_instance just so that I could use it before the tactic framework is defined

#### Kevin Buzzard (Apr 12 2019 at 19:28):

Here's a concrete example of what Mario is saying. I wanted to figure out where the category structure on opens X was coming from.

import category_theory.instances.Top.opens

open category_theory
open topological_space

variables (X : Type*) [topological_space X]

def XYZ : category (opens X) := by apply_instance
def ABC : category (opens X) := infer_instance
#print ABC -- useless
#print XYZ -- what I wanted to know i.e. category_theory.preorder_category
#check category_theory.preorder_category -- etc etc


#### Patrick Massot (Apr 12 2019 at 21:04):

Kevin, you do know the most efficient way would have been #check (by apply_instance : category \$ opens X) instance of this def/print dance right?

#### Kevin Buzzard (Apr 12 2019 at 23:02):

ha ha yes, I think Kenny showed me this trick once; I keep forgetting it.

Last updated: May 14 2021 at 22:15 UTC