mathlib3 documentation

tactic.reassoc_axiom

Tools to reformulate category-theoretic axioms in a more associativity-friendly way #

The reassoc attribute #

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.

The reassoc_axiom command #

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
source
meta def tactic.get_cat_inst  :
expr → tactic expr

From an expression f ≫ g, extract the expression representing the category instance.

source
meta def tactic.prove_reassoc (h : expr) :
tactic (expr × expr)

(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.

source
meta def tactic.reassoc_axiom (n : name) (n' : name := n.append_suffix "_assoc") :
tactic unit

(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.

source
meta def tactic.reassoc_attr  :
user_attribute unit (option name)

The reassoc attribute can be applied to a lemma

@[reassoc]
lemma some_lemma : foo ≫ bar = baz := ...

to 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.

source
def tactic_doc.attribute.reassoc  :
tactic_doc_entry

The reassoc attribute can be applied to a lemma

@[reassoc]
lemma some_lemma : foo ≫ bar = baz := ...

to 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.

source
meta def tactic.reassoc_cmd (_x : interactive.parse (lean.parser.tk "reassoc_axiom")) :
lean.parser unit

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

The above will produce:

lemma some_class.bar_assoc {Z : C} (g : Y ⟶ Z) :
  foo X ≫ f ≫ g = f ≫ foo Y ≫ g := ...

Here too, the reassoc attribute can be used instead. It works well when combined with simp:

attribute [simp, reassoc] some_class.bar
source
def tactic_doc.command.reassoc_axiom  :
tactic_doc_entry

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

The above will produce:

lemma some_class.bar_assoc {Z : C} (g : Y ⟶ Z) :
  foo X ≫ f ≫ g = f ≫ foo Y ≫ g := ...

Here too, the reassoc attribute can be used instead. It works well when combined with simp:

attribute [simp, reassoc] some_class.bar
source
meta def tactic.interactive.reassoc (del : interactive.parse (optional (lean.parser.tk "!"))) (ns : interactive.parse (lean.parser.many lean.parser.ident)) :
tactic unit

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.)

source
def tactic.calculated_Prop {α : Sort u_1} (β : Prop) (hh : α) :
Prop
Equations
source
meta def tactic.derive_reassoc_proof  :
tactic unit
source
theorem category_theory.reassoc_of {α : Sort u_1} (hh : α) {β : Prop} (x : tactic.calculated_Prop β hh . "derive_reassoc_proof") :
β

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 that are dismissed 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
source
def tactic_doc.tactic.category_theory.reassoc_of  :
tactic_doc_entry

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 keeps complicated assumptions that are used only once or twice from polluting the local context.

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.

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.