From ffbea840bfca68e682f1d4456e763df3f336875a Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 27 Nov 2023 23:41:40 +0100 Subject: [PATCH] feat: WF.GuessLex: If there is only one plausible measure, use it (#2954) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If here is only one plausible measure, there is no point having the `GuessLex` code see if it is terminating, running all the tactics, only for the `MkFix` code then run the tactics again. So if there is only one plausible measure (non-mutual recursion with only one varying parameter), just use that measure. Side benefit: If the function isn’t terminating, more detailed error messages are shown (failing proof goals), located at the recursive calls. --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 14 +++++++---- tests/lean/guessLexFailures.lean | 23 +++++++++++-------- tests/lean/guessLexFailures.lean.expected.out | 14 +++++++---- tests/lean/run/guessLex.lean | 10 +++++--- .../lean/terminationFailure.lean.expected.out | 7 +++++- 5 files changed, 44 insertions(+), 24 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index f12a0bbadc..e74aaa3394 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -569,11 +569,6 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) let arities := varNamess.map (·.size) trace[Elab.definition.wf] "varNames is: {varNamess}" - -- Collect all recursive calls and extract their context - let recCalls ←collectRecCalls unaryPreDef fixedPrefixSize arities - let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) - let callMatrix := rcs.map (inspectCall ·) - let forbiddenArgs ← preDefs.mapM fun preDef => getForbiddenByTrivialSizeOf fixedPrefixSize preDef @@ -581,6 +576,15 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) -- The function ordering measures come last let measures ← generateMeasures forbiddenArgs arities + -- If there is only one plausible measure, use that + if let #[solution] := measures then + return ← buildTermWF (preDefs.map (·.declName)) varNamess #[solution] + + -- Collect all recursive calls and extract their context + let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize arities + let rcs ← recCalls.mapM (RecCallCache.mk decrTactic? ·) + let callMatrix := rcs.map (inspectCall ·) + match ← liftMetaM <| solve measures callMatrix with | .some solution => do let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution diff --git a/tests/lean/guessLexFailures.lean b/tests/lean/guessLexFailures.lean index 28e7bff8d5..b7f745d019 100644 --- a/tests/lean/guessLexFailures.lean +++ b/tests/lean/guessLexFailures.lean @@ -1,17 +1,20 @@ /-! A few cases where guessing the lexicographic order fails, and where we want to keep tabs on the output. + +All functions take more than one changing argument, because the guesslex +code skips non-mutuals unary functions with only one plausible measure. -/ -def nonTerminating : Nat → Nat - | 0 => 0 - | n => nonTerminating (.succ n) +def nonTerminating : Nat → Nat → Nat + | 0, _ => 0 + | n, m => nonTerminating (.succ n) (.succ m) -- Saying decreasing_by forces Lean to use structural recursion, which gives a different -- error message -def nonTerminating2 : Nat → Nat - | 0 => 0 - | n => nonTerminating2 (.succ n) +def nonTerminating2 : Nat → Nat → Nat + | 0, _ => 0 + | n, m => nonTerminating2 (.succ n) (.succ m) decreasing_by decreasing_tactic @@ -19,16 +22,16 @@ decreasing_by decreasing_tactic -- At the time of writing, the error message is swallowed -- When guessing the lexicographic order becomes more verbose this will improve. def FinPlus1 n := Fin (n + 1) -def badCasesOn (n : Nat) : Fin (n + 1) := - Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n)) +def badCasesOn (n m : Nat) : Fin (n + 1) := + Nat.casesOn (motive := FinPlus1) n (⟨0,Nat.zero_lt_succ _⟩) (fun n => Fin.succ (badCasesOn n (.succ m))) decreasing_by decreasing_tactic -- termination_by badCasesOn n => n -- Like above, but now with a `casesOn` alternative with insufficient lambdas def Fin_succ_comp (f : (n : Nat) → Fin (n + 1)) : (n : Nat) → Fin (n + 2) := fun n => Fin.succ (f n) -def badCasesOn2 (n : Nat) : Fin (n + 1) := +def badCasesOn2 (n m : Nat) : Fin (n + 1) := Nat.casesOn (motive := fun n => Fin (n + 1)) n (⟨0,Nat.zero_lt_succ _⟩) - (Fin_succ_comp (fun n => badCasesOn2 n)) + (Fin_succ_comp (fun n => badCasesOn2 n (.succ m))) decreasing_by decreasing_tactic -- termination_by badCasesOn2 n => n diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index d170019599..5890ef5bf3 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -1,13 +1,17 @@ -guessLexFailures.lean:8:9-8:33: error: fail to show termination for +guessLexFailures.lean:11:12-11:46: error: fail to show termination for nonTerminating with errors argument #1 was not used for structural recursion failed to eliminate recursive application - nonTerminating (Nat.succ n) + nonTerminating (Nat.succ n) (Nat.succ m) + +argument #2 was not used for structural recursion + failed to eliminate recursive application + nonTerminating (Nat.succ n) (Nat.succ m) structural recursion cannot be used failed to prove termination, use `termination_by` to specify a well-founded relation -guessLexFailures.lean:12:0-15:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation -guessLexFailures.lean:22:0-24:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation -guessLexFailures.lean:30:0-33:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:15:0-18:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:25:0-27:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation +guessLexFailures.lean:33:0-36:31: error: failed to prove termination, use `termination_by` to specify a well-founded relation diff --git a/tests/lean/run/guessLex.lean b/tests/lean/run/guessLex.lean index 993ccddc1b..5ff67864b1 100644 --- a/tests/lean/run/guessLex.lean +++ b/tests/lean/run/guessLex.lean @@ -3,6 +3,9 @@ This files tests Lean's ability to guess the right lexicographic order. TODO: Once lean spits out the guessed order (probably guarded by an option), turn this on and check the output. + +When writing tests for GuesLex, keep in mind that it doesn't do anything +when there is only one plausible measure (one function, only one varying argument). -/ def ackermann (n m : Nat) := match n, m with @@ -78,11 +81,12 @@ def blowup : Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat -- unpacking of packed n-ary arguments def confuseLex1 : Nat → @PSigma Nat (fun _ => Nat) → Nat | 0, _p => 0 - | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x,y⟩ + | .succ n, ⟨x,y⟩ => confuseLex1 n ⟨x, .succ y⟩ def confuseLex2 : @PSigma Nat (fun _ => Nat) → Nat - | ⟨_y,0⟩ => 0 - | ⟨y,.succ n⟩ => confuseLex2 ⟨y,n⟩ + | ⟨_,0⟩ => 0 + | ⟨0,_⟩ => 0 + | ⟨.succ y,.succ n⟩ => confuseLex2 ⟨y,n⟩ def dependent : (n : Nat) → (m : Fin n) → Nat | 0, i => Fin.elim0 i diff --git a/tests/lean/terminationFailure.lean.expected.out b/tests/lean/terminationFailure.lean.expected.out index 2966b4cc4d..dae6521399 100644 --- a/tests/lean/terminationFailure.lean.expected.out +++ b/tests/lean/terminationFailure.lean.expected.out @@ -18,6 +18,11 @@ argument #1 was not used for structural recursion structural recursion cannot be used -failed to prove termination, use `termination_by` to specify a well-founded relation +failed to prove termination, possible solutions: + - Use `have`-expressions to prove the remaining goals + - Use `termination_by` to specify a different well-founded relation + - Use `decreasing_by` to specify your own tactic for discharging this kind of goal +x : Nat +⊢ False h (x : Nat) : Foo Foo.a