Questions about the simp tactic

Stream: general

[Bolton Bailey]

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]

The order of the list does not matter.

[Scott Morrison]

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

[Bolton Bailey]

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]

it will likely loop

[Gihan Marasingha]

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 :=
begin
  simp [mul_add, add_assoc, add_mul], -- succeeds
end

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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?