DecidableEq in AlternatingMap

Stream: mathlib4

[Paul Schwahn]

Hi everyone,

I stumbled across a problem when trying to define an alternating map:

import Mathlib

open Matrix

variable {K : Type*} [Field K] {A : Matrix (Fin 3) (Fin 3) K}

def foo : (Fin 3 → K) [⋀^Fin 3]→ₗ[K] (Fin 3 → K) := {
  toFun := fun m ↦
    m 0 ×₃ (A *ᵥ (m 1 ×₃ m 2)) - ((A *ᵥ (m 0 ×₃ m 1)) ×₃ m 2 + m 1 ×₃ (A *ᵥ (m 0 ×₃ m 2)))
  map_update_add' := by
    intro _ m i x y
    fin_cases i
    · simp only [Fin.zero_eta, Fin.isValue, Function.update_self, map_add, ne_eq, one_ne_zero,
        not_false_eq_true, Function.update_of_ne, Fin.reduceEq, LinearMap.add_apply, mulVec_add]
      module
    sorry
    sorry
  map_update_smul' := sorry
  map_eq_zero_of_eq' := sorry
}

def bar : (Fin 3 → K) [⋀^Fin 3]→ₗ[K] (Fin 3 → K) := {
  toFun := fun m ↦
    m 0 ×₃ (A *ᵥ (m 1 ×₃ m 2)) - ((A *ᵥ (m 0 ×₃ m 1)) ×₃ m 2 + m 1 ×₃ (A *ᵥ (m 0 ×₃ m 2)))
  map_update_add' := by
    have : (2 : Fin 3) ≠ 0 := by
      simp
    intro _ m i x y
    fin_cases i
    · simp only [Fin.zero_eta, Function.update_self, Function.update_of_ne one_ne_zero, Function.update_of_ne this]
      simp only [LinearMap.add_apply, map_add, mulVec_add]
      module
    sorry
    sorry
  map_update_smul' := sorry
  map_eq_zero_of_eq' := sorry
}

def baz  : (Fin 3 → K) [⋀^Fin 3]→ₗ[K] (Fin 3 → K) := {
  toFun := fun m ↦
    m 0 ×₃ (A *ᵥ (m 1 ×₃ m 2)) - ((A *ᵥ (m 0 ×₃ m 1)) ×₃ m 2 + m 1 ×₃ (A *ᵥ (m 0 ×₃ m 2)))
  map_update_add' := by
    intro _ m i x y
    have : (2 : Fin 3) ≠ 0 := by
      simp
    fin_cases i
    · simp only [Fin.zero_eta, Function.update_self, Function.update_of_ne one_ne_zero, Function.update_of_ne this]
      simp only [LinearMap.add_apply, map_add, mulVec_add]
      module
    sorry
    sorry
  map_update_smul' := sorry
  map_eq_zero_of_eq' := sorry
}

The theorem foo should naively work (modulo sorrys), but it throws the following error:

(kernel) application type mismatch
  eq_false_of_decide (Eq.refl false)
argument has type
  false = false
but function has type
  decide (2 = 0) = false → (2 = 0) = False

It doesn't know how to decide 2 = 0. I believe the reason is that the assumptions of map_update_add' include [DecidableEq (Fin 3)], and this somehow clashes with the already existing instance. This is illustrated by the fact that bar works without issue, but baz doesn't.

Of course having to write have : (2 : Fin 3) ≠ 0 in front of everything is a bit awkward, and the fact that the error isn't flagged in the proof but in the theorem name... Do we have to live with this, or is there something else one could do?

[Aaron Liu]

lean4#7444

[Paul Schwahn]

Ah, cool, so for the record, the problem is not with the definition of AlternatingMap but with some simprocs. I upvoted the github issue.