extensionality in matrix defs

Stream: new members

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

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]

Which means I can't just supply matrix.smul_val s A since it needs some i js explicitly

[Yakov Pechersky]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

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.