Unfolding a definition by pattern matching

Stream: general

[Paul van Wamelen]

Can someone please enlighten me on how to fill in the sorry here:

import data.matrix.basic

noncomputable theory
open_locale classical

universes u v
variables {n : Type u} [fintype n] {R : Type v} [comm_ring R]

def my_matrix (n : ℕ) : matrix (fin n) (fin n) R
| ⟨0, hn⟩ j := 0
| i j := 1

lemma my_matrix_def_not_the_first_row (n : ℕ) (i : fin n) (hn : 0 < n) (h0 : (⟨0, hn⟩ : fin n) ≠ i)
  (j : fin n) : (my_matrix n) i j = (1 : R) :=
begin
  sorry
  -- delta my_matrix,
end

delta my_matrix makes progress, but I'm still lost.
Is there a better/easier to work with way of defining something like my_matrix?

[Yakov Pechersky]

import data.matrix.basic

universes u v
variables {n : Type u} [fintype n] {R : Type v} [comm_ring R]

def my_matrix (n : ℕ) : matrix (fin (n + 1)) (fin (n + 1)) R :=
λ i _, if i = 0 then 0 else 1

lemma my_matrix_def_not_the_first_row (n : ℕ) (i j : fin (n + 1)) (ipos : 0 ≠ i) :
  (my_matrix n) i j = (1 : R) :=
by simp [my_matrix, ipos.symm]

[Yakov Pechersky]

A matrix is just a function "of two arguments", which in functional programming is a function that produces another function that produces a value

[Yakov Pechersky]

You won't be working with matrices of fin 0, so I already defined your my_matrix to work on matrices of dimenions at least 1.

[Yakov Pechersky]

That allows using the 0 that is available for all fin (n + 1). Additionally, it gets rid of the (hn : 0 < n) in your lemma

[Yakov Pechersky]

Then, in the proof, I can rw my_matrix, which makes it into an ite on some arbitrary i and j. I could have simp only to do beta reduction, then split_ifs to split into the i = 0 and i \ne 0 cases, show a contradiction in the first, etc... Or done rw if_neg ipos.symm to do that in one go... Or just do all of these steps in a single simp call like above.

[Kevin Buzzard]

Hey what have you got against the 0x0 matrix?

[Yakov Pechersky]

You're right Kevin. So here is a formalization following exactly the definition provided by Paul:

import data.matrix.basic

universes u v
variables {n : Type u} [fintype n] {R : Type v} [comm_ring R]

def my_matrix (n : ℕ) : matrix (fin n) (fin n) R
| ⟨0, hn⟩ j := 0
| i j := 1

lemma my_matrix_def_not_the_first_row (n : ℕ) (i : fin n) (hn : 0 < n) (h0 : (⟨0, hn⟩ : fin n) ≠ i)
  (j : fin n) : (my_matrix n) i j = (1 : R) :=
begin
  cases n,
  { exact fin_zero_elim i },
  { rcases i with _|i,
    { simpa using h0 },
    { rw my_matrix } }
end

[Yakov Pechersky]

Unfolding/rewriting an equation-compiler definition requires getting the expression where the definition is used to be in the same form as how the equation compiler has it.

[Yakov Pechersky]

So I break down the i into a ⟨0, _⟩ or ⟨i.succ, _⟩ form.

[Yakov Pechersky]

The first contradictory case can be discharged with either contradiction based on 0 < 0 or that having a term of fin 0 is already contradictory.

[Yakov Pechersky]

The second contradictory case is based on how inequality of subtypes means inequalities of values, so 0 ≠ 0 will follow from h0 . simpa takes care of discharging the goal with the contradiction.

[Yakov Pechersky]

Finally, the main case remains, which requires just the unfolding of the definition.

[Paul van Wamelen]

Wow, thanks for the detailed answer Yakov. This certainly taught me quite a few new tricks! I think I'll go with the ite definition, but it is good to know that the other definition is also workable.

[Filippo A. E. Nuccio]

Honestly, is the 0x0 matrix useful? Or was it a joke?

[Johan Commelin]

It's very useful in edge cases that would otherwise be very annoying.

[Kevin Buzzard]

It's not a joke at all. Is the zero-dimensional vector space useful? It's not like it's something which does not exist -- it's something which makes the theory complete. It's the kernel of an injective linear map. An endomorphism of that space is represented by a 0 x 0 matrix. It's an edge case, but it's no more an edge case than the idea that 0 is a natural number. The entire theory works and the proofs are all the same in the 0 x 0 case. It's nothing to be scared of :-) The trace is 0, the det is 1, the char poly is 1, the theorems in your linear algebra book are all true.

[Patrick Massot]

What about the zero-dimensional vector space over $\mathbb{F}_1$?

[Kevin Buzzard]

That's just Spec(Z) -> Spec(Z) as a toric variety, if my understanding is correct