Induction on Dependent Pairs

Stream: new members

[Calvin Lee]

I'm trying to write a function that will generate all elements of Fin n for any n. To do that I wrote a helper inductive function on Fin n that would return all the elements of Fin n below a certain value. However, even though the first element of the pair decreases, lean cannot prove termination. Is there anything I can do to remedy this? This is the failing function

theorem Nat.ltSucc : (n : Nat) -> Less n (Nat.succ n)
  | 0               => rfl
  | n'@(Nat.succ n) => ltSucc n

def allBelow {n : Nat} : (x : Fin n) -> List (Fin n)
  | x@⟨0, _⟩ => [x]
  | x@⟨Nat.succ m, lt⟩ => x :: allBelow ⟨m, Nat.ltTrans (Nat.ltSucc m) lt⟩

I'm using lean 4 nightly and the specific error is

error: fail to show termination for
  allBelow
with errors
structural recursion cannot be used

well founded recursion has not been implemented yet

[Notification Bot]

This topic was moved by Mario Carneiro to #lean4 > Induction on Dependent Pairs