# Zulip Chat Archive

## Stream: new members

### Topic: extensionality in matrix defs

#### Yakov Pechersky (Jun 11 2020 at 05:26):

I'm trying to show simple examples of matrix proofs. If the definition of a matrix is a `m -> n -> k`

, then why does the first proof not typecheck? I understand why the second one (specialized form of the #data/matrix proof) works.

```
import data.real.basic
import data.matrix.basic
variables {n : ℕ}
-- Multiplication of a matrix by a real scalar, doesn't work
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) : s • A = (∀ i j, s * (A i j)) :=
sorry
-- type expected at
-- s * A i j
-- term has type
-- ℝ
variables (s : ℝ) (A : matrix (fin n) (fin n) ℝ)
-- works
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) (i : fin n) (j : fin n) :
(s • A) i j = s * (A i j) :=
matrix.smul_val s A i j
```

#### Bryan Gin-ge Chen (Jun 11 2020 at 05:34):

You need to use `λ`

, not `∀`

:

```
import data.real.basic
import data.matrix.basic
variables {n : ℕ}
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) : s • A = (λ i j, s * (A i j)) :=
sorry
```

#### Yakov Pechersky (Jun 11 2020 at 05:35):

Totally. I should sleep more, confusing one triangle looking symbol with another.

#### Yakov Pechersky (Jun 11 2020 at 05:37):

However,

```
#check @matrix.smul_val
-- matrix.smul_val :
-- ∀ {m n : Type u_1} [_inst_2 : fintype m] [_inst_3 : fintype n] {α : Type u_2} [_inst_5 : semiring α] (a : α)
-- (A : matrix m n α) (i : m) (j : n), (a • A) i j = a * A i j
```

#### Yakov Pechersky (Jun 11 2020 at 05:38):

Which means I can't just supply `matrix.smul_val s A`

since it needs some `i j`

s explicitly

#### Yakov Pechersky (Jun 11 2020 at 05:44):

And simp can't solve it either. Gotta supply some `funext`

.

#### Bryan Gin-ge Chen (Jun 11 2020 at 05:46):

`by congr`

will solve it. Here's a more explicit term proof:

```
import data.real.basic
import data.matrix.basic
variables {n : ℕ}
-- Multiplication of a matrix by a real scalar, doesn't work
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) : s • A = (λ i j, s * (A i j)) :=
congr_arg ((•) s) rfl
```

#### Yakov Pechersky (Jun 11 2020 at 05:49):

`congr`

is not something I'm very familiar with, the tutorials didn't really cover it in depth. Any good docs on it? Mouse-over for it gives no info either. https://leanprover-community.github.io/mathlib_docs/tactics.html#congr doesn't mention `congr_arg`

directly, `solve_by_elim`

does though.

#### Yakov Pechersky (Jun 11 2020 at 05:53):

Is it more idiomatic to use `congr_arg`

or `funext`

, like in:

```
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) : s • A = λ i j, s * (A i j) :=
by { funext i j, exact matrix.smul_val s A i j }
```

#### Bryan Gin-ge Chen (Jun 11 2020 at 05:54):

`congr`

stands for congruence in the sense of congruence relation. Now that I look at the docs, I'm not so sure about the tactic, but lemmas starting with `congr`

are frequently useful when you have a function applied to both sides of an equality.

#### Bryan Gin-ge Chen (Jun 11 2020 at 05:57):

I'm not sure what's more idiomatic. Maybe this?

```
example (s : ℝ) (A : matrix (fin n) (fin n) ℝ) : s • A = λ i j, s * (A i j) :=
by { funext i j, refl }
```

#### Yakov Pechersky (Jun 11 2020 at 05:57):

Your statement that we're applying a function on both sides implies the fact that `\all (t : R), s • t = s * t`

. Does `rfl`

also utilize that?

#### Bryan Gin-ge Chen (Jun 11 2020 at 06:07):

`rfl`

is a term that proves an equality by asserting that the two sides are definitionally equal. `refl`

is the tactic version of that.

The goal that `refl`

closes in this case is: `(s • A) i j = s * A i j`

To see that this is a definitional equality, you can look at how src#matrix.has_scalar is defined. Well, it directs you to src#pi.has_scalar, which is `λ s x, λ i, s • (x i)`

. Here, `•`

is the scalar multiplication of `ℝ`

, which is definitionally the same as the ordinary multiplication `*`

.

#### Bryan Gin-ge Chen (Jun 11 2020 at 06:09):

Sorry... it's late, so I'm probably not explaining this very well.

#### Yakov Pechersky (Jun 11 2020 at 06:14):

It's a great explanation, thanks for the insight about the underlying `pi.has_scalar`

definition. It's impressive how far down the `rfl`

term goes without needing additional help. So in this example, recognizing that scalar multiplication `((•) s)`

on the underlying field is just that field's multiplication.

#### Bryan Gin-ge Chen (Jun 11 2020 at 06:23):

`rfl`

can be impressive, but since it can force Lean to unfold lots and lots, it's sometimes better to use lemmas instead. I found the discussion in this thread enlightening.

Last updated: Dec 20 2023 at 11:08 UTC