feat: WF.GuessLex: If there is only one plausible measure, use it (le…

…anprover#2954)

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

@@ -569,18 +569,22 @@ 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
 
     -- The list of measures, including the measures that order functions.
     -- 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

tests/lean/guessLexFailures.lean

@@ -1,34 +1,37 @@
 /-!
 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
 
 
 -- The GuessLex code does not like eta-contracted motives in `casesOn`.
 -- 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

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

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

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