Re: [isabelle] Proofs that hang



Jesper,

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?

Best,
Tjark





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.