How to formalize a proof for this matrix identity

Stream: new members

[Narayana Reinaldo]

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]

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]

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]

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]

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

[Narayana Reinaldo]

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]

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]

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]

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]

Instead of ext, I recommend congr That times out!

[Eric Wieser]

But ring works fine for me

[Eric Wieser]

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

[Kyle Miller]

@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]

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