mathlib documentation

tactic.elementwise

Tools to reformulate category-theoretic lemmas in concrete categories #

The elementwise attribute #

The elementwise attribute can be applied to a lemma

@[elementwise]
lemma some_lemma {C : Type*} [category C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...

and will produce

lemma some_lemma_apply {C : Type*} [category C] [concrete_category C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) (x : X) : g (f x) = h x := ...

Here X is being coerced to a type via concrete_category.has_coe_to_sort and f, g, and h are being coerced to functions via concrete_category.has_coe_to_fun. Further, we simplify the type using concrete_category.coe_id : ((𝟙 X) : X → X) x = x and concrete_category.coe_comp : (f ≫ g) x = g (f x), replacing morphism composition with function composition.

The name of the produced lemma can be specified with @[elementwise other_lemma_name]. If simp is added first, the generated lemma will also have the simp attribute.

Implementation #

This closely follows the implementation of the @[reassoc] attribute, due to Simon Hudon. Thanks to Gabriel Ebner for help diagnosing universe issues.

source
meta def tactic.extract_category  :
expr → tactic expr

From an expression f = g, where f g : X ⟶ Y for some objects X Y : V with [S : category V], extract the expression for S.

source
meta def tactic.prove_elementwise (h : expr) :
tactic (expr × expr × option name)

(internals for @[elementwise]) Given a lemma of the form f = g, where f g : X ⟶ Y and X Y : V, proves a new lemma of the form ∀ (x : X), f x = g x if we are already in a concrete category, or ∀ [concrete_category.{w} V] (x : X), f x = g x otherwise.

Returns the type and proof of this lemma, and the universe parameter w for the concrete_category instance, if it was not synthesized.

source
meta def tactic.elementwise_lemma (n : name) (n' : name := n.append_suffix "_apply") :
tactic unit

(implementation for @[elementwise]) Given a declaration named n of the form ∀ ..., f = g, proves a new lemma named n' of the form ∀ ... [concrete_category V] (x : X), f x = g x.

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

The elementwise attribute can be applied to a lemma

@[elementwise]
lemma some_lemma {C : Type*} [category C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) : f ≫ g = h := ...

and will produce

lemma some_lemma_apply {C : Type*} [category C] [concrete_category C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : X ⟶ Z) (w : ...) (x : X) : g (f x) = h x := ...

Here X is being coerced to a type via concrete_category.has_coe_to_sort and f, g, and h are being coerced to functions via concrete_category.has_coe_to_fun. Further, we simplify the type using concrete_category.coe_id : ((𝟙 X) : X → X) x = x and concrete_category.coe_comp : (f ≫ g) x = g (f x), replacing morphism composition with function composition.

The [concrete_category C] argument will be omitted if it is possible to synthesize an instance.

The name of the produced lemma can be specified with @[elementwise other_lemma_name]. If simp is added first, the generated lemma will also have the simp attribute.

source
meta def tactic.interactive.elementwise (del : interactive.parse (lean.parser.tk "!")?) (ns : interactive.parse lean.parser.ident*) :
tactic unit

elementwise h, for assumption w : ∀ ..., f ≫ g = h, creates a new assumption w : ∀ ... (x : X), g (f x) = h x.

elementwise! h, does the same but deletes the initial h assumption. (You can also add the attribute @[elementwise] to lemmas to generate new declarations generalized in this way.)

source
meta def tactic.derive_elementwise_proof  :
tactic unit

Auxiliary definition for category_theory.elementwise_of.

source
theorem category_theory.elementwise_of {α : Sort u_1} (hh : α) {β : Prop} (x : tactic.calculated_Prop β hh . "derive_elementwise_proof") :
β

With w : ∀ ..., f ≫ g = h (with universal quantifiers tolerated), elementwise_of w : ∀ ... (x : X), g (f x) = h x.

The type and proof of elementwise_of h is generated by tactic.derive_elementwise_proof which makes elementwise_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 (M N K : Mon.{u}) (f : M ⟶ N) (g : N ⟶ K) (h : M ⟶ K) (w : f ≫ g = h) (m : M) :
  g (f m) = h m :=
begin
  rw elementwise_of w,
end