Skip to content

refactor pool_safe

Lennard Gäher requested to merge ci/pool_safe into master

This MR refactors pool_safe to use a more constructive formulation (see #10).

In short,

  • the new definition of pool_safe pushes through the negation at the top of the old definition (which was defined in terms of pool_reach_stuck),
  • but leaves the definition of pool_reach_stuck as it is (a definition in terms of pool_safe seems very unconstructive). This is relevant in particular because our definition of behaviour still uses reach_stuck. This definition has the consequence that the equivalence not pool_safe <-> pool_reach_stuck does hold only classically or with decidability of reduction now.
  • we need XM at a few different places in the adequacy proof and in the behaviour metatheory and can drop it at others.
  • reach_or_stuck has become safe_reach and is defined in terms of pool_safe now,
  • IrredUnless has been replaced by SafeImplies, which is defined as safe P e σ -> ϕ, which mostly matches the def we show on paper.

This entails that also the relevant lemmas for exploiting safety have been renamed, e.g.:

  • source_red_irred_unless has become source_red_safe_implies,
  • safe_reach_irred has become safe_reach_safe,
  • pool_safe_irred has become pool_safe_implies.

@jung or @msammler : can you review if you are fine with the naming changes?

Merge request reports