feat(category_theory): add reassoc annotations (#1558)

* feat(category_theory): add `reassoc` annotations

* Update reassoc_axiom.lean

* Update src/tactic/reassoc_axiom.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/reassoc_axiom.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/reassoc_axiom.lean

Co-Authored-By: Scott Morrison <scott@tqft.net>

* Update src/tactic/reassoc_axiom.lean

* Update src/tactic/reassoc_axiom.lean

* Update reassoc_axiom.lean

* Update tactics.lean

* Update tactics.md

* Update reassoc_axiom.lean

docs/tactics.md

@@ -1165,6 +1165,30 @@ Here too, the `reassoc` attribute can be used instead. It works well when combin
 ```lean
 attribute [simp, reassoc] some_class.bar
 ```
+
+### The reassoc_of function
+
+`reassoc_of h` takes local assumption `h` and add a ` ≫ f` term on the right of both sides of the equality.
+Instead of creating a new assumption from the result, `reassoc_of h` stands for the proof of that reassociated
+statement. This prevents poluting the local context with complicated assumptions used only once or twice.
+
+In the following, assumption `h` is needed in a reassociated form. Instead of proving it as a new goal and adding it as 
+an assumption, we use `reassoc_of h` as a rewrite rule which works just as well.
+
+```lean
+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
+  -- reassoc_of h : ∀ {X' : C} (f : W ⟶ X'), x ≫ y ≫ f = w ≫ f
+  rw [h',reassoc_of h],
+end
+```
+
+Although `reassoc_of` is not a tactic or a meta program, its type is generated 
+through meta-programming to make it usable inside normal expressions.
+
 ### lint
 User commands to spot common mistakes in the code
 

src/category_theory/comma.lean

@@ -208,7 +208,7 @@ by tidy
 @[simp] lemma comp_left (a b c : over X) (f : a ⟶ b) (g : b ⟶ c) :
   (f ≫ g).left = f.left ≫ g.left := rfl
 
-@[simp] lemma w {A B : over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom :=
+@[simp, reassoc] lemma w {A B : over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom :=
 by have := f.w; tidy
 
 def mk {X Y : T} (f : Y ⟶ X) : over X :=

src/category_theory/functor.lean

@@ -13,7 +13,7 @@ Introduces notations
     (I would like a better arrow here, unfortunately ⇒ (`\functor`) is taken by core.)
 -/
 
-import category_theory.category
+import category_theory.category tactic.reassoc_axiom
 
 namespace category_theory
 
@@ -41,7 +41,7 @@ infixr ` ⥤ `:26 := functor       -- type as \func --
 restate_axiom functor.map_id'
 attribute [simp] functor.map_id
 restate_axiom functor.map_comp'
-attribute [simp] functor.map_comp
+attribute [simp, reassoc] functor.map_comp
 
 namespace functor
 

src/tactic/reassoc_axiom.lean

@@ -51,22 +51,29 @@ namespace tactic
 
 open interactive lean.parser category_theory
 
-meta def reassoc_axiom (n : name) (n' : name := n.append_suffix "_assoc") : tactic unit :=
-do d ← get_decl n,
-   let ls := d.univ_params.map level.param,
-   let c := @expr.const tt n ls,
-   (vs,t) ← infer_type c >>= mk_local_pis,
+/-- From an expression `f ≫ g`, extract the expression representing the category instance. -/
+meta def get_cat_inst : expr → tactic expr
+| `(@category_struct.comp _ %%struct_inst _ _ _ _ _) := pure struct_inst
+| _ := failed
+
+/-- (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.
+-/
+meta def prove_reassoc (h : expr) : tactic (expr × expr) :=
+do
+   (vs,t) ← infer_type h >>= mk_local_pis,
    (vs',t) ← whnf t >>= mk_local_pis,
    let vs := vs ++ vs',
    (lhs,rhs) ← match_eq t,
-   `(@category_struct.comp _ %%struct_inst _ _ _ _ _) ← pure lhs,
+   struct_inst ← get_cat_inst lhs <|> get_cat_inst rhs <|> fail "no composition found in statement",
    `(@has_hom.hom _ %%hom_inst %%X %%Y) ← infer_type lhs,
    C ← infer_type X,
    X' ← mk_local' `X' binder_info.implicit C,
    ft ← to_expr ``(@has_hom.hom _ %%hom_inst %%Y %%X'),
    f' ← mk_local_def `f' ft,
    t' ← to_expr ``(@category_struct.comp _ %%struct_inst _ _ _%%lhs %%f' = @category_struct.comp _ %%struct_inst _ _ _ %%rhs %%f'),
-   let c' := c.mk_app vs,
+   let c' := h.mk_app vs,
    (_,pr) ← solve_aux t' (rewrite_target c'; reflexivity),
    pr ← instantiate_mvars pr,
    let s := simp_lemmas.mk,
@@ -77,6 +84,16 @@ do d ← get_decl n,
    pr' ← mk_eq_mp pr' pr,
    t'' ← pis (vs ++ [X',f']) t'',
    pr' ← lambdas (vs ++ [X',f']) pr',
+   pure (t'',pr')
+
+/-- (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`.
+-/
+meta def reassoc_axiom (n : name) (n' : name := n.append_suffix "_assoc") : tactic unit :=
+do d ← get_decl n,
+   let ls := d.univ_params.map level.param,
+   let c := @expr.const tt n ls,
+   (t'',pr') ← prove_reassoc c,
    add_decl $ declaration.thm n' d.univ_params t'' (pure pr'),
    copy_attribute `simp n tt n'
 
@@ -100,7 +117,7 @@ meta def reassoc_attr : user_attribute unit (option name) :=
   descr := "create a companion lemma for associativity-aware rewriting",
   parser := optional ident,
   after_set := some (λ n _ _,
-    do some n' ← reassoc_attr.get_param n | reassoc_axiom n,
+    do some n' ← reassoc_attr.get_param n | reassoc_axiom n (n.append_suffix "_assoc"),
        reassoc_axiom n $ n.get_prefix ++ n' ) }
 
 /--
@@ -118,4 +135,48 @@ do n ← ident,
    do n ← resolve_constant n,
       reassoc_axiom n
 
+namespace interactive
+
+setup_tactic_parser
+
+/-- `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.)
+-/
+meta def reassoc (del : parse (tk "!")?) (ns : parse ident*) : tactic unit :=
+do ns.mmap' (λ n,
+   do h ← get_local n,
+      (t,pr) ← prove_reassoc h,
+      assertv n t pr,
+      when del.is_some (tactic.clear h) )
+
+end interactive
+
+def calculated_Prop {α} (β : Prop) (hh : α) := β
+
+meta def derive_reassoc_proof : tactic unit :=
+do `(calculated_Prop %%v %%h) ← target,
+   (t,pr) ← prove_reassoc h,
+   unify v t,
+   exact pr
+
 end tactic
+
+/-- 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:
+    
+    ```lean
+    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
+    ```
+-/
+def category_theory.reassoc_of {α} (hh : α) {β} (x : tactic.calculated_Prop β hh . tactic.derive_reassoc_proof) : β := x

test/tactics.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Scott Morrison
 -/
 
-import tactic.interactive tactic.finish tactic.ext tactic.lift tactic.apply
+import tactic.interactive tactic.finish tactic.ext tactic.lift tactic.apply tactic.reassoc_axiom
 
 example (m n p q : nat) (h : m + n = p) : true :=
 begin
@@ -296,6 +296,20 @@ do
 -- run and succeed silently.
 test_parser1
 
+section category_theory
+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
+
+end category_theory
+
 section is_eta_expansion
 /- test the is_eta_expansion tactic -/
 open function tactic