simps

Stream: general

[Johan Commelin]

Is there some way to ask simps which lemmas it has added?

[Floris van Doorn]

No. Currently the best methods are #print prefix (which will give way too much if your namespace is big) or autocompletion.

Do you want a @[simps?] which also prints which declarations it has added?

[Johan Commelin]

@[simps?] seems like a nice feature.

[Simon Hudon]

I think I would rather go for a #print-like command. Attributes usually do not have such options. On the other hand, if people know the options for #print, a similar command would mesh better with what they already know

[Floris van Doorn]

@[simps?] should never show up in the final version of a file.
It is probably both the easiest write in a file (just adding a question mark to an attribute you already have) and to implement (since I can just let my tactics return some information)

[Simon Hudon]

And #print should never appear either. I'm just thinking of the workflow of using Lean. I think it's better to aim for a consistent way of using it. That makes learning the tool and the language much easier. To me, it goes in the column of keeping arbitrary complexity down

[Floris van Doorn]

A lot of tactics give extra information when adding ?, so it's pretty similar to that (maybe more attributes should print debug info when ? is added).

[Simon Hudon]

It is a common convention for tactics but not attributes. I think I would support it if the ? option printed more than just a list of declarations added to the environment. Maybe some information about the tactics using the attribute for instance.

[Scott Morrison]

I've been away from zulip for a few days, and just came here specifically to ask for @[simps?], and I'm very glad to have been pre-empted.

[Scott Morrison]

Also --- I noticed @[simps] fails if the definition uses a let. Not super important.

[Reid Barton]

Oh, you might not have seen--I have a diff with a lot of simps for category theory, which I haven't PRed yet

[Scott Morrison]

Oops, okay, I didn't see that.

[Scott Morrison]

Where did you get to?

[Scott Morrison]

I ran into one problem in category_theory/products/associator.lean, where @[simps] on associator and inverse_associator didn't seem to have the desired effect. Not quite sure why.

[Scott Morrison]

I'll stop in that case, and put up what I did so far.

[Floris van Doorn]

Also --- I noticed @[simps] fails if the definition uses a let. Not super important.

I did not think about let expressions. What is the example in the library where it fails.

[Floris van Doorn]

I ran into one problem in category_theory/products/associator.lean, where @[simps] on associator and inverse_associator didn't seem to have the desired effect. Not quite sure why.

It is currently the expected behavior that @[simps] produces different lemmas for this. @[simps] has no idea which structures you want to "go into" and which structures you don't, so currently it creates associator_obj_fst, associator_obj_snd_fst and associator_obj_snd_snd (and same for map).
At some point, you might be able to write @[simps associator_obj associator_map] to get your desired output, but that is currently not the case. For now you probably shouldn't use @[simps] on this declaration. If you have an algorithmic method of deciding when to not "go into" a structure, let me know.

[Scott Morrison]

Also --- I noticed @[simps] fails if the definition uses a let. Not super important.

I did not think about let expressions. What is the example in the library where it fails.

In cones.lean:

def map_cone_inv [is_equivalence H]
  (c : cone (F ⋙ H)) : cone F :=
let t := (inv H).map_cone c in
let α : (F ⋙ H) ⋙ inv H ⟶ F :=
  ((whisker_left F (is_equivalence.unit_iso H).inv) : F ⋙ (H ⋙ inv H) ⟶ _) ≫ (functor.right_unitor _).hom in
{ X := t.X,
  π := ((category_theory.cones J C).map α).app (op t.X) t.π }

[Scott Morrison]

Thanks for the explanation in the associator case. I agree it's not obvious what to do here.

[Floris van Doorn]

@Scott Morrison Of course, in this case, I won't be able to generate the lemma map_cone_inv_X as currently stated, because that lemma unfolds some definitions. I could probably generate a lemma like the following:

(H.map_cone_inv c).X = ((inv H).map_cone c).X

Do we sometimes want to keep the let expression, like this:

(H.map_cone_inv c).X = (let t := (inv H).map_cone c in t.X)

[Floris van Doorn]

Also --- I noticed @[simps] fails if the definition uses a let. Not super important.

Fixed in #1626

[Floris van Doorn]

PR #1630 allows us to use simps for functors on product categories.

[Floris van Doorn]

I also tried to make simps useful for new category instances. I added an option to shorten the name (so that we generate the name my_category_hom instead of my_category_to_category_struct_to_has_hom_hom). Then I realized that there is a bigger problem: the simp-lemmas you wrote by hand use things like my_category.to_category_struct, but the automatically generated lemmas use the definiens of my_category.to_category_struct. It might be tricky to fold these definitions in.

[Floris van Doorn]

Is there a reason that whisker_left and whisker_right are defined as projections of whiskering_left/whiskering_right? The following feels more natural to me: (not only because we can use @[simps], but also because it's natural to factor a field out of the definition, if you're going to give it a name anyway)

variables {C : Type u₁} [𝒞 : category.{v₁} C]
          {D : Type u₂} [𝒟 : category.{v₂} D]
          {E : Type u₃} [ℰ : category.{v₃} E]
include 𝒞 𝒟 ℰ

