Rewriting function definition

Stream: new members

[Aron Erben]

Hello, I would like to rewrite a function definition with a specified target. Here is an MWE:

import data.matrix.basic
import data.real.basic
localized "infixl ` ⬝ `:75 := matrix.mul" in matrix

variables
  {n m : ℕ}
  {X : matrix (fin n) (fin m) ℝ}
  {Y : matrix (fin m) (fin n) ℝ}

lemma matrix_mul_mul : X ⬝ Y ⬝ X = X
:=
begin
  -- This should rewrite the first ⬝, not the second one!
  rw matrix.mul,
end

Currently, the rw matrix.mul rewrites Y ⬝ X, but I would like it to rewrite X ⬝ Y. I had the following two ideas, neither of which worked:

1. Adding an argument to the rewrite to indicate what should be rewritten:

begin
  -- This should rewrite the first ⬝, not the second one!
  rw matrix.mul X _,
end

This, unsurprisingly, doesn't work, I assume because matrix.mul is a function definition and not a theorem/lemma. So it just takes the X as the first argument.

2. Using nth_rewrite.

begin
  -- This should rewrite the first ⬝, not the second one!
  -- 1 should do the 2nd rewrite, as 0 does the 1st
  nth_rewrite 1 matrix.mul,
end

Which gives the following error:

31:3: failed: not enough rewrites found
state:
n m : ℕ,
X : matrix (fin n) (fin m) ℝ,
Y : matrix (fin m) (fin n) ℝ
⊢ X ⬝ Y ⬝ X = X

This also doesn't entirely make sense to me, as it should be able to do 2 rewrites.
Is there a way to do this?

[Eric Rodriguez]

Note that infixl is telling Lean that matrix.mul associates on the left. so the term is actually (X.mul Y).mul X, not X.mul (Y.mul X). you can see this with the option pp.notation (specifically the line set_option pp.notation false before the theorem statement, as a debugging option)

[Eric Rodriguez]

but for me, this does rewrite X * Y already, as you have Y * X terms left in the definition

[Aron Erben]

Eric Rodriguez said:

but for me, this does rewrite X * Y already, as you have Y * X terms left in the definition

My context after rw matrix.mul (without pp.notation turned off) is:

n m : ℕ,
X : matrix (fin n) (fin m) ℝ,
Y : matrix (fin m) (fin n) ℝ
⊢ (λ (i : fin n) (k : fin m), matrix.dot_product (λ (j : fin n), (X ⬝ Y) i j) (λ (j : fin n), X j k)) = X

So, for me, there is still (X ⬝ Y), is that not the case for you?

[Eric Rodriguez]

not at all:

n m : ℕ,
X : matrix (fin n) (fin m) ℝ,
Y : matrix (fin m) (fin n) ℝ
⊢ (λ (i : fin n) (k : fin m), matrix.dot_product (λ (j : fin m), X i j) (λ (j : fin m), (Y ⬝ X) j k)) = X

are you on the latest mathlib?

[Aron Erben]

Now I am on the newest version, but I'm still getting the same context as before...

Regardless, I would still like to be able to select which mul is being rewritten, so in your case I would like Y ⬝ X to be rewritten...

[Eric Rodriguez]

but note that Y * X doesn't exist! if the term is (X.mul Y).mul X, there is no Y.mul X in there. You first have to check that multiplication is associative, and then you can do that

[Eric Rodriguez]

(and of course it is, and the correct theorem is docs#matrix.mul_assoc)

[Aron Erben]

Eric Rodriguez said:

but note that Y * X doesn't exist! if the term is (X.mul Y).mul X, there is no Y.mul X in there. You first have to check that multiplication is associative, and then you can do that

Oh dangit, you're completely right... I've been doing this for all the other theorems, but completely missed it here (probably, as you pointed out, because of infixl). Thanks a lot!

[Aron Erben]

Ah, I've misunderstood my initial problem. It's not Y.mul X I would like to have rewritten but (X.mul Y).mul X (the outer mul). So I still have this problem in my non-MWE unfortunately... In general, I would just like to know how I can control which rewrite happens when I'm rewriting function definitions.

[Eric Rodriguez]

I'm personally a bit surprised that nth_rewrite doesn't work, and the docs#matrix.mul_apply methods have the arguments implicit, so you can't really do that either without a lot of _s

[Eric Rodriguez]

can you try rw [...] { occs := occurrences.pos [x] } and try messing with x and see if that works?

[Eric Rodriguez]

you can also try use conv to drill down to what you want