is_X_hom

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

Would it be hard to write such a tactic?

[Scott Morrison]

Let's do it. :-)

[Scott Morrison]

First of all, however, note the following:

[Scott Morrison]

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

[Scott Morrison]

@[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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

Yep. Bundled homs make simp work

[Johan Commelin]

With linear_map and alg_hom this has been quite pleasant.

[Johan Commelin]

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]

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]

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

[Johan Commelin]

Bundling and mixing are fighting with each other...

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Anyway, that's something to think about later.

[Scott Morrison]

How would we write the hom tactic?

[Johan Commelin]

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]

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

[Patrick Massot]

Which is a stuff pushing tactic

[Johan Commelin]

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

[Scott Morrison]

do you mean local hypotheses that have an is_X_hom instance?

[Scott Morrison]

or just subexpressions of the goal?

[Johan Commelin]

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

[Scott Morrison]

either is doable

[Johan Commelin]

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

[Johan Commelin]

Maybe we need to infer it.

[Scott Morrison]

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

[Scott Morrison]

By the way, the following works:

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

[Johan Commelin]

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

[Scott Morrison]

Yes.

[Scott Morrison]

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

[Scott Morrison]

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

Cool. Let me grab a bigger screen.

[Kevin Buzzard]

How is this done in Coq?

[Kevin Buzzard]

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]

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]

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]

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]

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

[Mario Carneiro]

I think by apply_instance predates the other one

[Mario Carneiro]

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

[Mario Carneiro]

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

[Keeley Hoek]

Cool, good to know

[Sebastian Ullrich]

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

[Kevin Buzzard]

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]

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]

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