simplifying in `monoid_algebra`

Stream: general

[Yury G. Kudryashov]

I'm helping @Laurent Bartholdi with a Lean course. @Cedric Holle is one of the students at this course and he tries to formalize some equality in $\mathbb Q[GL_4(\mathbb Q)]$ (actually, in $\mathbb Q[G]$, where $G$ is a subgroup of $GL_4(\mathbb Q)$ but this shouldn't be too important). The equality is rather long and I hope that Cedric will copy+paste relevant definitions below.
Once we unfold the definitions, we get a linear combination of finsupp.single (some_matrix) 1 1. In order to simplify this, we need to decide whether some_matrix is equal to one or no. Can some tactic do this for us?

[Kevin Buzzard]

Please tell me that GL_4(G) is a typo for G :-)

[Yury G. Kudryashov]

Thanks! Fixed.

[Kevin Buzzard]

Is some_matrix literally a 4x4 matrix with explicit rational coefficients? Does norm_num work?

[Yury G. Kudryashov]

Yes, some_matrix is an explicit 4x4 matrix. It is obtained using arithmetic operations from matrices in ![...] notation.

[Yury G. Kudryashov]

The problem is to make norm_num decide whether this matrix is equal to 1 or not.

[Yury G. Kudryashov]

And feed the result to one of 2 lemmas about finsupp.single.

[Yury G. Kudryashov]

More generally, we may have finsupp.single a b c, where a = c is decidable.

[Yury G. Kudryashov]

I don't remember if norm_num can tell whether (1 : matrix (fin 2) (fin 2) R) = ![[1, 0], [0, 1]] or not.

[Kevin Buzzard]

I see, and this is why you wanted dec_trivial!

[Yakov Pechersky]

have : some_matrix = (1 : matrix _ _ _),
{ ext i j; fin_cases i; fin_cases j; norm_num }

[Kevin Buzzard]

The problem with that is that it only proves that things are equal to 1, not that they're not equal to 1

[Yury G. Kudryashov]

And now you have 20-30 terms of this form.

[Yury G. Kudryashov]

The question is how to avoid 20-30 explicitly written lemmas "this is not equal to one".

[Yakov Pechersky]

The best I could do for similar problems can be found in this file: https://github.com/pechersky/e222/blob/master/src/problems02.lean#L49-L58

[Yury G. Kudryashov]

If you write a proof for "not equal" manually, then you can just tell Lean which elements are not equal.

[Yury G. Kudryashov]

I guess, one can write a tactic that goes over elements of fin 4 and evaluates LHS and RHS

[Yury G. Kudryashov]

But I'm not good at writing tactics.

[Yakov Pechersky]

Is that not fin_cases?

[Gabriel Ebner]

I guess, one can write a tactic that goes over elements of fin 4 and evaluates LHS and RHS
But I'm not good at writing tactics.

A simple approach is to write a lemma matrix22_ext_iff : (![![a,b], ![c,d]] = ![![e,f], ![g,h]]) ↔ a=e ∧ b = f ∧ c = g ∧ d = h and then call simp [matrix22_ext_iff] (we might have such a lemma already, didn't check).

[Yury G. Kudryashov]

Am I right that in this case simp will simplify each equality even if one of them already says false?

[Gabriel Ebner]

Right.

[Yury G. Kudryashov]

So, a specialized tactic can be more effective but requires some meta programming skills. Let's wait for the students to come here, read the backlog, and decide what they're going to do.

[Eric Wieser]

Rewriting backwards by docs#matrix.one_fin_three (but for four) might put you in a place where dec_trivial is easy

[Yury G. Kudryashov]

dec_trivial can't solve (5 : rat) = 1

[Yury G. Kudryashov]

And the matrices have half-integer elements.

[Yury G. Kudryashov]

So, we can't just deal with matrices over int.

[Kevin Buzzard]

You could write an ext lemma which clears the denominators and reduces to int :-)