Effective rewriting

Stream: new members

[Egor Morozov]

Suppose my goal contains a term of the form (p * q) * (r * s), where p, q, r, s are long expressions containing proofs. How to rewrite this piece as (p * s) * (r * q) minimizing the headache? Of course, I can catch this piece in conv mode by pattern matching but then I still have to write an ugly chain of mul_comm and mul_assoc sometimes putting p, q, r, s as explicit arguments (which are, again, very long and contain proofs). What I would like to do is to assign (meta?)variable names to p,q,r,s automatically by pattern matching and then just use ring. Is it possible to implement this strategy?

[Kevin Buzzard]

You could do something like this:

example (p q r s : ℕ) : (p * q) * (r * s) = 37 := by
  rw [mul_assoc]
  nth_rw 2 [mul_comm]
  nth_rw 3 [mul_comm]
  rw [mul_assoc]
  rw [← mul_assoc]
  show (p * s) * (r * q) = 37
  sorry

but this will only work if p,q,r,s don't have any multiplications in; if they do you'll have to tweak the numbers :-)

[Kevin Buzzard]

Oh this is probably better:

example (p q r s : ℕ) : (p * q) * (r * s) = 37 := by
  have foo (p q r s : ℕ) : (p * q) * (r * s) = (p * s) * (r * q) := by ring
  rw [foo]
  show (p * s) * (r * q) = 37
  sorry

[Damiano Testa]

There is also this option:

lemma mul_mul_mul_com_other (p q r s : ℕ) :
    (p * q) * (r * s) = (p * s) * (q * r) := by
  ring

example (p q r s : ℕ) : (p * q) * (r * s) = 37 := by
  rw [mul_mul_mul_com_other]
  sorry

Note that docs#mul_mul_mul_comm is actually a thing.

EDIT: Oh, I had not internalised Kevin's second snippet!

[Egor Morozov]

Oh, indeed, I can just abstract the variables in a separate lemma. It was so easy... @Kevin Buzzard, @Damiano Testa, thank you!