From 9c00a5933944bbc4801079777dd9fcc326e66390 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 27 Feb 2024 19:53:36 +0100 Subject: [PATCH] feat: use omega in default decreasing_trivial (#3503) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit with this, more functions will be proven terminating automatically, namely those where after `simp_wf`, lexicographic order handling, possibly `subst_vars` the remaining goal can be solved by `omega`. Note that `simp_wf` already does simplification of the goal, so this adds `omega`, not `(try simp) <;> omega` here. There are certainly cases where `(try simp) <;> omega` will solve more goals (e.g. due to the `subst_vars` in `decreasing_with`), and `(try simp at *) <;> omega` even more. This PR errs on the side of taking smaller steps. Just appending `<;> omega` to the existing `simp (config := { arith := true, failIfUnchanged := false })` call doesn’t work nicely, as that leaves forms like `Nat.sub` in the goal that `omega` does not seem to recognize. This does *not* remove any of the existing ad-hoc `decreasing_trivial` rules based on `apply` and `assumption`, to not regress over the status quo (these rules may apply in cases where `omega` wouldn't “see” everything, but `apply` due to defeq works). Additionally, just extending makes bootstrapping easier; early in `Init` where `omega` does not work yet these other tactics can still be used. (Using a single `omega`-based tactic was tried in #3478 but isn’t quite possible yet, and will be postponed until we have better automation including forward reasoning.) --- src/Init/WFTactics.lean | 3 ++- tests/lean/guessLexFailures.lean.expected.out | 16 ++++++++-------- tests/lean/letRecMissingAnnotation.lean | 8 -------- .../letRecMissingAnnotation.lean.expected.out | 8 -------- tests/lean/run/wfOmega.lean | 4 ++++ tests/lean/wf1.lean.expected.out | 2 +- 6 files changed, 15 insertions(+), 26 deletions(-) delete mode 100644 tests/lean/letRecMissingAnnotation.lean delete mode 100644 tests/lean/letRecMissingAnnotation.lean.expected.out create mode 100644 tests/lean/run/wfOmega.lean diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 250585721c..da46d6daaf 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -22,7 +22,8 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith) -/ syntax "decreasing_trivial" : tactic -macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })); done) +macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })) <;> done) +macro_rules | `(tactic| decreasing_trivial) => `(tactic| omega) macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption) macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out index 1fb51ba40e..ca6d94d2d1 100644 --- a/tests/lean/guessLexFailures.lean.expected.out +++ b/tests/lean/guessLexFailures.lean.expected.out @@ -40,7 +40,7 @@ The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) x1 x2 x3 1) 29:6-25 = = = -2) 30:6-23 = ? < +2) 30:6-23 = < _ 3) 31:6-23 < _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure. @@ -48,7 +48,7 @@ The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) x1 x2 x3 x4 1) 39:6-27 = = _ = -2) 40:6-25 = ? _ < +2) 40:6-25 = < _ _ 3) 41:6-25 < _ _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure. @@ -56,7 +56,7 @@ The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) n m l 1) 50:6-25 = = = -2) 51:6-23 = ? < +2) 51:6-23 = < _ 3) 52:6-23 < _ _ Please use `termination_by` to specify a decreasing measure. guessLexFailures.lean:59:6-59:7: error: fail to show termination for @@ -74,16 +74,16 @@ Call from Mutual.f to Mutual.f at 61:8-33: = = = Call from Mutual.f to Mutual.f at 62:8-31: n m l - = ? < + = < < Call from Mutual.f to Mutual.g at 63:8-39: n m l -n < _ ? -m ? _ ? +n < ? ? +m ? = ? H _ _ _ -l ? _ < +l ? ? < Call from Mutual.g to Mutual.g at 68:8-35: n m H l - ? _ _ = + ? ? _ = Call from Mutual.g to Mutual.g at 69:8-33: n m H l _ _ _ < diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean deleted file mode 100644 index c298310ede..0000000000 --- a/tests/lean/letRecMissingAnnotation.lean +++ /dev/null @@ -1,8 +0,0 @@ -def sum (as : Array Nat) : Nat := - let rec go (i : Nat) (s : Nat) : Nat := - if h : i < as.size then - go (i+2) (s + as.get ⟨i, h⟩) -- Error - else - s - termination_by as.size - i - go 0 0 diff --git a/tests/lean/letRecMissingAnnotation.lean.expected.out b/tests/lean/letRecMissingAnnotation.lean.expected.out deleted file mode 100644 index c50cf4d9d3..0000000000 --- a/tests/lean/letRecMissingAnnotation.lean.expected.out +++ /dev/null @@ -1,8 +0,0 @@ -letRecMissingAnnotation.lean:4:6-4:34: error: 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 -as : Array Nat -i s : Nat -h : i < Array.size as -⊢ Array.size as - (i + 2) < Array.size as - i diff --git a/tests/lean/run/wfOmega.lean b/tests/lean/run/wfOmega.lean new file mode 100644 index 0000000000..a7a165557f --- /dev/null +++ b/tests/lean/run/wfOmega.lean @@ -0,0 +1,4 @@ +/-! A wf recursive definition that needs omega to work -/ + +def foo (n : Nat) := + if h : n < 99 then 0 else foo (n - 99) diff --git a/tests/lean/wf1.lean.expected.out b/tests/lean/wf1.lean.expected.out index 6d61955c30..275641fcbf 100644 --- a/tests/lean/wf1.lean.expected.out +++ b/tests/lean/wf1.lean.expected.out @@ -15,5 +15,5 @@ Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) x y -1) 3:12-19 ? ? +1) 3:12-19 ≤ ? Please use `termination_by` to specify a decreasing measure.