kernel deep recursion detected

Stream: mathlib4

[Gareth Ma]

Hello, when compiling the following code, I get a (kernel) deep recursion detected error message. What does it mean?

import Mathlib.LinearAlgebra.Determinant

example : (1 : Matrix (Fin 8) (Fin 8) ℚ).det = 1 := by
  rw [Matrix.det_one]

I'm on Mathlib v4.10.0-rc2

[Gareth Ma]

Same error message on the lean interactive playground thing

[Eric Wieser]

You get slightly better diagnostics with

import Mathlib.LinearAlgebra.Determinant

example : (1 : Matrix (Fin 8) (Fin 8) ℚ).det = 1 := by
  have := Matrix.det_one (n := Fin 8) (R := ℚ)
  exact this

[Daniel Weber]

even making everything fully explicit it still fails :thinking:

import Mathlib.LinearAlgebra.Determinant

set_option pp.all true

#check @Matrix.det_one (Fin 8) (instDecidableEqFin 8) (Fin.fintype 8) ℚ Rat.commRing

example : @Eq.{1} Rat
  (@Matrix.det.{0, 0} (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))
    (instDecidableEqFin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))
    (Fin.fintype (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) Rat Rat.commRing
    (@OfNat.ofNat.{0}
      (Matrix.{0, 0, 0} (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))
        Rat)
      1
      (@One.toOfNat1.{0}
        (Matrix.{0, 0, 0} (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))
          (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) Rat)
        (@Matrix.one.{0, 0} (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) Rat
          (instDecidableEqFin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))
          (@CommMonoidWithZero.toZero.{0} Rat
            (@CommSemiring.toCommMonoidWithZero.{0} Rat (@CommRing.toCommSemiring.{0} Rat Rat.commRing)))
          (@Semiring.toOne.{0} Rat
            (@CommSemiring.toSemiring.{0} Rat (@CommRing.toCommSemiring.{0} Rat Rat.commRing)))))))
  (@OfNat.ofNat.{0} Rat 1
    (@One.toOfNat1.{0} Rat
      (@Semiring.toOne.{0} Rat (@CommSemiring.toSemiring.{0} Rat (@CommRing.toCommSemiring.{0} Rat Rat.commRing))))) := @Matrix.det_one.{0, 0} (Fin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) (instDecidableEqFin (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) (Fin.fintype (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8))) Rat Rat.commRing

[Daniel Weber]

This also fails for 5x5 matrices, but not before that

[Daniel Weber]

Making Matrix.det irreducible makes it work for 5x5, 6x6 and 7x7, but 8x8now gives (kernel) deep recursion detected

[Daniel Weber]

import Mathlib.LinearAlgebra.Determinant

example : (1 : Matrix (Fin 8) (Fin 8) ℤ).det = 1 := by
  unfold Matrix.det Matrix.detRowAlternating MultilinearMap.alternatization
  sorry

this also gives deep recursion detected

[Daniel Weber]

Daniel Weber said:

import Mathlib.LinearAlgebra.Determinant

example : (1 : Matrix (Fin 8) (Fin 8) ℤ).det = 1 := by
  unfold Matrix.det Matrix.detRowAlternating MultilinearMap.alternatization
  sorry

this also gives deep recursion detected

I'm not sure what causes this, but turning pp.all on here even for Fin 2 you get a huge expression

[Daniel Weber]

I managed to edit MultilinearMap.alternatization to fix this, I'll make a pull request

[Daniel Weber]

#15045

[Daniel Weber]

Daniel Weber said:

#15045

any ideas why this works?

[Gareth Ma]

I got another erronous code also with recursion error (not kernel error), seems to be the same bug though since it also triggers for n >= 5.

import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

local notation "n" => 5

def M : Matrix (Fin n) (Fin n) ℚ := sorry

theorem E8_det_eq_one : M.det = 1 :=
  -- "manual rref (laughing as I type this)"
  let c0 : Fin n → ℚ := ![1, 0, 0, 0, 0]
  let c1 : Fin n → ℚ := ![0, 1, 0, 0, 0]
  have h₁ := congrArg (fun f ↦ c1 1 • f) (Matrix.det_updateRow_sum M 0 c0)
  have h₂ := Matrix.det_updateRow_sum (M.updateRow 0 (∑ k, c0 k • M k)) 1 c1
  have := h₂.trans h₁
  sorry

Let me try your fix. If it works, I will prefer it to be merged as soon as possible :D

[Gareth Ma]

image.png

It does work!

[Gareth Ma]

(within your PR)

[Eric Wieser]

I wonder if making alternatization an irreducible_def is a better choice?

[Daniel Weber]

Eric Wieser said:

I wonder if making alternatization an irreducible_def is a better choice?

I tried this, but it doesn't fix the problem, surprisingly

[Daniel Weber]

this works, but I think it's much worse than what I'm doing in the PR.

opaque alternatization' : {b : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' //
  ∀ m, ⇑(b m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ : _)} :=
  ⟨{
    toFun := fun m ↦
      { ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ with
      toFun := ⇑(∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ)
      map_eq_zero_of_eq' := fun v i j hvij hij =>
        alternization_map_eq_zero_of_eq_aux m v i j hij hvij }
    map_add' := fun a b ↦ by
      ext
      simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply, add_apply,
        smul_add, Finset.sum_add_distrib, AlternatingMap.add_apply]
    map_zero' := by
      ext
      simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply,
        zero_apply, smul_zero, Finset.sum_const_zero, AlternatingMap.zero_apply]
  }, fun n ↦ rfl⟩

def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' :=
  alternatization'.1

[Yakov Pechersky]

Seems like a problem in the reduction of Fintype and finset. Does it work if you define it as a finsum instead? I don't know if those reduce, I assume not

[Eric Wieser]

Daniel Weber said:

this works, but I think it's much worse than what I'm doing in the PR.

opaque alternatization' : {b : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' //
  ∀ m, ⇑(b m) = (∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ : _)} :=sorry

def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' :=
  alternatization'.1

Isn't this precisely what irreducible_def does? Are you sure you didn't misread my suggestion as @[irreducible] def?

[Daniel Weber]

Oh, I have. But using irreducible_def collides with the existing docs#MultilinearMap.alternatization_def

[Eric Wieser]

That should probably be called alternatization_coeFn or coeFn_alternatization

[Eric Wieser]

Yakov Pechersky said:

Seems like a problem in the reduction of Fintype and finset.

I would guess that Finset.univ : Finset (Perm ι) is producing a very large term that the kernel is tricked into reducing

[Yakov Pechersky]

Right, so I hoped that Finset.univ.toSet_finite would possibly avoid it.

[David Renshaw]

How about mathlib4#30560?

[Oliver Nash]

I see three PRs related to this discussion:

1. #15045
2. #30560
3. #30562

Can @Daniel Weber or @David Renshaw save me a few minutes by quickly commenting about whether we with to pursue the approaches in these?

[David Renshaw]

If mathlib4#33590 solves the problem then I am okay with my PRs being closed.

[Oliver Nash]

Thank @David Renshaw. I think we still do need your work since #33590 doesn't solve the root cause (though it does contain the problem a bit better).

I was really just asking in case you could quickly tell me if you felt #30562 dominates #30560 or whether we should aim to add both.

But I'm happy to get to these in the course of the normal review cycle.

[Eric Wieser]

I think you didn't mean docs :)

[Eric Wieser]

My take is that #30562 is probably the most principled solution