dunfold vs delta

Stream: new members

[Yakov Pechersky]

Why can't dunfold be used in this proof? I'm able to dunfold det' in other proofs. Using delta gives me a nasty nat.brec statement that I am struggling with.

import data.matrix.notation

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (A : matrix (fin n) (fin n) R)

open_locale matrix big_operators
open matrix

def det' {R : Type*} [field R] :
    Π {n : ℕ}, matrix (fin n) (fin n) R -> fin n -> R
| 0 _ _ := 1
| 1 M i := M i i
| (n + 2) M ⟨0, h⟩ := ∑ j, (M 0 j * (-1 : R) ^ (j.val) * det' (minor M (fin.succ_above ⟨0, h⟩) (fin.succ_above j)) 0)
| (n + 2) M ⟨k + 1, hk⟩ := ∑ j, (M ⟨k + 1, hk⟩ j * (-1 : R) ^ (k + 1 + j.val) * det' (minor M (fin.succ_above ⟨k + 1, hk⟩) (fin.succ_above j))
      ⟨k, (add_lt_add_iff_right 1).mp hk⟩
      )

lemma det_eq_det {i j} (h : i ≠ j) : det' A i = det' A j :=
begin
  induction n with n hn,
  { exact fin.elim0 i },
  delta det', -- why can't dunfold be used here
  simp,
end

[Kevin Buzzard]

I'm not near Lean right now but presumably it has to do with the fact that you have a lot of cases in your equation compiler definition and Lean does not always do what you expect in these situations

[Kevin Buzzard]

I would have a good look at the actual equation lemmas generated by your definition. Those are the lemmas which "get you started" as it were

[Kevin Buzzard]

Sometimes you have to case on more things than you might expect eg you define f(a,b) by f(0,n), f(succ m,0) and f(succ m, succ n) and then it turns out that f(0,n) is not definitionally what you told it to be because the equation compiler did another case split internally into f(0,0) and f(0,succ n)

[Kevin Buzzard]

The equation lemmas will know what's really going on

[Yakov Pechersky]

By equation lemmas, do you mean something like

@[simp] lemma det_zero_eq_one (A : matrix (fin 0) (fin 0) R) {i} : det' A i = 1 := rfl

@[simp] lemma det_one_eq_elem (A : matrix (fin 1) (fin 1) R) {i} : det' A i = A i i := rfl

@[simp] lemma det_laplace_zero (A : matrix (fin (n + 2)) (fin (n + 2)) R) {h : 0 < n + 2} :
  det' A ⟨0, h⟩ = ∑ j, (A 0 j * (-1 : R) ^ (j.val) * det' (minor A (fin.succ_above ⟨0, h⟩) (fin.succ_above j)) 0) := rfl

@[simp] lemma det_laplace_nonzero (A : matrix (fin (n + 2)) (fin (n + 2)) R) {i} {h : i + 1 < n + 2} {nz : i ≠ 0}:
  det' A ⟨i + 1, h⟩ = ∑ j, (A ⟨i + 1, h⟩ j * (-1 : R) ^ (i + 1 + j.val) * det' (minor A (fin.succ_above ⟨i + 1, h⟩) (fin.succ_above j))
      ⟨i, (add_lt_add_iff_right 1).mp h⟩) := rfl

[Kevin Buzzard]

I mean #print prefix det' and look at all the auto generated stuff with weird names containing the string equation

[Kevin Buzzard]

All this unfold and dunfold and Delta stuff is using these things under the hood

[Kevin Buzzard]

And here you can see exactly what lean thinks is true about det'

[Yakov Pechersky]

Cool! Yeah, the lemmas I wrote out are basically what comes out of that #print statement.

[Reid Barton]

Indeed, dunfold wants to apply equational lemmas, but there are none that could apply to det' A i = det' A j.