From 127776288bfdaeed3b6fa10e30329d2746e6b1ea Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 13 May 2025 17:10:19 +0200 Subject: [PATCH] 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 | 27 +++--- tests/lean/guessLexDiff.lean.expected.out | 87 +++++++++++--------- tests/lean/run/issue8257.lean | 35 ++++++++ 3 files changed, 96 insertions(+), 53 deletions(-) create mode 100644 tests/lean/run/issue8257.lean diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index a565214934..5bcffd6ec1 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/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) : diff --git a/tests/lean/guessLexDiff.lean.expected.out b/tests/lean/guessLexDiff.lean.expected.out index 2b017593ba..3bf1b68116 100644 --- a/tests/lean/guessLexDiff.lean.expected.out +++ b/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 diff --git a/tests/lean/run/issue8257.lean b/tests/lean/run/issue8257.lean new file mode 100644 index 0000000000..d771a7157f --- /dev/null +++ b/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?