Open fpfu opened 5 months ago
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
Prerequisites
Description
I assume
acyclic
should now useomega
instead ofsimp_arith
Context
Steps to Reproduce
Expected behavior:
acyclic
can handle such a goalActual behavior:
acyclic
tactic produces an error message:Versions
4.7.0-rc2
Additional Information
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.