Zulip Chat Archive

Stream: general

Topic: Will simp go in a loop?


view this post on Zulip Kenny Lau (Apr 03 2018 at 03:35):

If I have two simp lemmas that are the inverse of each other, will simp go into a loop? For example:

@[simp] lemma mul_act : (g * h) • x = g • h • x :=
group_action.mul g h x

@[simp] lemma act_act : g • h • x = (g * h) • x :=
eq.symm $ group_action.mul g h x

view this post on Zulip Mario Carneiro (Apr 03 2018 at 03:36):

Why don't you try it? I think the answer is yes

view this post on Zulip Kenny Lau (Apr 03 2018 at 03:37):

I tried it and it succeeded

view this post on Zulip Kenny Lau (Apr 03 2018 at 03:38):

oh, it went in a loop when the goal can't be closed

view this post on Zulip Simon Hudon (Apr 03 2018 at 03:38):

I think you should think of simp lemmas as a way to decrease the complexity of your expressions. If they cancel each other, one of them must not be decreasing the complexity. Which one should you apply by name?


Last updated: May 17 2021 at 21:12 UTC