Zulip Chat Archive

Stream: general

Topic: associativity


view this post on Zulip Simon Hudon (Jul 30 2018 at 02:50):

I'm writing a tactic about associativity and I'm inferring the associativity of the operators that appear in an expression. It turns out that this is the bottleneck of my script: building an instance of is_associative takes hundreds of ms. Is there a faster way to do it?

view this post on Zulip Kevin Buzzard (Jul 30 2018 at 07:47):

I hardly ever understand your questions Simon (too CS!), but I'd like to begin to try. Do you mean "type class inference is taking a long time checking that my random operation is associative"? You know better than I do that you can just make your own instance and add it to the type class inference system. It occurs to me that in contrast to simp, where I can look at traces, I don't really know how to look at what type class inference is doing. I don't want to derail this thread though.

view this post on Zulip Patrick Massot (Jul 30 2018 at 08:23):

Of course you know it: set_option trace.class_instances true

view this post on Zulip Patrick Massot (Jul 30 2018 at 08:23):

But you only think of it when things go wrong

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:12):

@Kevin Buzzard That's exactly it. It's not clear to me that adding instances would improve the situation

view this post on Zulip Reid Barton (Jul 30 2018 at 14:17):

Are you trying to infer the associativity of some operations which don't have is_associative instances? If so, could you give an example?

view this post on Zulip Reid Barton (Jul 30 2018 at 14:18):

Or is it instance lookup itself that takes a long time?

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:45):

Instance lookup is taking a really long lime. My work around right now is, the first time I need that information, I add it to the local assumptions and I keep looking at assumptions to see if it's there before calling mk_instance.

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:46):

The other idea I'm considering is to have an internal table where I cache that kind of information. That could be faster still and less intrusive but I would redo the instance inference at least once per call to the overall tactic (which I call assoc_rewrite)

view this post on Zulip Reid Barton (Jul 30 2018 at 14:48):

Whoa, assoc_rewrite! I need this more than you can possibly imagine.
How hard do you think it would be to make this work with category-style associativity, where the composition operator is indexed on the source and target types? I haven't looked at the implementation yet. I can probably rig up a representative example at some point if that would be helpful.

view this post on Zulip Reid Barton (Jul 30 2018 at 14:49):

I imagine it could involve internally needing a "thrist" rather than just a list, though maybe you can just ignore the type indices.

view this post on Zulip Reid Barton (Jul 30 2018 at 14:53):

Checking that a diagram in a category commutes usually comes down to these alternately reassociating and then rewriting arguments and when there are more than three morphisms involved it's a real pain to specify the reassociation you want.

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:53):

That is very good to know! I can consider categories. I don't think it would be too hard. Given a categorical composition operator, is there an analogue to is_associative to get me the associativity law?

view this post on Zulip Reid Barton (Jul 30 2018 at 14:54):

It's just a constant--a class method of category (category.associativity)

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:55):

Cool :) can you give me a proof example? I'll see if I can add it to my PR

view this post on Zulip Reid Barton (Jul 30 2018 at 14:56):

That is, my compositions are already written syntactically in terms of the fixed composition operator category.compose.

view this post on Zulip Reid Barton (Jul 30 2018 at 14:56):

Well, hmm. It might be a bit tricky, since categories are not in mathlib yet.

view this post on Zulip Reid Barton (Jul 30 2018 at 14:59):

I guess I'll give you a self-contained example, including the category class, for starters.

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:59):

Yeah, that's tricky. Are you working on a branch of mathlib? If so I could make a version for that. Alternatively, I could make a associativity attribute that you can put on that associativity law.

view this post on Zulip Simon Hudon (Jul 30 2018 at 14:59):

That's a good start.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:07):

Here is a simple, but very common sort of example: https://gist.github.com/rwbarton/b10c0229be25bd6880661afb2f1b32f5

view this post on Zulip Reid Barton (Jul 30 2018 at 15:08):

An associativity attribute would be a good solution for me.

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:15):

Cool! Thanks! With the associativity attribute, it would probably be enough to put it on the associativity law from semigroup and add_semigroup and semi_lattice, what do you think?

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:17):

From an aesthetic perspective, if you use x*y = a*b to rewrite p * x * y * q, do you prefer the tactic to leave the expression flat (i.e. p * a * b * q) or manipulated only minimally after rewrite (i.e. p * (a * b) * q)?

view this post on Zulip Reid Barton (Jul 30 2018 at 15:20):

If using an attribute is faster than instance lookup then that sounds like a good approach, since users can mark their own operations with the attribute anyways. I doubt we need the Prolog-style search power here. (I'm also wondering why instance synthesis is so slow, though.)

view this post on Zulip Reid Barton (Jul 30 2018 at 15:21):

Good question. Probably I can answer it better after trying it out in a few dozen proofs :slight_smile:

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:22):

What I'm suspecting that there are some dead alleys in the set of instances. Maybe I should start tracing the instance search process

view this post on Zulip Reid Barton (Jul 30 2018 at 15:22):

I think it usually won't matter for me, since I'd probably follow it with either more assoc_rws or simp, which applies associativity everywhere anyways.

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:23):

