Skip to content
  • Robbert Krebbers's avatar
    Remove basic updates from the Iris model, and define them using plainly. · d3814459
    Robbert Krebbers authored
    We define basic updates as:
    
        |==> P  :=  (∀ Q, (P -∗ ■ Q) -∗ ■ Q)
    
    From this definitions, we can prove all laws of basic updates, apart from
    those related to frame preserving updates. For that, we need the following
    primitive rule:
    
        x ~~>: Φ →
        uPred_ownM x ∗ (∀ y, ⌜Φ y⌝ -∗ uPred_ownM y -∗ ■ R) ⊢ ■ R.
    
    So, in total, this gets rid of 1 primitive connective (|==>) and 5 primitive
    rules (those of `|==>`), which is replaced by one new primitive rule.
    d3814459