Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.



The mystery deepens. This problem is somehow my fault.

It is the presence of the three completely redundant equalities "u = Partition a" "s = ((aa, b), ba)" "s' = ((ab, bb), bc)" which causes the simplifier to loop. These have been preserved by the hypothesis substitution change.

In either case, the simplifier initially loops on the assumption it has
  "pasDomainAbs initial_aag (cur_domain b)
       ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
       cur_domain b = cur_domain bb"

But in the old world, the simplifier goes down the rabbit hole - up to a recursive depth of 100 - then realises it is stuck, gives up, and solves the problem instead.

In the new world, the simplifier does the same things. But once it has done that, it starts thinking about the preserved subgoal containing "aa" which provides a use for one of the conditional rewrites "aa = ab" floating around. Somehow the simplifier has multiple options now, so instead of running to a depth of 100 and then giving up and coming back, it starts backtracking different approaches, and will never finish.

In hindsight this all makes sense, and is entirely my problem. I hope noone else has to deal with anything this awful as a result of this change.

Thanks to everyone for listening to me talk to myself about simplifier mysteries.

Cheers,
    Thomas.

On 12/08/14 17:50, Thomas Sewell wrote:
It's been pointed out to me that this particular behaviour of the simplifier predates Isabelle2014.

Apologies to everyone. I assumed that the extracted example was representative because it also caused the simplifier to loop. Instead it looks like the context somehow previously allowed the simplifier not to loop, and this has changed. I will have to investigate further.

Apologies once again,
    Thomas.

On 12/08/14 15:03, Thomas Sewell wrote:
Hello Isabelle users.

I've been putting a little time into updating the l4.verified proofs to isabelle-2014 (partly because I wanted to know what fraction of the problems would be caused by my hypsubst change). I've had a few problems I will soon report on. The simplest problem to report involves the simplifier.

I haven't been following closely, but I take it the simplifier is now a bit more aggressive in figuring out how to instantiate assumptions. This is probably a good thing, and has shrunk a few of the proofs in the repository already.

The problem is that this new mechanism sometimes leads to divergence, and I don't know how to turn it off. Here's an example I came across (or see the attached theory):

theory Scratch imports Main begin

lemma foo:
  "⋀a aa b ba ab bb bc.
       pasDomainAbs initial_aag (cur_domain b)
       ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟹
       u = Partition a ⟹
       s = ((aa, b), ba) ⟹
       s' = ((ab, bb), bc) ⟹
       states_equiv_for
(λx. pasObjectAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a)) (λx. pasIRQAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a)) (λx. pasASIDAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a)) (λx. pasDomainAbs initial_aag x ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
        (λx. ptr_range x 12) b bb ⟹
       pasDomainAbs initial_aag (cur_domain b)
       ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
       cur_domain b = cur_domain bb ∧
       globals_equiv b bb ∧
       scheduler_action b = scheduler_action bb ∧
       work_units_completed b = work_units_completed bb ∧
       equiv_irq_state (machine_state b) (machine_state bb) ∧
       (user_modes ba ⟶ aa = ab) ∧
ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel) kheap b bb ⟹
       pasDomainAbs initial_aag (cur_domain bb)
       ∈ subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) ⟶
       cur_domain b = cur_domain bb ∧
       globals_equiv b bb ∧
       scheduler_action b = scheduler_action bb ∧
       work_units_completed b = work_units_completed bb ∧
       equiv_irq_state (machine_state b) (machine_state bb) ∧
       (user_modes ba ⟶ aa = ab) ∧
ba = bc ∧ equiv_for (λx. pasObjectAbs initial_aag x = SilcLabel) kheap b bb ⟹
       (user_modes ba ⟶ aa = ab) ∧ ba = bc
  "

This is just a copy of a goal that came up in a proof somewhere. I don't know what any of this means either, and it turns out it doesn't matter. The behaviour is the same in a scratch theory with none of the constants defined.

This problem will cause "simp" or "(simp only: )" to loop. It will be solved immediately by clarify or blast. It can be solved by metis if we adjust the problem a little to ensure the type variables all have sorts.

The news file suggests that [[simp_legacy_precond]] might be relevant to this issue, but it doesn't seem to change anything.

In detail, this problem is solved by simplifying the implication whose premise is already known, i.e. apply (drule(1) mp). It happens the script "apply (drule(1) mp, simp)" solves the goal.

This weakness of simp is quite frustrating. To generate the above goal, I had to work around the possible simp divergence by simplifying in stages:
  apply (simp add: uwr_def sameFor_def sameFor_subject_def)
  apply clarify
  apply (simp(no_asm_use))
  apply clarify

I'm willing to accept the argument that this is not a bug but rather a tradeoff, with the default behaviour now being to solve more problems but sometimes time out more often. However I'd really like a way to turn this off. I've already had to dance around the problem in a couple of places, and it seems to be a generally unpleasant experience. My usual workarounds (simp only: ) and (simp(no_asm_use)) can't help me here.

I attach my scratch theory with this problem.

I hope there's a simple fix.

Cheers,
    Thomas.










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