Zulip Chat Archive

Stream: general

Topic: Questions about the simp tactic

Bolton Bailey (May 16 2021 at 06:05):

A couple of questions about the simp tactic

If I use simp only [band_tt] on an expression that looks like (tt && tt && ... n times ... && tt) || (expression of length m not involving &&) should I expect it to take O(mn) time, or O(m + n) time?

Will simp do simplifications in the order I specify? For example, on (tt && tt && ... n times ... && tt) && ff, what is the complexity of simp only [band_tt, band_ff] versus simp only [band_ff, band_tt]?

Scott Morrison (May 16 2021 at 06:16):

The order of the list does not matter.

Scott Morrison (May 16 2021 at 06:17):

I think O(m+n) here, but I've not thought about this much.

Bolton Bailey (May 16 2021 at 06:21):

A more practical question: If I have a cycle of simplifications that would cause an infinite loop of rewrites on their own, but there is another simplification which can escape that cycle, is it guaranteed to escape or might it loop infinitely?

Scott Morrison (May 16 2021 at 06:29):

it will likely loop

Gihan Marasingha (Aug 09 2021 at 13:34):

On the order of lemmas presented to simp. I find that it does matter.

Here's a simple example. What's curious to me is that the second example succeeds if simp is replaced with simp_rw, while the first would fail with the same replacement. Can any explain how the function of simp depends on the order of the lemmas?

import tactic

example (a b n m : ): (a + b) * (n + m) = a * n + a * m  + b * n + b * m :=
  simp [mul_add, add_assoc, add_mul], -- succeeds

example (a b n m : ): (a + b) * (n + m) = a * n + a * m  + b * n + b * m :=
  simp [add_mul, mul_add, add_assoc], -- fails

Bryan Gin-ge Chen (Aug 09 2021 at 13:36):

I can't check right now, but if you add set_option trace.simplify.rewrite true before the examples, you should be able to see the precise sequence of rewrites that simp performs in each case.

Gihan Marasingha (Aug 09 2021 at 13:40):

Thanks @Bryan Gin-ge Chen. I can see what happens in those particular cases now. I'm curious to know if a human reader can determine in advance in what order the lemmas will be applied. It makes a difference as to whether the application will fail or not.

Is there a 'meta simp' that tries all permutations?

Yakov Pechersky (Aug 09 2021 at 13:41):

This is partially because add_assoc is not a great simp lemma. You can add add_left_comm to both and then both will work.

Yakov Pechersky (Aug 09 2021 at 13:41):

add_assoc can lead to states in the term permutation tree that are terminal and simp can't do anything else about it.

Yakov Pechersky (Aug 09 2021 at 13:43):

In general, for ring like things like +, *, /\, \/, doing [op_assoc, op_comm, op_left_comm] will be a ring-like simp.

Kevin Buzzard (Aug 09 2021 at 14:20):

Another way of explaining the issue here is I guess that the lemmas which you gave to simp do not form a confluent rewrite system

Gihan Marasingha (Aug 09 2021 at 14:25):

Ooh, I think that's the concept I was trying to express. Is there a nice way for a human to determine whether a given set of lemmas do indeed form a confluent rewrite system?

Last updated: Aug 03 2023 at 10:10 UTC