## Stream: general

### Topic: simps

#### Johan Commelin (Sep 27 2019 at 17:44):

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

#### Floris van Doorn (Sep 27 2019 at 18:32):

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 (Sep 27 2019 at 19:49):

@[simps?] seems like a nice feature.

#### Simon Hudon (Sep 27 2019 at 20:09):

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 (Sep 27 2019 at 20:40):

@[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 (Sep 27 2019 at 21:18):

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 (Sep 27 2019 at 21:19):

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 (Sep 27 2019 at 21:29):

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 (Oct 01 2019 at 03:55):

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 (Oct 01 2019 at 04:30):

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

#### Reid Barton (Oct 01 2019 at 04:40):

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 (Oct 01 2019 at 04:48):

Oops, okay, I didn't see that.

#### Scott Morrison (Oct 01 2019 at 04:49):

Where did you get to?

#### Scott Morrison (Oct 01 2019 at 04:50):

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 (Oct 01 2019 at 04:50):

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

#### Floris van Doorn (Oct 01 2019 at 14:48):

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 (Oct 01 2019 at 14:54):

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 (Oct 02 2019 at 04:40):

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 (Oct 02 2019 at 04:42):

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

#### Floris van Doorn (Oct 05 2019 at 20:57):

@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 (Oct 28 2019 at 22:01):

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

Fixed in #1626

#### Floris van Doorn (Oct 29 2019 at 03:20):

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

#### Floris van Doorn (Oct 29 2019 at 03:29):

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 (Oct 29 2019 at 03:47):

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 (Oct 29 2019 at 03:58):

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 (Oct 29 2019 at 04:02):

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

#### Yury G. Kudryashov (Mar 25 2020 at 03:25):

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

#### Yury G. Kudryashov (Mar 25 2020 at 03:27):

Already guessed name in my case

#### Bryan Gin-ge Chen (Mar 25 2020 at 07:38):

Do you mean #print prefix your_namespace?

#### Johan Commelin (Aug 18 2020 at 04:06):

@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 (Aug 18 2020 at 04:28):

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 (Aug 18 2020 at 04:31):

That it applies less often?

#### Johan Commelin (Aug 18 2020 at 04:31):

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

#### Johan Commelin (Aug 18 2020 at 04:32):

Thanks for teaching me about that option!

#backticks

#### Simon Hudon (Aug 18 2020 at 14:17):

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

#### Johan Commelin (Aug 18 2020 at 14:17):

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

#### Simon Hudon (Aug 18 2020 at 14:20):

What do you mean?

#### Reid Barton (Aug 18 2020 at 14:21):

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 (Aug 18 2020 at 14:22):

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

#### Floris van Doorn (Aug 18 2020 at 15:49):

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

#### Reid Barton (Aug 18 2020 at 15:51):

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

#### Floris van Doorn (Aug 18 2020 at 15:58):

@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 (Aug 18 2020 at 15:58):

Yes, that's right

#### Reid Barton (Aug 18 2020 at 16:00):

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.

Last updated: May 13 2021 at 06:15 UTC