@[simps] def whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) : (F ⋙ G) ⟶ (F ⋙ H) :=
{ app := λ c, α.app (F.obj c),
  naturality' := by intros X Y f; rw [functor.comp_map, functor.comp_map, α.naturality] }

@[simps] def whisker_right {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) : (G ⋙ F) ⟶ (H ⋙ F) :=
{ app := λ c, F.map (α.app c),
  naturality' := by intros X Y f;
    rw [functor.comp_map, functor.comp_map, ←F.map_comp, ←F.map_comp, α.naturality] }

variables (C D E)

@[simps] def whiskering_left : (C ⥤ D) ⥤ ((D ⥤ E) ⥤ (C ⥤ E)) :=
{ obj := λ F,
  { obj := λ G, F ⋙ G,
    map := λ G H α, whisker_left F α },
  map := λ F G τ,
  { app := λ H,
    { app := λ c, H.map (τ.app c),
      naturality' := λ X Y f, begin dsimp, rw [←H.map_comp, ←H.map_comp, ←τ.naturality] end },
    naturality' := λ X Y f, begin ext1, dsimp, rw [f.naturality] end } }

@[simps] def whiskering_right : (D ⥤ E) ⥤ ((C ⥤ D) ⥤ (C ⥤ E)) :=
{ obj := λ H,
  { obj := λ F, F ⋙ H,
    map := λ _ _ α, whisker_right α H },
  map := λ G H τ,
  { app := λ F,
    { app := λ c, τ.app (F.obj c),
      naturality' := λ X Y f, begin dsimp, rw [τ.naturality] end },
    naturality' := λ X Y f, begin ext1, dsimp, rw [←nat_trans.naturality] end } }

variables {C D E}

[Floris van Doorn]

One thing which I might add in the future is to automatically generate lemmas like cone_of_cocone_left_op_π_app for cone_of_cocone_left_op (in category_theory.limits.cones).
Currently, if you write attribute [simps π_app] cone_of_cocone_left_op then when the tactic reaches the app field, it fails. This is because it needs cone_of_cocone_left_op.π to be a constructor to "look into". Instead, I can just apply app to both the LHS and the RHS, and then call simp on the RHS to generate the lemma.
This should automatically generate cone_of_cocone_left_op_π_app.

[Floris van Doorn]

Oh, I now see #1613. That answers my question 2 messages ago.

[Yury G. Kudryashov]

Can I somehow query the list of lemmas generated by simps? Or print all lemmas in a namespace?

[Yury G. Kudryashov]

Already guessed name in my case

[Bryan Gin-ge Chen]

Do you mean #print prefix your_namespace?

[Johan Commelin]

@Floris van Doorn @Simon Hudon This is from the docs of simps

Example:
lean def equiv.simps.inv_fun (e : α ≃ β) : β → α := e.symm @[simps] def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ := ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm⟩
generates
@[simp] lemma equiv.trans_to_fun : ∀ {α β γ} (e₁ e₂) (a : α), ⇑(e₁.trans e₂) a = (⇑e₂ ∘ ⇑e₁) a @[simp] lemma equiv.trans_inv_fun : ∀ {α β γ} (e₁ e₂) (a : γ), ⇑((e₁.trans e₂).symm) a = (⇑(e₁.symm) ∘ ⇑(e₂.symm)) a

And here's my question:
Wouldn't it be better if this generated

@[simp] lemma equiv.trans_to_fun : ∀ {α β γ} (e₁ e₂), ⇑(e₁.trans e₂) = (⇑e₂ ∘ ⇑e₁)

instead? It could chain with function.comp_apply to get the original version, but it would also apply in "unapplied" situations (sorry for the pun).

[Floris van Doorn]

There is an option for that: @[simps {fully_applied := ff}]. See docs#simps_cfg, there are some other nice options, too.

I don't know what the best form for simp-lemmas are. Most simp-lemmas we write in a fully applied version, I believe. Is there any downside to the non-fully applied version?

[Johan Commelin]

That it applies less often?

[Johan Commelin]

But I guess that in practice it doesn't really matter that much

[Johan Commelin]

Thanks for teaching me about that option!

[Kenny Lau]

#backticks

[Simon Hudon]

@Floris van Doorn I must say, I really appreciate that the error message with simps comes with suggestions. So useful!

[Johan Commelin]

We still need to put the tactic suggestions in the docstrings of exists etc...

[Simon Hudon]

What do you mean?

[Reid Barton]

I have a third situation where the type of a field is a function that returns a function (the latter function being of the form fin n -> R) and ideally simps would produce a lemma which is applied to only the first argument.

  coords := λ p, coords R p.1 ++ coords R p.2,    -- here `++` is notation for concatenating `fin n -> R`

I kind of thought it would work that way by default, where simps would use the shape of the definition to decide how many times to eta expand the lemma. Looks like there isn't a setting for this?

[Reid Barton]

Same way simps uses record construction syntax to decide when to apply projections (right?)

[Floris van Doorn]

@Simon Hudon You mean the suggestion to add {rhs_md := semireducible}? I'm glad that was helpful!

[Reid Barton]

I actually just used this :this: today as well :+1:

[Floris van Doorn]

@Reid Barton: You're saying @[simps] should apply the functions to an argument only if you used a lambda (or at least, that there should be an option for that)? That is currently not an option indeed, but I could make it one.

[Reid Barton]

Yes, that's right

[Reid Barton]

It's not really a big deal for me, I could easily write all ~6 simp lemmas I need by hand. But generating lemmas based on the definition term rather than its type seems consistent with the way we treat structures.