Zulip Chat Archive

Stream: new members

Topic: dunfold vs delta


Yakov Pechersky (Jul 21 2020 at 06:16):

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 (Jul 21 2020 at 07:47):

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 (Jul 21 2020 at 07:48):

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 (Jul 21 2020 at 07:50):

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 (Jul 21 2020 at 07:50):

The equation lemmas will know what's really going on

Yakov Pechersky (Jul 21 2020 at 07:57):

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 (Jul 21 2020 at 08:20):

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

Kevin Buzzard (Jul 21 2020 at 08:21):

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

Kevin Buzzard (Jul 21 2020 at 08:21):

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

Yakov Pechersky (Jul 21 2020 at 08:26):

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

Reid Barton (Jul 21 2020 at 12:29):

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


Last updated: Dec 20 2023 at 11:08 UTC