"bad" simp lemmas can lead to `acyclic` tactic failure with `simp` recursion limit

[fpfu]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I assume acyclic should now use omega instead of simp_arith

Context

Steps to Reproduce

import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Data.Nat.Basic

@[simp] theorem succ_le_iff_lt: n + 1 ≤ k ↔ n < k := sorry

inductive Foo 
| mk (x y: Foo)

set_option trace.Meta.Tactic.acyclic true in
example {x y: Foo} (h: x = Foo.mk y x): False := nomatch h

Expected behavior: acyclic can handle such a goal

Actual behavior: acyclic tactic produces an error message:

[Meta.Tactic.acyclic] failed with
    tactic 'simp' failed, nested error:
    maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit) 

Versions

4.7.0-rc2

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[leodemoura]

Remark: acyclic relies on the sizeOf automatically generated simp theorems. Thus, omega by itself cannot close the goals created by acyclic.

Possible solution: add new sizeOf simp set which contains only the sizeOf simp equational theorems.

Possible solution: new acyclic implementation that does not rely on sizeOf. This is the TODO list anyway since the current approach cannot handle functional fields. Example:

inductive Foo 
  | mk (x : Nat → Foo) 
  | bla : Foo

example {x : Foo} (h: x = Foo.mk fun _ => x) : False := 
  nomatch h -- currently fails

Remark: theorem succ_le_iff_lt is problematic independently of acyclic. Example:

example : n + 1 ≤ k := by
  simp_arith -- maximum recursion depth has been reached