From 2c8fb9d3fcd933d729dbdc9a10f3e345bf287b38 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Wed, 5 Mar 2025 18:15:49 +0000 Subject: [PATCH] fix: strip optional parameters when elaborating the termination hints (#7335) This PR modifies `elabTerminationByHints` in a way that the type of the recursive function used for elaboration of the termination measure is striped of from optional parameters. It prevents introducing dependencies between the default values for arguments, that can cause the termination checker to fail. Closes https://github.com/leanprover/lean4/issues/6351. --- src/Lean/Elab/PreDefinition/TerminationMeasure.lean | 3 +-- tests/lean/run/issue6531.lean | 9 +++++++++ 2 files changed, 10 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/issue6531.lean diff --git a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean index de827c16e7..5ea783ca6d 100644 --- a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean +++ b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean @@ -52,7 +52,6 @@ Elaborates a `TerminationBy` to an `TerminationMeasure`. def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat) (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do assert! extraParams ≤ arity - if h : hint.vars.size > extraParams then let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++ m!"{funName} only binds {parameters extraParams}." @@ -64,7 +63,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : -- Bring parameters before the colon into scope let r ← withoutErrToSorry <| - forallBoundedTelescope type (arity - extraParams) fun ys type' => do + forallBoundedTelescope (cleanupAnnotations := true) type (arity - extraParams) fun ys type' => do -- Bring the variables bound by `termination_by` into scope. elabFunBinders hint.vars (some type') fun xs type' => do -- Elaborate the body in this local environment diff --git a/tests/lean/run/issue6531.lean b/tests/lean/run/issue6531.lean new file mode 100644 index 0000000000..e82d8473f2 --- /dev/null +++ b/tests/lean/run/issue6531.lean @@ -0,0 +1,9 @@ +-- This used to cause +-- error: The termination argument's type must not depend on the function's varying parameters + +def foo (as : Array Nat) (i := 0) (j := as.size - 1) : Array Nat := + if j ≤ i then as + else + let newas := as.set! 0 0 + foo newas (i+1) (j-1) +termination_by j - i