fix: GuessLex: also look for negations of Nat comparisons (#8321)

This PR lets the termination argument inference consider negations of
Nat comparisons. Fixes #8257.

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -364,19 +364,22 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedParamPerms : FixedParamP
       RecCallWithContext.create (← getRef) caller callerParams callee calleeArgs
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
-def isNatCmp (e : Expr) : MetaM (Option (Expr × Expr)) := withReducible do
-  let (α, e₁, e₂) ←
-    match_expr e with
-    | LT.lt α _ e₁ e₂ => pure (α, e₁, e₂)
-    | LE.le α _ e₁ e₂ => pure (α, e₁, e₂)
-    | GT.gt α _ e₁ e₂ => pure (α, e₂, e₁)
-    | GE.ge α _ e₁ e₂ => pure (α, e₂, e₁)
-    | _ => return none
+partial def isNatCmp (e : Expr) : MetaM (Option (Expr × Expr)) := withReducible do
+  match_expr e with
+  | Not e' => Option.map (Prod.swap) <$> isNatCmp e'
+  | _ =>
+    let (α, e₁, e₂) ←
+      match_expr e with
+      | LT.lt α _ e₁ e₂ => pure (α, e₁, e₂)
+      | LE.le α _ e₁ e₂ => pure (α, e₁, e₂)
+      | GT.gt α _ e₁ e₂ => pure (α, e₂, e₁)
+      | GE.ge α _ e₁ e₂ => pure (α, e₂, e₁)
+      | _ => return none
 
-  if (←isDefEq α (mkConst ``Nat)) then
-    return some (e₁, e₂)
-  else
-    return none
+    if (←isDefEq α (mkConst ``Nat)) then
+      return some (e₁, e₂)
+    else
+      return none
 
 def complexMeasures (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
     (userVarNamess : Array (Array Name)) (recCalls : Array RecCallWithContext) :

tests/lean/guessLexDiff.lean.expected.out

@@ -24,19 +24,20 @@ Cannot use parameter i:
 Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-            i #1 #2 i + i
-1) 85:26-38 =  =  =     =
-2) 85:58-76 ?  <  _     _
-3) 85:26-38 =  =  =     =
-4) 88:26-42 _  <  _     _
-5) 88:26-42 ?  ≤  ≤     ?
-6) 88:26-42 _  <  _     _
-7) 88:26-42 _  <  _     _
-8) 88:26-42 _  <  _     _
-9) 97:8-20  _  <  _     _
+            i #1 #2 i + 1 0 - i #3 i + i
+1) 85:26-38 =  =  =     =     =  =     =
+2) 85:58-76 ?  <  _     _     _  _     _
+3) 85:26-38 =  =  =     =     =  =     =
+4) 88:26-42 _  <  _     _     _  _     _
+5) 88:26-42 ?  ≤  ≤     ?     ≤  ≤     ?
+6) 88:26-42 _  <  _     _     _  _     _
+7) 88:26-42 _  <  _     _     _  _     _
+8) 88:26-42 _  <  _     _     _  _     _
+9) 97:8-20  _  <  _     _     _  _     _
 
 #1: xs.size - i
 #2: xs.size - (i + 1)
+#3: 42 - i
 
 Please use `termination_by` to specify a decreasing measure.
 guessLexDiff.lean:102:4-102:18: error: fail to show termination for
@@ -57,45 +58,49 @@ Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
 Call from mutual_failure to mutual_failure2 at 104:4-24:
-   i #1 #2
-i  =  ?  ?
-#3 ?  =  ?
+   i #1 #2 i + 1
+i  =  ?  ?     <
+#3 ?  =  ?     ?
 Call from mutual_failure to mutual_failure2 at 104:52-78:
-   i #1 #2
-i  ?  _  _
-#3 _  <  _
+   i #1 #2 i + 1
+i  ?  _  _     =
+#3 _  <  _     _
 Call from mutual_failure to mutual_failure2 at 104:4-24:
-   i #1 #2
-i  _  _  _
-#3 _  =  _
+   i #1 #2 i + 1
+i  _  _  _     <
+#3 _  =  _     _
 Call from mutual_failure to mutual_failure2 at 111:4-28:
-   i #1 #2
-i  _  _  _
-#3 _  <  _
+   i #1 #2 i + 1
+i  _  _  _     =
+#3 _  <  _     _
 Call from mutual_failure to mutual_failure2 at 117:8-28:
-   i #1 #2
-i  _  _  _
-#3 _  ?  _
+   i #1 #2 i + 1
+i  _  _  _     <
+#3 _  ?  _     _
 Call from mutual_failure2 to mutual_failure at 123:4-23:
-   i #3
-i  _  _
-#1 _  _
-#2 _  _
+      i #3
+i     _  _
+#1    _  _
+#2    _  _
+i + 1 ?  _
 Call from mutual_failure2 to mutual_failure at 123:50-75:
-   i #3
-i  _  _
-#1 _  _
-#2 _  _
+      i #3
+i     _  _
+#1    _  _
+#2    _  _
+i + 1 _  _
 Call from mutual_failure2 to mutual_failure at 127:4-27:
-   i #3
-i  _  _
-#1 _  _
-#2 _  _
+      i #3
+i     _  _
+#1    _  _
+#2    _  _
+i + 1 _  _
 Call from mutual_failure2 to mutual_failure at 133:8-27:
-   i #3
-i  _  _
-#1 _  _
-#2 _  _
+      i #3
+i     _  _
+#1    _  _
+#2    _  _
+i + 1 _  _
 
 
 #1: xs.size - i

tests/lean/run/issue8257.lean

@@ -0,0 +1,35 @@
+/-- info: Try this: termination_by xs.length / 2 - i -/
+#guard_msgs in
+def foo (xs : String) (i : Nat) (a b : String.Iterator) : Bool :=
+  if xs.length / 2 ≤ i then
+    true
+  else if a.curr ≠ b.curr then
+    false
+  else
+    foo xs (i + 1) a.next b.prev
+termination_by?
+
+/-- info: Try this: termination_by xs.length / 2 - i -/
+#guard_msgs in
+def bar (xs : String) (i : Nat) (a b : String.Iterator) : Bool :=
+  if i < xs.length / 2 then
+    if a.curr ≠ b.curr then
+      false
+    else
+      bar xs (i + 1) a.next b.prev
+  else
+    true
+termination_by?
+
+
+/-- info: Try this: termination_by xs.length / 2 - i -/
+#guard_msgs in
+def baz (xs : String) (i : Nat) (a b : String.Iterator) : Bool :=
+  if ¬ (i < xs.length / 2) then
+    true
+  else
+    if a.curr ≠ b.curr then
+      false
+    else
+      baz xs (i + 1) a.next b.prev
+termination_by?