conv and associativity

Stream: maths

[Scott Morrison]

If any category theorists have recently been fighting with associativity, they might like the new conv tactic I just wrote:

/--
`slice` is a conv tactic; if the current focus is a composition of several morphisms,
`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.

Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
 -/

[Scott Morrison]

@Reid Barton, @Michael Jendrusch, @Johan Commelin in particular may like this.

[Scott Morrison]

It needs a better name, and perhaps to be generalised to an arbitrary associative operation ...

[Johan Commelin]

Hurray! That looks really cool. And yes, I wouldn't mind having this for groups and rings as well!

[Patrick Massot]

Oh yes, I already asked for this tactic in groups and rings

[Kevin Buzzard]

I was doing some basic binomial theorem stuff yesterday for the UGs and this would have been very convenient if it worked for + i.e. let me zoom into (a+b)+((c+d)+e)