feat(simps): allow the user to specify the projections (#1630)

* feat(simps): allow the user to specify the projections

Also add option to shorten generated lemma names
Add the attribute to more places in the category_theory library
The projection lemmas of inl_ and inr_ are now called inl__obj and similar

* use simps partially in limits/cones and whiskering

* revert whiskering

* rename last_name to short_name

* Update src/category_theory/products/basic.lean

* Update src/category_theory/limits/cones.lean

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

* Update src/category_theory/products/associator.lean

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

* Update src/data/string/defs.lean

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

* clarify is_eta_expansion docstrings

Author: fpvandoorn

docs/tactics.md

@@ -1175,7 +1175,7 @@ attribute [simp, reassoc] some_class.bar
 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 
+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
@@ -1189,7 +1189,7 @@ begin
 end
 ```
 
-Although `reassoc_of` is not a tactic or a meta program, its type is generated 
+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
@@ -1283,24 +1283,32 @@ See also additional documentation of `using_well_founded` in
 ### simps
 
 * The `@[simps]` attribute automatically derives lemmas specifying the projections of the declaration.
-* Example:
+* Example: (note that the forward and reverse functions are specified differently!)
   ```lean
-  @[simps] def refl (α) : α ≃ α := ⟨id, id, λ x, rfl, λ x, rfl⟩
+  @[simps] def refl (α) : α ≃ α := ⟨id, λ x, x, λ x, rfl, λ x, rfl⟩
   ```
   derives two simp-lemmas:
   ```lean
-  @[simp] lemma refl_to_fun (α) : (refl α).to_fun = id
-  @[simp] lemma refl_inv_fun (α) : (refl α).inv_fun = id
+  @[simp] lemma refl_to_fun (α) (x : α) : (refl α).to_fun x = id x
+  @[simp] lemma refl_inv_fun (α) (x : α) : (refl α).inv_fun x = x
   ```
 * It does not derive simp-lemmas for the prop-valued projections.
 * It will automatically reduce newly created beta-redexes, but not unfold any definitions.
 * If one of the fields itself is a structure, this command will recursively create
   simp-lemmas for all fields in that structure.
+* You can use `@[simps proj1 proj2 ...]` to only generate the projection lemmas for the specified
+  projections. For example:
+  ```lean
+  attribute [simps to_fun] refl
+  ```
 * If one of the values is an eta-expanded structure, we will eta-reduce this structure.
 * You can use `@[simps lemmas_only]` to derive the lemmas, but not mark them
   as simp-lemmas.
+* You can use `@[simps short_name]` to only use the name of the last projection for the name of the
+  generated lemmas.
+* The precise syntax is `('simps' 'lemmas_only'? 'short_name'? ident*)`.
 * If one of the projections is marked as a coercion, the generated lemmas do *not* use this
   coercion.
+* `@[simps]` reduces let-expressions where necessary.
 * If one of the fields is a partially applied constructor, we will eta-expand it
   (this likely never happens).
-* `@[simps]` reduces let-expressions where necessary.

src/category_theory/limits/cones.lean

@@ -377,46 +377,36 @@ namespace category_theory.limits
 
 variables {F : J ⥤ Cᵒᵖ}
 
-def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
+-- Here and below we only automatically generate the `@[simp]` lemma for the `X` field,
+-- as we can be a simpler `rfl` lemma for the components of the natural transformation by hand.
+@[simps X] def cone_of_cocone_left_op (c : cocone F.left_op) : cone F :=
 { X := op c.X,
   π := nat_trans.right_op (c.ι ≫ (const.op_obj_unop (op c.X)).hom) }
 
-@[simp] lemma cone_of_cocone_left_op_X (c : cocone F.left_op) :
-  (cone_of_cocone_left_op c).X = op c.X :=
-rfl
 @[simp] lemma cone_of_cocone_left_op_π_app (c : cocone F.left_op) (j) :
   (cone_of_cocone_left_op c).π.app j = (c.ι.app (op j)).op :=
 by { dsimp [cone_of_cocone_left_op], simp }
 
-def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
+@[simps X] def cocone_left_op_of_cone (c : cone F) : cocone (F.left_op) :=
 { X := unop c.X,
   ι := nat_trans.left_op c.π }
 
-@[simp] lemma cocone_left_op_of_cone_X (c : cone F) :
-  (cocone_left_op_of_cone c).X = unop c.X :=
-rfl
 @[simp] lemma cocone_left_op_of_cone_ι_app (c : cone F) (j) :
   (cocone_left_op_of_cone c).ι.app j = (c.π.app (unop j)).unop :=
 by { dsimp [cocone_left_op_of_cone], simp }
 
-def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
+@[simps X] def cocone_of_cone_left_op (c : cone F.left_op) : cocone F :=
 { X := op c.X,
   ι := nat_trans.right_op ((const.op_obj_unop (op c.X)).hom ≫ c.π) }
 
-@[simp] lemma cocone_of_cone_left_op_X (c : cone F.left_op) :
-  (cocone_of_cone_left_op c).X = op c.X :=
-rfl
 @[simp] lemma cocone_of_cone_left_op_ι_app (c : cone F.left_op) (j) :
   (cocone_of_cone_left_op c).ι.app j = (c.π.app (op j)).op :=
 by { dsimp [cocone_of_cone_left_op], simp }
 
-def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
+@[simps X] def cone_left_op_of_cocone (c : cocone F) : cone (F.left_op) :=
 { X := unop c.X,
   π := nat_trans.left_op c.ι }
 
-@[simp] lemma cone_left_op_of_cocone_X (c : cocone F) :
-  (cone_left_op_of_cocone c).X = unop c.X :=
-rfl
 @[simp] lemma cone_left_op_of_cocone_π_app (c : cocone F) (j) :
   (cone_left_op_of_cocone c).π.app j = (c.ι.app (unop j)).unop :=
 by { dsimp [cone_left_op_of_cocone], simp }

src/category_theory/products/associator.lean

@@ -20,28 +20,16 @@ variables (C : Type u₁) [𝒞 : category.{v₁} C]
           (E : Type u₃) [ℰ : category.{v₃} E]
 include 𝒞 𝒟 ℰ
 
-def associator : ((C × D) × E) ⥤ (C × (D × E)) :=
+-- Here and below we specify explicitly the projections to generate `@[simp]` lemmas for, 
+-- as the default behaviour of `@[simps]` will generate projections all the way down to components of pairs.
+@[simps obj map] def associator : ((C × D) × E) ⥤ (C × (D × E)) :=
 { obj := λ X, (X.1.1, (X.1.2, X.2)),
   map := λ _ _ f, (f.1.1, (f.1.2, f.2)) }
 
-@[simp] lemma associator_obj (X) :
-  (associator C D E).obj X = (X.1.1, (X.1.2, X.2)) :=
-rfl
-@[simp] lemma associator_map {X Y} (f : X ⟶ Y) :
-  (associator C D E).map f = (f.1.1, (f.1.2, f.2)) :=
-rfl
-
-def inverse_associator : (C × (D × E)) ⥤ ((C × D) × E) :=
+@[simps obj map] def inverse_associator : (C × (D × E)) ⥤ ((C × D) × E) :=
 { obj := λ X, ((X.1, X.2.1), X.2.2),
   map := λ _ _ f, ((f.1, f.2.1), f.2.2) }
 
-@[simp] lemma inverse_associator_obj (X) :
-  (inverse_associator C D E).obj X = ((X.1, X.2.1), X.2.2) :=
-rfl
-@[simp] lemma inverse_associator_map {X Y} (f : X ⟶ Y) :
-  (inverse_associator C D E).map f = ((f.1, f.2.1), f.2.2) :=
-rfl
-
 def associativity : (C × D) × E ≌ C × (D × E) :=
 equivalence.mk (associator C D E) (inverse_associator C D E)
   (nat_iso.of_components (λ X, eq_to_iso (by simp)) (by tidy))

src/category_theory/products/basic.lean

@@ -51,45 +51,32 @@ variables (C : Type u₁) [𝒞 : category.{v₁} C] (D : Type u₂) [𝒟 : cat
 include 𝒞 𝒟
 
 /-- `inl C Z` is the functor `X ↦ (X, Z)`. -/
-def inl (Z : D) : C ⥤ C × D :=
+-- Here and below we specify explicitly the projections to generate `@[simp]` lemmas for, 
+-- as the default behaviour of `@[simps]` will generate projections all the way down to components of pairs.
+@[simps obj map] def inl (Z : D) : C ⥤ C × D :=
 { obj := λ X, (X, Z),
   map := λ X Y f, (f, 𝟙 Z) }
 
-@[simp] lemma inl_obj (Z : D) (X : C) : (inl C D Z).obj X = (X, Z) := rfl
-@[simp] lemma inl_map (Z : D) {X Y : C} {f : X ⟶ Y} : (inl C D Z).map f = (f, 𝟙 Z) := rfl
-
 /-- `inr D Z` is the functor `X ↦ (Z, X)`. -/
-def inr (Z : C) : D ⥤ C × D :=
+@[simps obj map] def inr (Z : C) : D ⥤ C × D :=
 { obj := λ X, (Z, X),
   map := λ X Y f, (𝟙 Z, f) }
 
-@[simp] lemma inr_obj (Z : C) (X : D) : (inr C D Z).obj X = (Z, X) := rfl
-@[simp] lemma inr_map (Z : C) {X Y : D} {f : X ⟶ Y} : (inr C D Z).map f = (𝟙 Z, f) := rfl
-
 /-- `fst` is the functor `(X, Y) ↦ X`. -/
-def fst : C × D ⥤ C :=
+@[simps obj map] def fst : C × D ⥤ C :=
 { obj := λ X, X.1,
   map := λ X Y f, f.1 }
 
-@[simp] lemma fst_obj (X : C × D) : (fst C D).obj X = X.1 := rfl
-@[simp] lemma fst_map {X Y : C × D} {f : X ⟶ Y} : (fst C D).map f = f.1 := rfl
-
 /-- `snd` is the functor `(X, Y) ↦ Y`. -/
-def snd : C × D ⥤ D :=
+@[simps obj map] def snd : C × D ⥤ D :=
 { obj := λ X, X.2,
   map := λ X Y f, f.2 }
 
-@[simp] lemma snd_obj (X : C × D) : (snd C D).obj X = X.2 := rfl
-@[simp] lemma snd_map {X Y : C × D} {f : X ⟶ Y} : (snd C D).map f = f.2 := rfl
-
-def swap : C × D ⥤ D × C :=
+@[simps obj map] def swap : C × D ⥤ D × C :=
 { obj := λ X, (X.2, X.1),
   map := λ _ _ f, (f.2, f.1) }
 
-@[simp] lemma swap_obj (X : C × D) : (swap C D).obj X = (X.2, X.1) := rfl
-@[simp] lemma swap_map {X Y : C × D} {f : X ⟶ Y} : (swap C D).map f = (f.2, f.1) := rfl
-
-def symmetry : swap C D ⋙ swap D C ≅ 𝟭 (C × D) :=
+@[simps hom_app inv_app] def symmetry : swap C D ⋙ swap D C ≅ 𝟭 (C × D) :=
 { hom := { app := λ X, 𝟙 X },
   inv := { app := λ X, 𝟙 X } }
 
@@ -107,21 +94,15 @@ section
 variables (C : Type u₁) [𝒞 : category.{v₁} C] (D : Type u₂) [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
-def evaluation : C ⥤ (C ⥤ D) ⥤ D :=
+@[simps] def evaluation : C ⥤ (C ⥤ D) ⥤ D :=
 { obj := λ X,
   { obj := λ F, F.obj X,
     map := λ F G α, α.app X, },
   map := λ X Y f,
   { app := λ F, F.map f,
     naturality' := λ F G α, eq.symm (α.naturality f) } }
 
-@[simp] lemma evaluation_obj_obj (X) (F) : ((evaluation C D).obj X).obj F = F.obj X := rfl
-@[simp] lemma evaluation_obj_map (X) {F G} (α : F ⟶ G) :
-  ((evaluation C D).obj X).map α = α.app X := rfl
-@[simp] lemma evaluation_map_app {X Y} (f : X ⟶ Y) (F) :
-  ((evaluation C D).map f).app F = F.map f := rfl
-
-def evaluation_uncurried : C × (C ⥤ D) ⥤ D :=
+@[simps obj map] def evaluation_uncurried : C × (C ⥤ D) ⥤ D :=
 { obj := λ p, p.2.obj p.1,
   map := λ x y f, (x.2.map f.1) ≫ (f.2.app y.1),
   map_comp' := λ X Y Z f g,
@@ -132,10 +113,6 @@ def evaluation_uncurried : C × (C ⥤ D) ⥤ D :=
         category.assoc, nat_trans.naturality],
   end }
 
-@[simp] lemma evaluation_uncurried_obj (p) : (evaluation_uncurried C D).obj p = p.2.obj p.1 := rfl
-@[simp] lemma evaluation_uncurried_map {x y} (f : x ⟶ y) :
-  (evaluation_uncurried C D).map f = (x.2.map f.1) ≫ (f.2.app y.1) := rfl
-
 end
 
 variables {A : Type u₁} [𝒜 : category.{v₁} A]
@@ -146,23 +123,20 @@ include 𝒜 ℬ 𝒞 𝒟
 
 namespace functor
 /-- The cartesian product of two functors. -/
-def prod (F : A ⥤ B) (G : C ⥤ D) : A × C ⥤ B × D :=
+@[simps obj map] def prod (F : A ⥤ B) (G : C ⥤ D) : A × C ⥤ B × D :=
 { obj := λ X, (F.obj X.1, G.obj X.2),
   map := λ _ _ f, (F.map f.1, G.map f.2) }
 
 /- Because of limitations in Lean 3's handling of notations, we do not setup a notation `F × G`.
    You can use `F.prod G` as a "poor man's infix", or just write `functor.prod F G`. -/
 
-@[simp] lemma prod_obj (F : A ⥤ B) (G : C ⥤ D) (a : A) (c : C) :
-  (F.prod G).obj (a, c) = (F.obj a, G.obj c) := rfl
-@[simp] lemma prod_map (F : A ⥤ B) (G : C ⥤ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) :
-  (F.prod G).map f = (F.map f.1, G.map f.2) := rfl
 end functor
 
 namespace nat_trans
 
 /-- The cartesian product of two natural transformations. -/
-def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I :=
+@[simps app] def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) :
+  F.prod H ⟶ G.prod I :=
 { app         := λ X, (α.app X.1, β.app X.2),
   naturality' := λ X Y f,
   begin
@@ -174,8 +148,6 @@ def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod
 /- Again, it is inadvisable in Lean 3 to setup a notation `α × β`;
    use instead `α.prod β` or `nat_trans.prod α β`. -/
 
-@[simp] lemma prod_app  {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) (a : A) (c : C) :
-  (nat_trans.prod α β).app (a, c) = (α.app a, β.app c) := rfl
 end nat_trans
 
 end category_theory

src/category_theory/sums/basic.lean

@@ -55,21 +55,15 @@ include 𝒞 𝒟
 
 /-- `inl_` is the functor `X ↦ inl X`. -/
 -- Unfortunate naming here, suggestions welcome.
-def inl_ : C ⥤ C ⊕ D :=
+@[simps] def inl_ : C ⥤ C ⊕ D :=
 { obj := λ X, inl X,
   map := λ X Y f, f }
 
-@[simp] lemma inl_obj (X : C) : (inl_ C D).obj X = inl X := rfl
-@[simp] lemma inl_map {X Y : C} {f : X ⟶ Y} : (inl_ C D).map f = f := rfl
-
 /-- `inr_` is the functor `X ↦ inr X`. -/
-def inr_ : D ⥤ C ⊕ D :=
+@[simps] def inr_ : D ⥤ C ⊕ D :=
 { obj := λ X, inr X,
   map := λ X Y f, f }
 
-@[simp] lemma inr_obj (X : D) : (inr_ C D).obj X = inr X := rfl
-@[simp] lemma inr_map {X Y : D} {f : X ⟶ Y} : (inr_ C D).map f = f := rfl
-
 /-- The functor exchanging two direct summand categories. -/
 def swap : C ⊕ D ⥤ D ⊕ C :=
 { obj :=

src/data/list/defs.lean

@@ -531,4 +531,11 @@ protected def traverse {F : Type u → Type v} [applicative F] {α β : Type*} (
 | [] := pure []
 | (x :: xs) := list.cons <$> f x <*> traverse xs
 
+/-- `get_rest l l₁` returns `some l₂` if `l = l₁ ++ l₂`.
+  If `l₁` is not a prefix of `l`, returns `none` -/
+def get_rest [decidable_eq α] : list α → list α → option (list α)
+| l      []      := some l
+| []     _       := none
+| (x::l) (y::l₁) := if x = y then get_rest l l₁ else none
+
 end list

src/data/string/defs.lean

@@ -15,9 +15,15 @@ def split_on (c : char) (s : string) : list string :=
 def is_prefix_of (x y : string) : bool :=
 x.to_list.is_prefix_of y.to_list
 
+/-- Tests whether the first string is a suffix of the second string -/
 def is_suffix_of (x y : string) : bool :=
 x.to_list.is_suffix_of y.to_list
 
+/-- `get_rest s t` returns `some r` if `s = t ++ r`.
+  If `t` is not a prefix of `s`, returns `none` -/
+def get_rest (s t : string) : option string :=
+list.as_string <$> s.to_list.get_rest t.to_list
+
 /-- Removes the first `n` elements from the string `s` -/
 def popn (s : string) (n : nat) : string :=
 (s.mk_iterator.nextn n).next_to_string

src/meta/expr.lean

@@ -475,14 +475,18 @@ namespace expr
   is an eta-expansion of a structure. (not to be confused with eta-expanion for `λ`). -/
 open tactic
 
-/-- Checks whether for all elements `(nm, val)` in the list we have `val = nm.{univs} args` -/
+/-- `is_eta_expansion_of args univs l` checks whether for all elements `(nm, pr)` in `l` we have
+  `pr = nm.{univs} args`.
+  Used in `is_eta_expansion`, where `l` consists of the projections and the fields of the value we
+  want to eta-reduce. -/
 meta def is_eta_expansion_of (args : list expr) (univs : list level) (l : list (name × expr)) :
   bool :=
 l.all $ λ⟨proj, val⟩, val = (const proj univs).mk_app args
 
-/-- Checks whether there is an expression `e` such that for all elements `(nm, val)` in the list
-  `val = nm ... e` where `...` denotes the same list of parameters for all applications.
-  Returns e if it exists. -/
+/-- `is_eta_expansion_test l` checks whether there is a list of expresions `args` such that for all
+  elements `(nm, pr)` in `l` we have `pr = nm args`. If so, returns the last element of `args`.
+  Used in `is_eta_expansion`, where `l` consists of the projections and the fields of the value we
+  want to eta-reduce. -/
 meta def is_eta_expansion_test : list (name × expr) → option expr
 | []              := none
 | (⟨proj, val⟩::l) :=
@@ -497,17 +501,22 @@ meta def is_eta_expansion_test : list (name × expr) → option expr
   | _                       := none
   end
 
-/-- Checks whether there is an expression `e` such that for all *non-propositional* elements
-  `(nm, val)` in the list `val = e ... nm` where `...` denotes the same list of parameters for all
-  applications. Also checks whether the resulting expression unifies with the given one -/
+/-- `is_eta_expansion_aux val l` checks whether `val` can be eta-reduced to an expression `e`.
+  Here `l` is intended to consists of the projections and the fields of `val`.
+  This tactic calls `is_eta_expansion_test l`, but first removes all proofs from the list `l` and
+  afterward checks whether the retulting expression `e` unifies with `val`.
+  This last check is necessary, because `val` and `e` might have different types. -/
 meta def is_eta_expansion_aux (val : expr) (l : list (name × expr)) : tactic (option expr) :=
 do l' ← l.mfilter (λ⟨proj, val⟩, bnot <$> is_proof val),
   match is_eta_expansion_test l' with
   | some e := option.map (λ _, e) <$> try_core (unify e val)
   | none   := return none
   end
 
-/-- Checks whether there is an expression `e` such that `val` is the eta-expansion of `e`.
+/-- `is_eta_expansion val` checks whether there is an expression `e` such that `val` is the
+  eta-expansion of `e`.
+  With eta-expansion we here mean the eta-expansion of a structure, not of a function.
+  For example, the eta-expansion of `x : α × β` is `⟨x.1, x.2⟩`.
   This assumes that `val` is a fully-applied application of the constructor of a structure.
 
   This is useful to reduce expressions generated by the notation

src/tactic/core.lean

@@ -1107,8 +1107,9 @@ and fails otherwise.
 meta def {u} success_if_fail_with_msg {α : Type u} (t : tactic α) (msg : string) : tactic unit :=
 λ s, match t s with
 | (interaction_monad.result.exception msg' _ s') :=
-  if msg = (msg'.iget ()).to_string then result.success () s
-  else mk_exception "failure messages didn't match" none s
+  let expected_msg := (msg'.iget ()).to_string in
+  if msg = expected_msg then result.success () s
+  else mk_exception format!"failure messages didn't match. Expected:\n{expected_msg}" none s
 | (interaction_monad.result.success a s) :=
    mk_exception "success_if_fail_with_msg combinator failed, given tactic succeeded" none s
 end