Rearranging terms with commutative operator

Stream: new members

[Martin C. Martin]

Below I declare a binary operator, and assert it is associative and commutative. Then I try to use simp to rearrange some terms, but it fails. What am I doing wrong?

def op : ℕ → ℕ → ℕ := sorry

theorem op_assoc : ∀ n m k : ℕ, op (op n m) k = op n (op m k) := sorry

theorem op_comm :  ∀ n m : ℕ, op n m = op m n := sorry

theorem rearrange : ∀ n m k l: ℕ, op (op l k) (op n m) = op (op l n) (op k m) :=
  by simp [op_assoc, op_comm]

[Martin C. Martin]

I figured it out: I need to tell it that it can use op_assoc in the other direction as well.

[Notification Bot]

Martin C. Martin has marked this topic as resolved.

[Notification Bot]

Martin C. Martin has marked this topic as unresolved.

[Martin C. Martin]

I spoke too soon. If I change the last line to:
by simp [op_assoc, op_comm, ← op_assoc]
I get a (deterministic) timeout.

How do I get this working?

[Yakov Pechersky]

You need one more rule, op_left_comm (a b c : nat) : op a (op b c) = op b (op a c)

[Yakov Pechersky]

That should be enough with simp [op_comm, op_assoc, op_left_comm]

[Martin C. Martin]

Thanks! Why does it time out? There should only be a few hundred combinations for 4 leaves and a single operator. Doesn't simp keep track of previous expressions it has generated, so it knows when it has a duplicate?

In general, how do you know when it's ok to add an expression to a simp list? Just try it and see if you get a timeout? And how do you know what alternate to put in it's place, i.e. how would you think of op_left_comm above?

[Yakov Pechersky]

I don't think simp is smart enough to "cancel" out simp [my_lemma, <-my_lemma]. Think of each mentioned lemma a rule. So simp tries to apply any rules it can, and this makes it enter a loop. Just simp [my_comm_lemma] won't enter a loop because for the one rule, there is an "order" of expressions where one is preferred over the other. If you had dome simp [my_comm_lemma, <-my_comm_lemma], that would loop. The 3 rules I provided are sufficient to normalize commutative left associative operation.

[Yakov Pechersky]

That's my headcanon, I think there are more precise/rigorous definitions

[Martin C. Martin]

Thanks Yakov. Another question, this time about rw in calc mode. To prove op_left_comm, this works:

theorem op_left_comm (a b c : nat) : op a (op b c) = op b (op a c) :=
    calc
      op a (op b c) = op (op a b) c : by rw op_assoc
                ... = op (op b a) c : by rw op_comm a
                ... = op b (op a c) : by rw op_assoc

But if I try to combine the first two rw, it fails:

theorem op_left_comm' (a b c : nat) : op a (op b c) = op b (op a c) :=
    calc
      op a (op b c) = op (op b a) c : by rw [op_assoc, op_comm a b]
                ... = op b (op a c) : by rw op_assoc

with

rewrite tactic failed, did not find instance of the pattern in the target expression
  op a b
state:
a b c : ℕ
⊢ op a (op b c) = op b (op a c)

It seems to be trying to apply op_comm a b to the original LHS. Combining the 2nd and 3rd rw works fine though. Is this just a quirk of the first line of calc mode?

[Reid Barton]

You are just not telling it to do what you want it to do. Look at the state after the first rw (you can put your cursor on the , or so).

[Martin C. Martin]

This is what I'm remembering, from TPiL section 5.7:
"It may seem that commutativity and left-commutativity are problematic, in that repeated application of either causes looping. But the simplifier detects identities that permute their arguments, and uses a technique known as ordered rewriting. This means that the system maintains an internal ordering of terms, and only applies the identity if doing so decreases the order. With the three identities mentioned above, this has the effect that all the parentheses in an expression are associated to the right, and the expressions are ordered in a canonical (though somewhat arbitrary) way. Two expressions that are equivalent up to associativity and commutativity are then rewritten to the same canonical form."

So as you say, it's a local choice per identity looking at ordering, not a global "remember all generated expressions to detect loops" as I somehow thought.

[Martin C. Martin]

Thanks Reid, it looks like it's transforming the RHS into the LHS, I assumed it would do the opposite, which seems more natural to me.

[Reid Barton]

Right, because that is the only thing op_assoc can do when used for rewriting in the forward direction.

[Martin C. Martin]

Ah got it, thanks. I pictured calc mode as manipulating an expression (the LHS), not manipulating an equation. TIL!

[Kevin Buzzard]

I still remember the day I learnt this :-) (and was equally confused before the penny dropped!)

[Martin C. Martin]

Yakov Pechersky said:

That should be enough with simp [op_comm, op_assoc, op_left_comm]

So that's still not working, although now I can't make sense of the error message:

def op : ℕ → ℕ → ℕ := sorry

theorem op_assoc : ∀ n m k : ℕ, op (op n m) k = op n (op m k) := sorry

theorem op_comm :  ∀ n m : ℕ, op n m = op m n := sorry

theorem op_left_comm (a b c : nat) : op a (op b c) = op b (op a c) :=
  by rw [← op_assoc, op_comm a b, op_assoc]

theorem rearrange : ∀ n m k l: ℕ, op (op l k) (op n m) = op (op l n) (op k m) :=
  by simp [op_assoc, op_comm, op_left_comm]

The simp fails with:

tactic failed, there are unsolved goals
state:
⊢ ℕ → ℕ → ℕ → ℕ → true

What exactly is the remaining goal? What is it that's left to prove?

[Kevin Buzzard]

simp doesn't do intros by default. The mathlib convention would be to move all of the variables left of the colon as you did with op_left_comm. Alternatively you can add something like {contextual := true} to the simp call