From 45e1300414560bdaac7a7d27efe983a22bd732fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Oct 2020 10:38:51 -0700 Subject: [PATCH] fix: nested structural recursion --- src/Lean/Elab/PreDefinition/Structural.lean | 8 ++++++-- tests/lean/run/nestedrec.lean | 12 ++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/nestedrec.lean diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index a9fe679a7c..413136090c 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/src/Lean/Elab/PreDefinition/Structural.lean @@ -231,8 +231,12 @@ let rec loop : Expr → Expr → MetaM Expr -- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them. let argsNonFixed := args.extract numFixed args.size -- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too. - let fArgs := argsNonFixed.iterate #[] fun i a fArgs => - if recArgInfo.pos == i.val || recArgInfo.indicesPos.contains i.val then fArgs else fArgs.push a + let fArgs := #[] + for i in [:argsNonFixed.size] do + if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then + let arg := argsNonFixed[i] + let arg ← replaceRecApps recFnName recArgInfo below arg + fArgs := fArgs.push arg pure $ mkAppN f fArgs else pure $ mkAppN (← loop below f) (← args.mapM (loop below)) diff --git a/tests/lean/run/nestedrec.lean b/tests/lean/run/nestedrec.lean new file mode 100644 index 0000000000..a25567d3d6 --- /dev/null +++ b/tests/lean/run/nestedrec.lean @@ -0,0 +1,12 @@ +#lang lean4 + +def f : Nat → Nat → Nat +| 0, b => b+1 +| a+1, b => f a (f a b) + +theorem ex1 (b) : f 0 b = b+1 := rfl +theorem ex2 (b) : f 1 b = (b+1)+1 := rfl +theorem ex3 (b) : f 2 b = b+1+1+1+1 := rfl +theorem ex4 (a b) : f (a+1) b = f a (f a b) := rfl + +#eval f 2 5