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



Dear Thomas,

I just tried your file with Isabelle2013-2 and simp looped. This corroborates
your experience that [[simp_legacy_precond]] doesn't do anything, because the
divergence is not related to it. In any case, the only simplifier change I am
aware of relates to the handling of conjunctions in the premises of conditional
rewrite rules, and [[simp_legacy_precond]] switches that off.

Tobias

On 12/08/2014 07: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.