861f722844
This PR fixes a panic when compiling mutually recursive definitions that use `casesOn` on indexed inductive types (e.g. `Vect`). The `splitMatchOrCasesOn` function in `WF.Unfold` asserted `matcherInfo.numDiscrs = 1`, but for indexed types the casesOn recursor has multiple discriminants (indices + major premise). The fix uses the last discriminant (the major premise) and lets the `cases` tactic handle index discriminants automatically. Closes #13015 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
24 lines
983 B
Text
24 lines
983 B
Text
-- Mutually recursive definitions using casesOn on indexed types should not panic.
|
||
-- https://github.com/leanprover/lean4/issues/13015
|
||
|
||
inductive Vect (α : Type u) : Nat → Type u
|
||
| nil : Vect α 0
|
||
| cons : α → {n : Nat} → Vect α n → Vect α (n+1)
|
||
|
||
mutual
|
||
def zipWithAux (f : α → β → γ) (a : α) (as : Vect α m) (bs : Vect β n) : n = m + 1 → γ × Vect γ m :=
|
||
Vect.casesOn (motive := λ k _ ↦ k = m + 1 → γ × Vect γ m) bs
|
||
(nil := λ h ↦ Nat.noConfusion h)
|
||
(cons := λ (b : β) (k : Nat) (bs : Vect β k) h ↦
|
||
Nat.noConfusion h (λ h1 : k = m ↦
|
||
((f a b), (zipWith f as (h1 ▸ bs) rfl)))
|
||
)
|
||
|
||
def zipWith (f : α → β → γ) {n : Nat} (as : Vect α n) (bs : Vect β n) : n = n → Vect γ n :=
|
||
Vect.casesOn (motive := λ m _ ↦ n = m → Vect γ m) as
|
||
(nil := λ _ ↦ Vect.nil)
|
||
(cons := λ (a : α) (m : Nat) (as : Vect α m) h ↦
|
||
let p := zipWithAux f a as bs h
|
||
Vect.cons p.1 p.2
|
||
)
|
||
end
|