Email Gateway (Aug 18 2022 at 11:43): Email Gateway (Aug 18 2022 at 11:43):From: Jesper Bengtson <jesperb@it.uu.se>
Greetings
In my current formalisation I have a relation which is created through
some quite trivial rules. It's an equivalence relation, it is a
congruence, it's idempotent and it has one or two more obscure rules.
The problem is that these rules are inherently symmetric -- especially
rules regarding associativity and commutativity of one of the
operators and I am having a hard time to have Isabelel automatically
verify proofs even though they are seemingly quite simple. Doing it by
hand works, but it's a bit of a pain.
My question is basically if there is a way to reason about these types
of relations automatically in Isabelle where the automatic tactics get
stuck on symmetries.
Thank you for your time.
Jesper Bengtson
Email Gateway (Aug 18 2022 at 11:43):From: Tjark Weber <tjark.weber@gmx.de>
Jesper,
Isabelle uses ordered rewriting. Permutative rules, e.g. commutativity, are
applied only if this results in a "smaller" (with respect to some fixed
lexicographic order on terms) term.
For an associative and commutative operator f, you should add not only
associativity and commutativity to the set of default rewrite rules, but also
a derived rule, left-commutativity: f(x, f(y, z)) = f(y, f(x, z)). Please
see Section 9.1.1 of the Isabelle/HOL tutorial for further details.
Since ordered rewriting should prevent the simplifier from "getting stuck" on
symmetries, loops are probably due to more complex interaction between
different rewrite rules. Maybe try "Isabelle > Settings > Trace Simplifier"
in ProofGeneral to see which rules are getting used. "apply (simp del: XXX)"
and "apply (simp only: XXX)" (see Section 3.1.4 of the Isabelle/HOL tutorial)
might also be useful to locate the problem.
I hope this answers your question. Otherwise could you maybe supply a
concrete example of a proof that hangs?
Best,
Tjark
Last updated: May 03 2024 at 04:19 UTC