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