feat(category_theory): add reassoc annotations

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[jcommelin]

Looks good to me... but I'm a metamateur...

[robertylewis]

Definitions need docstrings. What does this actually change? I'm surprised to see the attribute added with no proofs affected.

[semorrison]

Okay, my take on this PR is that the real content is a new tactic, [reassoc] which tweaks a given hypothesis so that it can be used even when things aren't associated correctly.

Along the way, the PR adds a handful of correct, harmless, not-immediately necessary @[reassoc] attributes on existing lemmas, and also correctly removes some unused arguments in other lemmas.

Under the hood, it does some refactoring (with no change in behaviour) of the machinery for creating reassoc lemmas.

@cipher1024, is this a correct summary? Have I missed anything?

[semorrison]

@cipher1024, I added some documentation suggestions, but I'll let you merge them if you like them.

[cipher1024]

Thanks!

[semorrison]

We also need some test cases. I'm not sure that the ! mode is useful enough to warrant adding.

[cipher1024]

I use it more than I don't use it. I must admit that I don't like keeping such a complicated assumption in my context though. Maybe I should try reworking it so that I can write rw [# h] where # creates a reassoc proof out h but without adding it to the context. That would work nicely with simp too.

[jcommelin]

Hi that sounds like fun (-; But I'm also worried a bit.
While really short and convenient it's also an incomprehensible sigil that really doesn't explain what's going on. Soon we will require beginners to have expertise in reading runes to decipher proofs...
Also... are you suggesting to generate the reassoc proof whenever it's needed? That seems like it will also be slower than the current situation.
My 2 cowry shells (-;

[cipher1024]

I don't think I would generate them whenever needed for lemmas, only assumptions. Here is an example where the notation is less cryptic:

namespace tactic

def Prop' {α} (β : Prop) (hh : α) := β

meta def foo_tac : tactic unit :=
do `(Prop' %%v %%h) ← target,
   (t,pr) ← prove_reassoc h,
   unify v t,
   exact pr

end tactic

def reassoc_of {α} (hh : α) {β} (x : tactic.Prop' β hh . tactic.foo_tac) : β := x

open category_theory
variables {C : Type} [category.{1} C]

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

[cipher1024]

(from experience, doing reassoc on an assumption gets really clunky and makes the context less readable; discarding it immediately seems simpler and more readable to me)

[jcommelin]

Aah, that seems nice.

[semorrison]

I like this example. What is the plan for this PR?

[cipher1024]

I think I would just merge it as is. What do you think @semorrison?