Zulip Chat Archive

Stream: general

Topic: simps


view this post on Zulip Johan Commelin (Sep 27 2019 at 17:44):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 27 2019 at 19:49):

@[simps?] seems like a nice feature.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 01 2019 at 04:30):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Oct 01 2019 at 04:48):

Oops, okay, I didn't see that.

view this post on Zulip Scott Morrison (Oct 01 2019 at 04:49):

Where did you get to?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 01 2019 at 04:50):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.π }

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Oct 29 2019 at 03:20):

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

view this post on Zulip 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.

view this post on Zulip 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}

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Oct 29 2019 at 04:02):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Mar 25 2020 at 03:27):

Already guessed name in my case

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2020 at 07:38):

Do you mean #print prefix your_namespace?

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 18 2020 at 04:31):

That it applies less often?

view this post on Zulip Johan Commelin (Aug 18 2020 at 04:31):

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

view this post on Zulip Johan Commelin (Aug 18 2020 at 04:32):

Thanks for teaching me about that option!

view this post on Zulip Kenny Lau (Aug 18 2020 at 06:37):

#backticks

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Aug 18 2020 at 14:17):

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

view this post on Zulip Simon Hudon (Aug 18 2020 at 14:20):

What do you mean?

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 18 2020 at 14:22):

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

view this post on Zulip 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!

view this post on Zulip Reid Barton (Aug 18 2020 at 15:51):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 18 2020 at 15:58):

Yes, that's right

view this post on Zulip 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