Re: [isabelle] Proofs that hang
On Sunday 13 April 2008 13:35, Jesper Bengtson wrote:
> 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.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and