# Zulip Chat Archive

## 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 ~~ That times out!`ext`

, I recommend `congr`

#### 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