the identity matrix and decidable equality

Stream: mathlib4

[Emily Riehl]

For expository purposes, I've been trying to formalize a tiny bit of linear algebra, and I'm having some difficulties with the identity matrix.

Firstly, this must surely be in mathlib somewhere, but where is it?

In any case, it's nice sometimes to do something yourself, so I wrote this:

import Mathlib.Data.Matrix.Basic

open Matrix

variable (R : Type) [Field R]
variable (n : Type) [DecidableEq n] [Fintype n] [Inhabited n]

/-- The identity matrix. -/
def I : Matrix n n R := by
  refine Matrix.of ?_
  intro i j
  cases (decEq i j)
  · exact 0
  · exact 1

This is my first time using decidable equality in Lean. Was this the right approach?

In particular, I can't seem to do anything with this definition. In particular, I'm unable to prove that I R n i j = I R n j i for i j : n e.g. by case splitting on whether or not i = j.

[Riccardo Brasca]

1 : Matrix _ _ _ should work.

[Floris van Doorn]

Emily Riehl said:

This is my first time using decidable equality in Lean. Was this the right approach?

You can also use the tactic by_cases h : i = j

[Floris van Doorn]

IIRC that uses a decidability proof if there is one, otherwise uses classical principles.

[Riccardo Brasca]

In general defining data in tactic mode is not a very good idea. I would do something like

def I : Matrix n n R := Matrix.of (fun i j ↦ if i = j then 0 else 1)

[Floris van Doorn]

True, my comments works, but for definitions Riccardo's suggestion is better.

[Floris van Doorn]

(if the 1 and 0 are swapped)

[Riccardo Brasca]

import Mathlib

variable (R : Type) [Field R]
variable (n : Type) [DecidableEq n]

def I : Matrix n n R := Matrix.of (fun i j ↦ if i = j then 1 else 0)

example (i j : n) : I R n i j = I R n j i := by
  dsimp only [I]
  aesop

[Emily Riehl]

Thanks for the suggestions. It's great that aesop can prove this but I want to be able to prove it too!

Right now I'm trying (using @Riccardo Brasca's definition):

theorem one : I R n = 1 := by
  ext i j
  unfold I
  by_cases h : i = j
  · sorry
  · sorry

[Riccardo Brasca]

Concerning DecidableEq, the rule of thumb is: if it's needed in a statement or in a def add it as you did. If it is needed in a proof just start the proof by classical and Lean should find it automatically.

[Emily Riehl]

When I use the if .. then .. else in a def and I have either the first hypothesis or its negation how do I reduce that def to the appropriate case?

[Riccardo Brasca]

simp usually does it

[Emily Riehl]

Blerg. Actually the reason I was stuck was I copied your first definition which has a typo.

[Riccardo Brasca]

Ops, sorry!

[Emily Riehl]

Lol. Serves me right for not being careful.

So simp is best practice to reduce an if .. then .. else?

[Edward van de Meent]

i tend to do rw [if_pos h] or rw [if_neg h]

[Edward van de Meent]

also note docs#dif_pos and docs#dif_neg for the dependent version

[Riccardo Brasca]

I am a little bit sad that simp [h] does not work in the first case.

import Mathlib

variable (R : Type) [Field R]
variable (n : Type) [DecidableEq n]

def I : Matrix n n R := Matrix.of (fun i j ↦ if i = j then 1 else 0)

theorem one : I R n = 1 := by
  ext i j
  unfold I
  by_cases h : i = j
  · rw [h]
    simp
  · simp [h]

[Emily Riehl]

Weirdly by_cases h : i = j <;> rfl works, though.

Regarding @Edward van de Meent's suggestion is this supposed to follow a by_cases h : i = j? Because I'm getting an error

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  if i = j then ?m.2305 else ?m.2306

even though it looks like it's there to me.

[Riccardo Brasca]

rfl works because 1 is literally defined like that

[Riccardo Brasca]

I mean, theorem one : I R n = 1 := rfl also works.

[Riccardo Brasca]

In particular it does nothing about the cases

[Edward van de Meent]

Emily Riehl said:

Weirdly by_cases h : i = j <;> rfl works, though.

Regarding Edward van de Meent's suggestion is this supposed to follow a by_cases h : i = j? Because I'm getting an error

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  if i = j then ?m.2305 else ?m.2306

even though it looks like it's there to me.

the fix seems to be to do rw [Matrix.of_apply] before the cases, as there technically wasn't an appropriate pattern in the goal.

[Edward van de Meent]

i.e. the goal contains (Matrix.of (fun x y => if x = y then 1 else 0)) i j, which is not reducibly defeq to if i = j then 1 else 0, i think

[Riccardo Brasca]

Edward van de Meent said:

i.e. the goal contains (Matrix.of (fun x y => if x = y then 1 else 0)) i j, which is not reducibly defeq to if i = j then 1 else 0, i think

Yes,

theorem one : I R n = 1 := by
  with_reducible rfl

does not work.

[Riccardo Brasca]

@Emily Riehl my personal opinion is that, if you're doing mathematics and you don't want to enter into such technicalities, simp [h] in practice works well.

[Emily Riehl]

Thanks. This works now

theorem one : I R n = 1 := by
  ext i j
  unfold I
  rw [Matrix.of_apply]
  by_cases h : i = j
  · rw [if_pos h, h]
    simp
  · rw [if_neg h]
    simp [h]

as does

theorem one : I R n = 1 := by
  ext i j
  unfold I
  rw [Matrix.of_apply]
  by_cases h : i = j <;> rfl

[Emily Riehl]

Riccardo Brasca said:

Emily Riehl my personal opinion is that, if you're doing mathematics and you don't want to enter into such technicalities, simp [h] in practice works well.

It bothers me, though, that I still can't do very basic things in Lean because there are a lot of tactics I don't know (eg the if .. then .. else, which I've never used before, or case splitting over decidable equality). When things that I'm expecting to work (like rw or simp) get stuck then I'm very stuck.

[Emily Riehl]

Anyway I appreciate your help!

[Riccardo Brasca]

DecidableEq is rather simple. Just ignore it until Lean complains, and add it if needed (unless you want to write an algorithm that actually computes stuff, then you have to pay attention).

[Emily Riehl]

And actually --- more to the point this time --- I'm trying to prepare a sample proof for a talk for a non-math audience that illustrates what a formal proof looks like. So I'm trying to use more basic (read "human understandable") tactics.

[Edward van de Meent]

if you'd like to have a purely syntactic proof:

theorem one : I R n = 1 := by
  ext i j
  unfold I
  rw [Matrix.of_apply]
  by_cases h : i = j
  · rw [if_pos h, h, Matrix.one_apply_eq]
  · rw [if_neg h, Matrix.one_apply_ne h]

[Floris van Doorn]

If you have a subterm if ... then ... else ... in your goal (or hypotheses) you can also use the tactics split or split_ifs (which are similar)

[Kevin Buzzard]

Here's my effort:

import Mathlib

variable (R : Type) [Field R]
variable (n : Type) [DecidableEq n]

def I : Matrix n n R := Matrix.of (fun i j ↦ if i = j then 1 else 0)

theorem one : I R n = 1 := by
  unfold I
  ext i j
  -- look near the definition of `Matrix.one` in mathlib to see what the useful
  -- lemmas are called
  simp [Matrix.one_apply]

I was expecting to have to use split_ifs but I found the right lemma in the API.

[Eric Wieser]

of course, there's always

theorem one : I R n = 1 := by exact? -- rfl

which makes this not so ideal as a pedagogical example