If you follow with simp, it might be more effective to flatten the expression so that simp doesn't waste time flattening it one associativity at a time.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:24):

BTW, when do I get assoc_simp? :)

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:25):

On Christmas if you've been a good boy ;-)

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:26):

Actually, I'd like to tackle simp as well but it seems like a bigger project.

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:26):

I'll keep you posted

view this post on Zulip Reid Barton (Jul 30 2018 at 15:26):

I have a way to deal with associativity in simp to some degree already, so it's not so bad. Actually it's stolen from @Scott Morrison's idea here: https://github.com/semorrison/lean-category-theory-pr/blob/lean-3.4.1/src/categories/isomorphism.lean#L34

view this post on Zulip Reid Barton (Jul 30 2018 at 15:27):

The general form is: if you have a @[simp] lemma which states that a * b = c * d * e, first generalize it to the form z * (a * b) = z * (c * d * e), and then reassociate the parentheses on the left side (there can be more than two original factors).

view this post on Zulip Reid Barton (Jul 30 2018 at 15:28):

Make that another simp lemma. Then you have a left-hand side of the form (z * a) * b = ... where z can be anything. So it will match any left-nested tree in which a and b appear "consecutively".

view this post on Zulip Reid Barton (Jul 30 2018 at 15:29):

(You can reassociate the parentheses on the right-hand side too, so that simp doesn't have to do it every time you apply the lemma.)

view this post on Zulip Reid Barton (Jul 30 2018 at 15:31):

This is like a Knuth-Bendix completion step: we could simplify z * (a * b) to either z * (c * d * e) or (z * a) * b, so add another rewrite rule to make those confluent.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:33):

So one wishlist item is an tactic/attribute to put on a simp lemma which will apply this transformation and make a new simp lemma.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:33):

I've done this by hand in a few cases, and it simplified some proofs.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:35):

But this is not by itself sufficient to deal with situations where we want to use hypotheses, rather than simp lemmas, like the equation e in my example earlier. That's why I still want assoc_rw for this situation. (Maybe an alternative is to generate a transformed version of the hypotheses, but I might also want to rewrite using equations tucked away inside fields of structures and things like that.)

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:35):

Ah I see! So assoc_simp would be better still I assume because then you wouldn't need to duplicate so many lemmas

view this post on Zulip Reid Barton (Jul 30 2018 at 15:37):

Right, I mean in general rw and simp are distinct, but overlapping in their uses, so both assoc_rw and assoc_simp ought to be useful as well.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:38):

Maybe assoc_simp with arguments could apply this transformation to those arguments, as well as all simp lemmas

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:43):

I was thinking of rewriting the simp tactic and changing the rewriting function so that it matches modulo associativity.

view this post on Zulip Reid Barton (Jul 30 2018 at 15:45):

Ah, I see. Sounds more ambitious, but probably more powerful as well.
Is simp in Lean? Maybe worth waiting for Lean 4?

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:45):

Where it gets tricky I find is when you have a lemma forall x, x * y = foo, you may instantiate x with a * b which is harder for my current matching to consider.

view this post on Zulip Simon Hudon (Jul 30 2018 at 15:46):

Ah, I see. Sounds more ambitious, but probably more powerful as well.
Is simp in Lean? Maybe worth waiting for Lean 4?

It might be. In any case, maybe I should first roll out assoc_rw and wait for feedback before getting started on assoc_simp

view this post on Zulip Simon Hudon (Jul 30 2018 at 16:14):

I think the category theory development looks beautiful, by the way. I wish I understood more of it

view this post on Zulip Scott Morrison (Jul 31 2018 at 02:08):

On the subject of associativity, there is something I would like to work on soon, but that I think it still orthogonal to rw_assoc and simp_assoc.

view this post on Zulip Scott Morrison (Jul 31 2018 at 02:09):

When working with monoidal categories, very often one has to insert associators (which are isomorphisms, not equations!) in order to be able to compose.

view this post on Zulip Scott Morrison (Jul 31 2018 at 02:15):

For example, if I have f : A -> (B ⊗ C) ⊗ D and g : B ⊗ (C ⊗ D) -> E, of course f ≫ g doesn't typecheck.

view this post on Zulip Scott Morrison (Jul 31 2018 at 02:17):

I would like to define some extra notation, e.g. f ⊗≫ g, which would invoke a tactic that inspects the target of f and the source of g, and decides if they are isomorphic via associator isomorphisms (probably also via identity isomorphisms, absorbing the monoidal unit on either side), and if so contructs that isomorphism α and returns f ≫ α ≫ g .

view this post on Zulip Scott Morrison (Jul 31 2018 at 02:18):

(By the axioms for monoidal categories, it doesn't matter _which_ associator isomorphism we use, as they are all equal.)

view this post on Zulip Simon Hudon (Jul 31 2018 at 03:45):

should there be an arrow in the type of g?

view this post on Zulip Simon Hudon (Jul 31 2018 at 03:49):

I think I see where you're going for. Similar logic to my assoc_rw tactic can be used to construct α

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:04):

