Zulip Chat Archive
Stream: lean4
Topic: Induction on Dependent Pairs
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
Mario Carneiro (Jan 23 2021 at 02:34):
You have to write this as a function which is structurally recursive, by first untupling
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: Dec 20 2023 at 11:08 UTC