PR #7166 was green, mathlib built, I sent it to the queue, and it came back with a pretty tricky failure in the recursive theorem Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_denote_eq.

After some debugging I found out that the issue is in WF/Fix.lean, which I didn’t even change! But it seems by reordering the parameters I have uncovered a pre-existing bug:

/--
warning: declaration uses 'sorry'
---
error: application type mismatch
  congrArg (fun _a => _a = ⟨idx, h⟩) (x✝ n✝ (id sorry))
argument has type
  a = if hidx : idx < distance then ⟨idx, hidx⟩ else a
but function has type
  (a = if hidx : idx < distance then ⟨idx, hidx⟩ else a) →
    (fun _a => _a = ⟨idx, h⟩) a = (fun _a => _a = ⟨idx, h⟩) (if hidx : idx < distance then ⟨idx, hidx⟩ else a)
-/
#guard_msgs in
theorem demo (distance : Nat) (idx : Nat) (a : Fin distance) (fuel : Nat) :
    a = if hidx : idx < distance then Fin.mk idx hidx else a := by
  cases fuel
  · sorry
  next fuel =>
    split
    · rw [demo distance idx a fuel]
      sorry
    · rfl
termination_by fuel
decreasing_by sorry

The problem is that refining the induction hypothesis through the matcher introduced by split changes the type from

a = @dite (Fin distance) (idx < distance) (idx.decLt distance) (fun hidx => ⟨idx, hidx⟩) 

to

  a = @dite (Fin distance) (idx < distance) (isTrue h) (fun hidx => ⟨idx, hidx⟩) fun hidx => a

and that’s no longer type correct.

Tricky!

(A workaround is to do the rw before the split, but maybe I can find a fix.)

Versions

Lean 4.19.0-nightly-2025-03-04

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.