Email Gateway (Aug 18 2022 at 15:16): Email Gateway (Aug 18 2022 at 15:16):From: Brian Huffman <brianh@cs.pdx.edu>
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):
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.
Email Gateway (Aug 18 2022 at 15:17):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Email Gateway (Aug 18 2022 at 15:17):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Thomas Sewell schrieb:
Email Gateway (Aug 18 2022 at 15:17):From: Lawrence Paulson <lp15@cam.ac.uk>
The current design has the advantage of causing simplification to resemble execution: the arms of a conditional or case expression are left untouched until the relevant case has been identified. I would not express this as "degrading the simplifier". It certainly doesn't degrade its performance. However, I agree that there are situations where people are surprised that obvious simplifications do not take place in a case expression.
Larry
Thomas Sewell schrieb:
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.
Last updated: Nov 21 2024 at 12:39 UTC