Reformulate category-theoretic axioms in a more associativity-friendly way.
The reassoc attribute can be applied to a lemma
@[reassoc]
lemma some_lemma : foo ≫ bar = baz := ...
and produce
lemma some_lemma_assoc {Y : C} (f : X ⟶ Y) : foo ≫ bar ≫ f = baz ≫ f := ...
The name of the produced lemma can be specified with @[reassoc other_lemma_name]. If simp is added first, the generated lemma will also have the simp attribute.
When declaring a class of categories, the axioms can be reformulated to be more amenable to manipulation in right associated expressions:
class some_class (C : Type) [category C] :=
(foo : Π X : C, X ⟶ X)
(bar : ∀ {X Y : C} (f : X ⟶ Y), foo X ≫ f = f ≫ foo Y)
reassoc_axiom some_class.bar
Here too, the reassoc attribute can be used instead. It works well when combined with simp:
attribute [simp, reassoc] some_class.bar
From an expression f ≫ g, extract the expression representing the category instance.
(internals for @[reassoc]) Given a lemma of the form f ≫ g = h, proves a new lemma of the form h : ∀ {W} (k), f ≫ (g ≫ k) = h ≫ k, and returns the type and proof of this lemma.
(implementation for @[reassoc]) Given a declaration named n of the form f ≫ g = h, proves a new lemma named n' of the form ∀ {W} (k), f ≫ (g ≫ k) = h ≫ k.
On the following lemma:
@[reassoc]
lemma foo_bar : foo ≫ bar = foo := ...
generates
lemma foo_bar_assoc {Z} {x : Y ⟶ Z} : foo ≫ bar ≫ x = foo ≫ x := ...
The name of foo_bar_assoc can also be selected with @[reassoc new_name]
reassoc_axiom my_axiom
produces the lemma my_axiom_assoc which transforms a statement of the form x ≫ y = z into x ≫ y ≫ k = z ≫ k.
reassoc h, for assumption h : x ≫ y = z, creates a new assumption h : ∀ {W} (f : Z ⟶ W), x ≫ y ≫ f = z ≫ f. reassoc! h, does the same but deletes the initial h assumption. (You can also add the attribute @[reassoc] to lemmas to generate new declarations generalized in this way.)
With h : x ≫ y ≫ z = x (with universal quantifiers tolerated), reassoc_of h : ∀ {X'} (f : W ⟶ X'), x ≫ y ≫ z ≫ f = x ≫ f.
The type and proof of reassoc_of h is generated by tactic.derive_reassoc_proof which make reassoc_of meta-programming adjacent. It is not called as a tactic but as an expression. The goal is to avoid creating assumptions to dismiss after one use:
example (X Y Z W : C) (x : X ⟶ Y) (y : Y ⟶ Z) (z z' : Z ⟶ W) (w : X ⟶ Z)
(h : x ≫ y = w)
(h' : y ≫ z = y ≫ z') :
x ≫ y ≫ z = w ≫ z' :=
begin
rw [h',reassoc_of h],
end