Stream: new members

Topic: How to formalize a proof for this matrix identity

Narayana Reinaldo (Aug 24 2023 at 17:25):

I am trying to formalize the proof of the following fact in lean:

$\begin{pmatrix}1 & 1 & 1 \\ 0 & 1 & 1\\ 0 & 0 & 1\end{pmatrix}^n = \begin{pmatrix}1 & n & \frac{n(n+1)}{2} \\ 0 & 1 & n\\ 0 & 0 & 1\end{pmatrix}$

The proof is almost immediately using induction, but I haven't managed to formalize the proof in lean, my idea was to use theorems like monoid.pow_zero and monoid.pow_succ, but I don't know how to access these. Should I prove that matrices form a monoid?

Can anyone point me in the right direction to be able to proof this?

This is the code I have until now:

import tactic -- imports all the Lean tactics
import data.matrix.notation

example (n : ℕ):
!![1, 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![1, n, n*(n+1)/2; 0, 1, n; 0, 0, 1] :=
begin
induction n with n hn,
{ -- Should be simply monoid.pow_zero
sorry},
{ -- Should be simply monoid.pow_succ with simple algebra
sorry}
end


From my question in Stack Overflow, I know that I might have problems with n*(n+1)/2 because n has type nat, but I don't know how to coarce it into rational type, since writing (n : \Q)*(n+1)/2 gives me an error.

Thank you

Ruben Van de Velde (Aug 24 2023 at 17:47):

On one hand, you're likely to summon Kevin with a question like this, to give you the correct syntax to state this as a result on rational matrices.

On the other, there's a good chance you won't be getting much help with lean 3 questions anymore

Ruben Van de Velde (Aug 24 2023 at 17:49):

On a third hand, it may be the case (I'm not sure at all) that you need to use a theorem specifically about matrix powers, not pow_succ

Alex J. Best (Aug 24 2023 at 18:02):

The syntax error is because lean realises too late that you actually want to talk about rational matrices, a fix is to insert type ascriptions as follows

import tactic -- imports all the Lean tactics
import data.matrix.notation

example (n : ℕ):
!![(1 : ℚ), 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![(1 : ℚ), n, (n : ℚ)*(n+1)/2; 0, 1, n; 0, 0, 1] :=
begin
induction n with n hn,
{ -- Should be simply monoid.pow_zero
sorry},
{ -- Should be simply monoid.pow_succ with simple algebra
sorry}
end


Yakov Pechersky (Aug 24 2023 at 18:04):

It also won't be just monoid.pow_foo, you have to show they're equal extensionally (element-by-element).

Narayana Reinaldo (Aug 24 2023 at 18:16):

Alex J. Best said:

The syntax error is because lean realises too late that you actually want to talk about rational matrices, a fix is to insert type ascriptions as follows

import tactic -- imports all the Lean tactics
import data.matrix.notation

example (n : ℕ):
!![(1 : ℚ), 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![(1 : ℚ), n, (n : ℚ)*(n+1)/2; 0, 1, n; 0, 0, 1] :=
begin
induction n with n hn,
{ -- Should be simply monoid.pow_zero
sorry},
{ -- Should be simply monoid.pow_succ with simple algebra
sorry}
end


Thank you, indeed this now fixes the error, now lean should assume that all the elements of the matrix are in \Q, right? At least, if I check the type of !![(1 : ℚ), 1, 1; 0, 1, 1; 0, 0, 1] now is matrix (fin 3) (fin 3) ℚ.

Narayana Reinaldo (Aug 24 2023 at 18:24):

Yakov Pechersky said:

It also won't be just monoid.pow_foo, you have to show they're equal extensionally (element-by-element).

Sorry, indeed, I wasn't expecting that those theorems would immediately solve the goals. But for the induction proof, I first need to prove the following:

⇑matrix.of ![![1, 1, 1], ![0, 1, 1], ![0, 0, 1]] ^ 0 = ⇑matrix.of ![![1, ↑0, ↑0 * (↑0 + 1) / 2], ![0, 1, ↑0], ![0, 0, 1]]


To solve this, I would expect to use something like pow_zero in the LHS (and then prove that whatever is left is actually equal to the RHS). But I don't know how to use this kind of theorems, matrix.pow_zero doesn't exist, so I thought that maybe monoid.pow_zero would be the way. But I don't know if I have to prove that the matrices form a monoid or this is already known to lean.

Kevin Buzzard (Aug 24 2023 at 19:04):

Yes, matrices are a monoid so you can just use pow_zero and pow_succ. Here's a proof (Lean 4):

import Mathlib.Tactic -- imports all the Lean tactics
import Mathlib.Data.Matrix.Notation

example (n : ℕ):
!![(1 : ℚ), 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![(1 : ℚ), n, (n : ℚ)*(n+1)/2; 0, 1, n; 0, 0, 1] := by
induction' n with n hn
{ rw [pow_zero]
simp }
{ rw [pow_succ, hn]
simp
ring }


Narayana Reinaldo (Aug 25 2023 at 07:47):

Thank you, Kevin, so if I understand it correctly, the theorems pow_zero and pow_succ are immediately imported when doing import tactic, and those theorems can be applied to any type with monoid structure, right?

example (n : ℕ):
!![(1:ℚ), 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![(1:ℚ), n, n*(n+1)/2; 0, 1, n; 0, 0, 1] :=
begin
induction n with n hn,
{ rw pow_zero,
simp,
dec_trivial,},
{ rw pow_succ,
rw hn,
simp,
-- Still need to prove
-- ⊢ ![![1, ↑n + 1, ↑n * (↑n + 1) / 2 + (↑n + 1)], ![0, 1, ↑n + 1], ![0, 0, 1]]
--   = ![![1, ↑n + 1, (↑n + 1) * (↑n + 1 + 1) / 2], ![0, 1, ↑n + 1], ![0, 0, 1]]
sorry
}
end


I am still left with one goal:
⊢ ![![1, ↑n + 1, ↑n * (↑n + 1) / 2 + (↑n + 1)], ![0, 1, ↑n + 1], ![0, 0, 1]] = ![![1, ↑n + 1, (↑n + 1) * (↑n + 1 + 1) / 2], ![0, 1, ↑n + 1], ![0, 0, 1]]
Now, the only non-trivial thing here is to prove ↑n * (↑n + 1) / 2 + (↑n + 1)=(↑n + 1) * (↑n + 1 + 1) / 2, which should be solved by the ring tactic. But I don't know how to prove this using the matrix types (the tactic ring alone doesn't work for me, it raises a (deterministic) timeout error), I've tried to use ext i j together with cases i, thinking that maybe it would split the goal into three goals for i=0,1,2, but of course (i : fin 3) is defined by i : \N and hi : i < 3, so this doesn't work. Any idea how to proceed?

Eric Wieser (Aug 25 2023 at 07:52):

Instead of ext, I recommend congr That times out!

Eric Wieser (Aug 25 2023 at 07:53):

But ring works fine for me

Eric Wieser (Aug 25 2023 at 07:59):

@Kyle Miller, any idea why congr 1 times out here?

Kyle Miller (Aug 25 2023 at 13:31):

@Eric Wieser I only checked Lean 4, but it looks like it's from trying to apply rfl. If you replace congr 1 with rfl it doesn't fail immediately (I didn't run it long enough to check if it times out). If you use the Std extensions for congr to turn off trying things like rfl at the end, then congr (config := {closePost := false}) 1 does not time out. The congr! 1 tactic does not time out (not sure why).

Narayana Reinaldo (Aug 25 2023 at 16:49):

Thanks @Eric Wieser, the congr tactic worked, now this proof succeeds:

example (n : ℕ):
!![(1:ℚ), 1, 1; 0, 1, 1; 0, 0, 1] ^ n = !![(1:ℚ), n, n*(n+1)/2; 0, 1, n; 0, 0, 1] :=
begin
induction n with n hn,
{ rw pow_zero,
simp,
dec_trivial},
{ rw pow_succ,
rw hn,
simp,
congr,
ring}
end


Last updated: Dec 20 2023 at 11:08 UTC