Re: [isabelle] Weird situation with the simplifier, congruence rules, and eta-expansion

You are right as to the motivation for the design. It seemed to better
choice at the time. I still find it works well for me. But I would not
want to argue with you if you say that you think the opposite choice
works better for your L4.verified, and that may actually be more
representative for the average user. It was a heuristic design. I
suspect it would be a lot of work to reverse it.


Thomas Sewell schrieb:
> Hello Brian & Isabelle users.
> There's a tension here between Isabelle's resolution engine and its rewriting engine. The resolution engine makes eta-expansion irrelevant; the simplification engine does not. This is more often seen with simplification rules like o_apply - simple constants like "op o" seem to get unfolded inexplicably, the explanation being that the term they were in had been invisibly eta-expanded at some point. The advantage in this case is that it's usually easy to understand what's happened, even if it's difficult to explain why.
> The situation with congruence rules, however, is deeply unpleasant. The simpler way to fix your problem was to install the stronger form of the nat_case congruence rule, nat.case_cong. This one strengthens rather than degrades the simplifier, and eta contraction makes less difference.
> As I understand it, the weak case rules are installed to prevent the rewrite rules of complex recursive functions (e.g. "f x = if x = 0 then 1 else x * f (x - 1)") looping the simplifier. I agree that looping must be prevented, even at the cost of making the simplifier work less often. My experience from the L4.verified project, however, is that it is far preferable to remove the rewrite rules of such functions than to degrade the simplifier.
> There are four reasons for this:
>   1) Novice Isabelle users just don't understand the current default setup, nor do they understand what congruence rules are. It shouldn't be this complicated to explain when (simp add: useful_rule_we_wrote) will work.
>   2) The current situation won't stop looping anway, as split_if is in the default splitter set. The above function will loop the simplifier, as will many, If being more common than any case expression.
>   3) It's easy to write a terminating function that doesn't depend on a case expression for termination. Consider this (contrived) code in the error+state monad:
> "f = do
>   done <- checkIfDone
>   when done $ throwError ()
>   takeOneStep
>   f
> "
>   This function might terminate (depending on the behaviour of checkIfDone and takeOneStep). Its expansion rule must be dropped from the simpset to prevent looping.
>   4) Proofs about complex recursive functions of this type were usually complex and done by induction anyway. Having to manually unroll them with subst is not much additional effort.
> In short, I would prefer it if the stronger case congruence rules were in the default simpset and looping was prevented by other means.
> Yours,
>     Thomas.
> ________________________________________
> From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Brian Huffman [brianh at]
> Sent: Wednesday, May 12, 2010 6:54 AM
> To: isabelle-users
> Subject: [isabelle] Weird situation with the simplifier, congruence rules,      and     eta-expansion
> Hello all,
> The left-hand side of the following lemma is simply an eta-expanded
> version of the right-hand side. It could be solved immediately by
> "apply (rule refl)". One might think that the simplifier could easily
> handle such a simple task.
> lemma "(%n. nat_case 1 Suc n) = (nat_case 1 Suc)"
> by simp
> But... the proof fails! If you do "apply simp" instead, here's what is
> left over:
> goal (1 subgoal):
>  1. (%n. nat_case 1 Suc n) = nat_case (Suc 0) Suc
> The problem is that there is a congruence rule for nat_case:
> Nat.nat.weak_case_cong:
>   M = M' ==> nat_case f1 f2 M = nat_case f1 f2 M'
> On the eta-expanded left-hand side, the congruence rule applies and
> prevents the "1" from being rewritten to "Suc 0". But the congruence
> rule does not apply to the eta-contracted right-hand side.
> To prevent the simplifier from rewriting the first two arguments of
> nat_case it seems like we really need a couple more congruence rules
> for the partially-applied cases:
> lemma nat_weak_case_cong2 [cong]: "nat_case f1 f2 = nat_case f1 f2"
> lemma nat_weak_case_cong3 [cong]: "nat_case f1 = nat_case f1"
> ... but the simplifier only allows one congruence per constant to be
> active at one time.
> This problem is actually important in practice: It makes some internal
> proofs in the HOLCF fixrec package break for certain definitions. To
> avoid this issue, I am forced to have fixrec maintain its own private
> simpset that doesn't include any congruence rules.
> It seems like Isabelle tries to maintain the illusion that
> eta-equivalent terms are identical (especially when the "Eta Contract"
> option is enabled in ProofGeneral). The behavior I have described
> above breaks this abstraction.
> - Brian
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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