Zulip Chat Archive

Stream: new members

Topic: Induction on Dependent Pairs


view this post on Zulip Calvin Lee (Jan 23 2021 at 00:14):

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

view this post on Zulip Notification Bot (Jan 23 2021 at 02:32):

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


Last updated: May 10 2021 at 00:31 UTC