leanprover
split fails with non-fvar discriminants and dependent motives
Consider this
/--
error: Tactic `split` failed: Could not split an `if` or `match` expression in the goal
n : Nat
⊢ Fin.last n =
match id n with
| 0 => Fin.last 0
| n.succ => Fin.last (n + 1)
-/
#guard_msgs(pass trace, all) in
example (n : Nat) : Fin.last n = match (motive := ∀ n, Fin (n+1)) id n with
| 0 => Fin.last 0
| n + 1 => Fin.last (n + 1) := by
split <;> rfl
it works if the discriminant id n were a simple variable n.
This seems to be the core issue of underlying #10195, and is blocking #10268 and similar constructions.
Versions
Lean 4.25.0-nightly-2025-09-16
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
PR #10425 is an attempt to fix this at least for discriminants that are proofs, maybe good enough to unblock #10268.
It may be possible to push further on this if split, when it’s generalizing a discriminant that’s dependent, fixes the type up by wrapping the match statement in something like
h.symm.ndrec (motive := fun n => Fin (n + 1)) (match …)
where h is the assumed equality. In nice cases (e.g. if the discriminant is a constructor and the subsequent Cases.unifyEqs? takes care of this) this might just work nicely. In other cases it may leave casts around but at least not fail the split. Not sure how horrible the ndrec call here gets if the motive has multiple arguments it’s dependent on.