|
| 1 | +/- |
| 2 | +Copyright (c) 2019 Simon Hudon. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Author(s): Simon Hudon |
| 5 | +-/ |
| 6 | +import category_theory.category |
| 7 | + |
| 8 | +/-! |
| 9 | +Reformulate category-theoretic axioms in a more associativity-friendly way. |
| 10 | +
|
| 11 | +## The `reassoc` attribute |
| 12 | +
|
| 13 | +The `reassoc` attribute can be applied to a lemma |
| 14 | +
|
| 15 | +```lean |
| 16 | +@[reassoc] |
| 17 | +lemma some_lemma : foo ≫ bar = baz := ... |
| 18 | +``` |
| 19 | +
|
| 20 | +and produce |
| 21 | +
|
| 22 | +```lean |
| 23 | +lemma some_lemma_assoc {Y : C} (f : X ⟶ Y) : foo ≫ bar ≫ f = baz ≫ f := ... |
| 24 | +``` |
| 25 | +
|
| 26 | +The name of the produced lemma can be specified with `@[reassoc other_lemma_name]`. If |
| 27 | +`simp` is added first, the generated lemma will also have the `simp` attribute. |
| 28 | +
|
| 29 | +## The `reassoc_axiom` command |
| 30 | +
|
| 31 | +When declaring a class of categories, the axioms can be reformulated to be more amenable |
| 32 | +to manipulation in right associated expressions: |
| 33 | +
|
| 34 | +``` |
| 35 | +class some_class (C : Type) [category C] := |
| 36 | +(foo : Π X : C, X ⟶ X) |
| 37 | +(bar : ∀ {X Y : C} (f : X ⟶ Y), foo X ≫ f = f ≫ foo Y) |
| 38 | +
|
| 39 | +reassoc_axiom some_class.bar |
| 40 | +``` |
| 41 | +
|
| 42 | +Here too, the `reassoc` attribute can be used instead. It works well when combined with |
| 43 | +`simp`: |
| 44 | +
|
| 45 | +``` |
| 46 | +attribute [simp, reassoc] some_class.bar |
| 47 | +``` |
| 48 | +-/ |
| 49 | + |
| 50 | +namespace tactic |
| 51 | + |
| 52 | +open interactive lean.parser category_theory |
| 53 | + |
| 54 | +meta def reassoc_axiom (n : name) (n' : name := n.append_suffix "_assoc") : tactic unit := |
| 55 | +do d ← get_decl n, |
| 56 | + let ls := d.univ_params.map level.param, |
| 57 | + let c := @expr.const tt n ls, |
| 58 | + (vs,t) ← infer_type c >>= mk_local_pis, |
| 59 | + (vs',t) ← whnf t >>= mk_local_pis, |
| 60 | + let vs := vs ++ vs', |
| 61 | + (lhs,rhs) ← match_eq t, |
| 62 | + `(@category_struct.comp _ %%struct_inst _ _ _ _ _) ← pure lhs, |
| 63 | + `(@has_hom.hom _ %%hom_inst %%X %%Y) ← infer_type lhs, |
| 64 | + C ← infer_type X, |
| 65 | + X' ← mk_local' `X' binder_info.implicit C, |
| 66 | + ft ← to_expr ``(@has_hom.hom _ %%hom_inst %%Y %%X'), |
| 67 | + f' ← mk_local_def `f' ft, |
| 68 | + t' ← to_expr ``(@category_struct.comp _ %%struct_inst _ _ _%%lhs %%f' = @category_struct.comp _ %%struct_inst _ _ _ %%rhs %%f'), |
| 69 | + let c' := c.mk_app vs, |
| 70 | + (_,pr) ← solve_aux t' (rewrite_target c'; reflexivity), |
| 71 | + pr ← instantiate_mvars pr, |
| 72 | + let s := simp_lemmas.mk, |
| 73 | + s ← s.add_simp ``category.assoc, |
| 74 | + s ← s.add_simp ``category.id_comp, |
| 75 | + s ← s.add_simp ``category.comp_id, |
| 76 | + (t'',pr') ← simplify s [] t', |
| 77 | + pr' ← mk_eq_mp pr' pr, |
| 78 | + t'' ← pis (vs ++ [X',f']) t'', |
| 79 | + pr' ← lambdas (vs ++ [X',f']) pr', |
| 80 | + add_decl $ declaration.thm n' d.univ_params t'' (pure pr'), |
| 81 | + copy_attribute `simp n tt n' |
| 82 | + |
| 83 | +/-- |
| 84 | +On the following lemma: |
| 85 | +``` |
| 86 | +@[reassoc] |
| 87 | +lemma foo_bar : foo ≫ bar = foo := ... |
| 88 | +``` |
| 89 | +generates |
| 90 | +
|
| 91 | +``` |
| 92 | +lemma foo_bar_assoc {Z} {x : Y ⟶ Z} : foo ≫ bar ≫ x = foo ≫ x := ... |
| 93 | +``` |
| 94 | +
|
| 95 | +The name of `foo_bar_assoc` can also be selected with @[reassoc new_name] |
| 96 | +-/ |
| 97 | +@[user_attribute] |
| 98 | +meta def reassoc_attr : user_attribute unit (option name) := |
| 99 | +{ name := `reassoc, |
| 100 | + descr := "create a companion lemma for associativity-aware rewriting", |
| 101 | + parser := optional ident, |
| 102 | + after_set := some (λ n _ _, |
| 103 | + do some n' ← reassoc_attr.get_param n | reassoc_axiom n, |
| 104 | + reassoc_axiom n $ n.get_prefix ++ n' ) } |
| 105 | + |
| 106 | +/-- |
| 107 | +``` |
| 108 | +reassoc_axiom my_axiom |
| 109 | +``` |
| 110 | +
|
| 111 | +produces the lemma `my_axiom_assoc` which transforms a statement of the |
| 112 | +form `x ≫ y = z` into `x ≫ y ≫ k = z ≫ k`. |
| 113 | +-/ |
| 114 | +@[user_command] |
| 115 | +meta def reassoc_cmd (_ : parse $ tk "reassoc_axiom") : lean.parser unit := |
| 116 | +do n ← ident, |
| 117 | + of_tactic' $ |
| 118 | + do n ← resolve_constant n, |
| 119 | + reassoc_axiom n |
| 120 | + |
| 121 | +end tactic |
0 commit comments