Zulip Chat Archive

Stream: lean4

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 Mario Carneiro (Jan 23 2021 at 02:34):

You have to write this as a function which is structurally recursive, by first untupling

view this post on Zulip Mario Carneiro (Jan 23 2021 at 02:38):

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) := aux x.1 x.2
  where aux : (x : Nat) -> x < n -> List (Fin n)
  | 0, h => [⟨0, h⟩]
  | Nat.succ m, lt => Nat.succ m, lt :: aux m (Nat.ltTrans (Nat.ltSucc m) lt)

Last updated: May 07 2021 at 13:21 UTC