Topic: Will simp go in a loop?
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
Mario Carneiro (Apr 03 2018 at 03:36):
Why don't you try it? I think the answer is yes
Kenny Lau (Apr 03 2018 at 03:37):
I tried it and it succeeded
Kenny Lau (Apr 03 2018 at 03:38):
oh, it went in a loop when the goal can't be closed
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