@Reid Barton applying assoc_rw to categories is more complicated than I thought. It might be that I should just write a cat_rw specifically for categories. Is there any other context in which such a tactic would be useful or would it make sense to just refer to composition from category?

view this post on Zulip Mario Carneiro (Jul 31 2018 at 04:07):

a semigroupoid? :D

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:14):

:) Shouldn't that be an ancestor of category?

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:14):

I could hard-code semigroupoid composition instead of category composition, no?

view this post on Zulip Scott Morrison (Jul 31 2018 at 04:17):

I've heard the word semicategory, and there's actually some natural reasons to study them.

view this post on Zulip Scott Morrison (Jul 31 2018 at 04:17):

(Idempotent completion takes semicategories to categories, and in a certain sense is adjoint to the functor which forgets identities)

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:20):

Would it be worth introducing a has_comp type class?

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:24):

(I assume semicategories have an associative composition)

view this post on Zulip Mario Carneiro (Jul 31 2018 at 04:25):

I'm joking. I prefer to introduce concepts when they become useful and not before

view this post on Zulip Mario Carneiro (Jul 31 2018 at 04:26):

it's not hard to retrofit them if some time in the future we see a genuine semigroupoid which is not a category

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:27):

Fair enough :) my sense of usefulness for category theory still needs sharpening

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:29):

While we wait for the category theory stuff to be merged, would it be worth it to add has_comp to mathlib if I can use it in assoc_rw? That might facilitate the development of the category theory proofs.

view this post on Zulip Mario Carneiro (Jul 31 2018 at 04:43):

that sounds like it would be tied to a notation, but probably assoc_rw will need to be usable with at least a few notations, in particular +, *, and o

view this post on Zulip Simon Hudon (Jul 31 2018 at 04:45):

What I'm thinking is for operators with simpler types (e.g. +, *) I can rely on is_associative and then make a special case for categorical composition. The matching is a bit different anyway

view this post on Zulip Mario Carneiro (Jul 31 2018 at 05:09):

that sounds reasonable. I doubt categorical composition will use any other notation than whatever Scott is setting up

view this post on Zulip Patrick Massot (Jul 31 2018 at 10:06):

I also have something like Scott's associators everywhere in my group completion work. For every uniform space a, I have a complete Hausdorff completion a and a map from a to completion a, and every uniformly continuous map from a to b lifts to a map between completions. This is all fun. The trouble comes when product spaces are involved. I have an isomorphism from completion (a × b) tocompletion a × completion b, but I need to insert it and its inverse at a lot of places.

view this post on Zulip Reid Barton (Jul 31 2018 at 16:25):

Would it be worth introducing a has_comp type class?

Hmm, I wonder if moving to notation for a has_comp class would be viable, with an instance for function.comp... though I guess that is all in core Lean, so not viable at the moment.

view this post on Zulip Kevin Buzzard (Jul 31 2018 at 16:34):

Although this is even less under our control, is the correct long-term solution really to try and rethink how the actual type class system works? Or is the type class system some sort of standard machine which clearly will never change and we have to figure out how to work around it?

view this post on Zulip Johannes Hölzl (Jul 31 2018 at 18:37):

The mechanism will not change, at least there are no public plans for Lean 4 to change the type class mechanism. What will change, is the type class hierarchy. One thing is to move properties like commutativity, or zero_ne_one to be type class mixins, i.e. predicates over other type classes. [comm_ring A] will become [ring A] [is_commutative A (*)] (or similar). Also the lower type classes in the hierarcht like semigroups, monoid, etc, will be parameterized in their operators. This could eliminate parts of the additive / multiplicative split of the type class hierarchy.

view this post on Zulip Johan Commelin (Aug 01 2018 at 10:10):

Concerning Lean 4: in what time scales should I think about the release? 3 weeks, 3 months, 3 years, 3 decades? Is there any hope/expectation/statement about this?

view this post on Zulip Kevin Buzzard (Aug 01 2018 at 10:11):

"Not before the end of 2018" said Leo in Oxford IIRC

view this post on Zulip Kevin Buzzard (Aug 01 2018 at 10:11):

Maybe some of my students with better memories than me can confirm this

view this post on Zulip Johan Commelin (Aug 01 2018 at 10:13):

Ok. I didn't know anything at all. So if people said we would have to wait till at least 2025, I wouldn't have been surprised either.

view this post on Zulip Reid Barton (Aug 01 2018 at 18:03):

@Simon Hudon was there a question here left over from yesterday?
There isn't currently anything which generalizes category.compose nor any concrete plans to add such a thing.
I assume it would be easy to change assoc_rw later if this changes, anyways.

view this post on Zulip Reid Barton (Aug 01 2018 at 18:07):

By the way how do you feel about the name rw_assoc (and potentially simp_assoc) instead? Potentially more discoverable by autocompletion, for one

view this post on Zulip Simon Hudon (Aug 01 2018 at 18:34):

Yes you're right. The other thing that such a generalization helps with is separating the category code from the code of assoc_rw

view this post on Zulip Simon Hudon (Aug 01 2018 at 18:37):

I chose assoc_rw to conform with ac_refl. I think I could be convinced in favor of rw_assoc


Last updated: May 11 2021 at 21:10 UTC