feat: use omega in default decreasing_trivial (#3503)

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

@@ -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

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
  _ _ _ <

tests/lean/letRecMissingAnnotation.lean

@@ -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

tests/lean/letRecMissingAnnotation.lean.expected.out

@@ -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

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)

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.