Zulip Chat Archive

Stream: general

Topic: is_X_hom


view this post on Zulip Scott Morrison (Apr 09 2019 at 06:54):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Apr 09 2019 at 06:58):

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

view this post on Zulip Scott Morrison (Apr 09 2019 at 06:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:00):

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

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:04):

Would it be hard to write such a tactic?

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:04):

Let's do it. :-)

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:04):

First of all, however, note the following:

view this post on Zulip 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:

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:06):

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

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:06):

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

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:07):

Yep. Bundled homs make simp work

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:07):

With linear_map and alg_hom this has been quite pleasant.

view this post on Zulip 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...

view this post on Zulip 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)... :-)

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:09):

Bundling and mixing are fighting with each other...

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:09):

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

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:11):

Anyway, that's something to think about later.

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:11):

How would we write the hom tactic?

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Apr 09 2019 at 07:12):

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

view this post on Zulip Patrick Massot (Apr 09 2019 at 07:12):

Which is a stuff pushing tactic

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:15):

do you mean local hypotheses that have an is_X_hom instance?

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:16):

or just subexpressions of the goal?

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:16):

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

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:16):

either is doable

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:16):

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

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:16):

Maybe we need to infer it.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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}.

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:18):

Yes.

view this post on Zulip Scott Morrison (Apr 09 2019 at 07:19):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 09 2019 at 07:20):

Cool. Let me grab a bigger screen.

view this post on Zulip Kevin Buzzard (Apr 09 2019 at 08:02):

How is this done in Coq?

view this post on Zulip 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 :-(

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Apr 09 2019 at 10:56):

I think by apply_instance predates the other one

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2019 at 10:58):

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

view this post on Zulip Keeley Hoek (Apr 09 2019 at 10:59):

Cool, good to know

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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