simp and unfold with matrix mul

Stream: new members

[Yakov Pechersky]

The docs suggest that simp will use unfold. So why do the examples below fail if unfold is not invoked? Also, why does the presence of matrix.mul_eq_mul confuse simp? Changing the definition attribute from reducible to anything else does not change the behavior.

import data.matrix.basic

set_option trace.simplify.rewrite true

variables (n : ℕ) (R : Type*) [field R]
variables (A B C : matrix (fin n) (fin n) R)

variables {n} {R}
-- attempt using (*)
@[reducible] def mat_invertible : Prop := A * B = 1

-- this lemma is never used by simp
@[simp] lemma mat_invertible_def : mat_invertible A B ↔ A * B = 1 := iff.rfl

example (h : mat_invertible A B) : A * B * C = C :=
by { simp [-matrix.mul_eq_mul, h] } -- fails, simp does not unfold h

@[simp] lemma mat_inv_left_cancel (h : mat_invertible A B) : A * B * C = C :=
by { unfold mat_invertible at h, simp [h] }

example (h : mat_invertible A B) : C * A * B = C :=
by { unfold mat_invertible at h, simp [h, mul_assoc] } -- fails, does not utilize mul_assoc

example (h : mat_invertible A B) : C * A * B = C :=
by { unfold mat_invertible at h, simp [h, matrix.mul_assoc] } -- fails, does not utilize h

@[simp] lemma mat_inv_right_cancel (h : mat_invertible A B) : C * A * B = C :=
by { unfold mat_invertible at h, simp [-matrix.mul_eq_mul, h, mul_assoc] } -- succeeds

-- attempt using (matrix.mul)
@[reducible] def mat_invertible' : Prop := matrix.mul A B = 1

-- this lemma is never used by simp
@[simp] lemma mat_invertible_def' : mat_invertible' A B ↔ matrix.mul A B = 1 := iff.rfl

example (h : mat_invertible' A B) : A * B * C = C :=
by { simp [h] } -- fails, simp does not unfold h

@[simp] lemma mat_inv_left_cancel' (h : mat_invertible' A B) : A * B * C = C :=
by { unfold mat_invertible' at h, simp [h] }

example (h : mat_invertible' A B) : C * A * B = C :=
by { unfold mat_invertible' at h, simp [h, mul_assoc] } -- fails, does not utilize mul_assoc

example (h : mat_invertible' A B) : C * A * B = C :=
by { unfold mat_invertible' at h, simp [h, matrix.mul_assoc] } -- succeeds

@[simp] lemma mat_inv_right_cancel' (h : mat_invertible A B) : C * A * B = C :=
by { unfold mat_invertible at h, simp [-matrix.mul_eq_mul, h, mul_assoc] } -- succeeds

[Alex J. Best]

Which docs suggest simp will use unfold? Simp matches terms by syntactic equality so it doesn't "know" how to use mat_invertible_def to match terms, you can do

simp at h,
simp [h],

instead,
The lemma mat_invertible_def is applied if the target has mat_invertible A B in it, but your goal doesn't, only h does.

[Yakov Pechersky]

Aha. That makes sense. So I can do simp * at * to resolve some of the unfold away. But the -matrix.mul_eq_mul issue remains:

import data.matrix.basic

set_option trace.simplify.rewrite true

variables (n : ℕ) (R : Type*) [field R]
variables (A B C : matrix (fin n) (fin n) R)

variables {n} {R}
-- attempt using (*)
@[reducible] def mat_invertible : Prop := A * B = 1

-- this lemma is never used by simp
@[simp] lemma mat_invertible_def : mat_invertible A B ↔ A * B = 1 := iff.rfl

@[simp] lemma mat_inv_left_cancel (h : mat_invertible A B) : A * B * C = C :=
by simp * at *

example (h : mat_invertible A B) : C * A * B = C :=
by simp [*, mul_assoc] at * -- fails, does not utilize mul_assoc

example (h : mat_invertible A B) : C * A * B = C :=
by simp [-matrix.mul_eq_mul, *, mul_assoc] at * -- succeeds

@[simp] lemma mat_inv_right_cancel (h : mat_invertible A B) : C * A * B = C :=
by simp [*, matrix.mul_assoc] at * -- succeeds

-- attempt using (matrix.mul)
@[reducible] def mat_invertible' : Prop := matrix.mul A B = 1

-- this lemma is never used by simp
@[simp] lemma mat_invertible_def' : mat_invertible' A B ↔ matrix.mul A B = 1 := iff.rfl

@[simp] lemma mat_inv_left_cancel' (h : mat_invertible' A B) : A * B * C = C :=
by simp * at *

example (h : mat_invertible' A B) : C * A * B = C :=
by simp [*, mul_assoc] at * -- fails, does not utilize mul_assoc

example (h : mat_invertible' A B) : C * A * B = C :=
by simp [-matrix.mul_eq_mul, *, mul_assoc] at * -- fails because of mat_invertible' defn

example (h : mat_invertible' A B) : C * A * B = C :=
by simp [*, matrix.mul_assoc] at * -- succeeds

[Alex J. Best]

What do you mean by the issue remains? Which of the fails would you like to work?

[Yakov Pechersky]

I guess the question is why does including -matrix.mul_eq_mul make the latter example here work:

example (h : mat_invertible A B) : C * A * B = C :=
by simp [*, mul_assoc] at * -- fails, does not utilize mul_assoc

example (h : mat_invertible A B) : C * A * B = C :=
by simp [-matrix.mul_eq_mul, *, mul_assoc] at * -- succeeds

[Alex J. Best]

Because mul_assoc says c*a*b = c*(a*b) so if matrix.mul_eq_mul fires before mul_assoc then the goal becomes (c.mul a).mul b and mul_assoc can't match this as its in terms of * not mul.
Basically you have to make a choice whether your simp lemmas are in terms of mul or * for matrix and feed in the right lemmas for whatever choice you make, so either have matrix.mul_eq_mul in your simp set and use matrix.mul_assoc or have matrix.mul_eq_mul not in the simp set and use mul_assoc.

[Alex J. Best]

Or you make no choice and include both mul_assoc and matrix.mul_assoc in your simp set.
You might find reading about confluent rewriting systems interesting, https://en.wikipedia.org/wiki/Confluence_(abstract_rewriting)