Remove basic updates from the Iris model, and define them using plainly.

changed the description

By the way, note the similarity between the definition of the basic update modality and the definition of the plausibly modality in !185 (closed).

Instead of rule for updates in the MR description, we could also have:

Lemma ownM_updateP x R :
  uPred_ownM x ∗
  (∀ z, ✓ (x ⋅ z) → ∃ y, ✓ (y ⋅ z) ∧ (uPred_ownM y -∗ ■ R)) ⊢ ■ R.

This rule takes the notion of frame preserving updates out of the base logic.

This change will be rather invasive:

We will only have the old rule for frame preserving updates when the camera is discrete.
For non-discrete cameras, we need to have a notion of frame preserving updates in the logic (this is not part of the primitives).

I think this actually makes a lot of sense.

FWIW: Since all of the frame preserving update stuff is from the time before we had the proof mode, it may be the case that we could get away by only having frame preserving updates in the logic.

changed the description

I just noted that the definition can be simplified to:

|==> P  :=  (∀ R, (P -∗ ■ R) -∗ R)

Not sure if the absence of the ■ in the conclusion makes it easier to read.

This is great. If we understand plainly as the analogue of pure for step-indexed assertions (which was the intuition I got from #161 (closed)), then it makes sense to me why this works and gives you something cleaner than !172 (closed). In hindsight, the pure propositions in !172 (closed) shifted by arbitrary ▷^n are maybe crudely trying to mimic plainly. (I would like to better understand if there is a connection and whether we can define a plainly modality as shiftings of pure propositions). Plus, the connection to !185 (closed) is quite nice indeed.

Although defining it in terms of frame preserving updates was good for some intuitions/connections to earlier separation logics, I've felt like the double-negation/continuation style might make it a little bit less mystical/alien seeming to logicians.

My only suggestion is that I would prefer to see the definition moved to the generic bi stuff. It works for any logic with plainly, right? So why not make it an optional module you can import.

So, #161 (closed) lets us define plainly for an arbitrary sbi, !186 (closed) then lets us get basic update. Can we get fancy updates and invariants somehow for a generic sbi?

In hindsight, the pure propositions in !172 (closed) shifted by arbitrary ▷^n are maybe crudely trying to mimic plainly. (I would like to better understand if there is a connection and whether we can define a plainly modality as shiftings of pure propositions).

I came up with the following a while ago but didn't pursue it because I couldn't derive some of the axioms of plainly:

Lemma embed_f_change_resource {M} (f : nat → Prop) k x y :
  (∀ n : nat, ▷^n ⌜f n⌝ : uPred M)%I k x → (∀ n : nat, ▷^n ⌜f n⌝ : uPred M)%I k y.
Proof.
  simpl.
  uPred.unseal.
  intros Hf n; specialize (Hf n); simpl in *; revert Hf.
  generalize (f n); revert k.
  induction n; auto.
  simpl. uPred.unseal.
  destruct k; auto. intros P Hf.
  apply IHn; auto.
Qed.

Lemma implies_Plain {M} (P : uPred M) :
  (∃ f, P ∧ ((∀ n : nat, ▷^n ⌜f n⌝) ≡ P)) ⊢ ■ P.
Proof.
  uPred.unseal.
  split => n x Hx [f [HP21 HP22]].
  apply HP22; eauto using ucmra_unit_validN.
  pose proof (@embed_f_change_resource M f n x ε) as Her.
  revert Her; uPred.unseal.
  intros Her. apply Her.
  apply HP22; auto.
Qed.

Lemma uPredN_char {M} (P : uPred M) x n k :
  (▷^n P)%I k x = if decide (k < n) then True else P (k - n) x.
Proof.
  revert k; induction n; intros k.
  - destruct decide; auto with omega.
    replace (k - 0) with k by omega; trivial.
  - simpl; uPred.unseal. destruct k; simpl; auto.
    etrans; first apply IHn.
    repeat destruct decide; auto with omega.
Qed.

Lemma Plain_implies {M} (P : uPred M) :
  ■ P ⊢ (∃ f, P ∧ ((∀ n : nat, ▷^n ⌜f n⌝) ≡ P)).
Proof.
  uPred.unseal.
  split => n x Hx HP.
  exists (λ n, P n ε).
  split; first by apply uPred.plainly_elim; try uPred.unseal; auto.
  split => k z Hk Hz; split.
  - intros Hf.
    apply uPred.plainly_elim; try uPred.unseal; auto.
    change ((uPred_plainly_def P) k x).
    eapply uPred_mono; eauto.
  - intros HP' l.
    rewrite uPredN_char.
    destruct decide; auto.
    change (P l ε).
    eapply uPred_mono; first apply HP; eauto with omega.
Qed.

One big issue is existential quantification, e.g., with this formulation it is not easy to show (without going into the model and using things like afineness of the logic) that plainly commutes with universal quantifier.

This is great. If we understand plainly as the analogue of pure for step-indexed assertions (which was the intuition I got from #161 (closed)), then it makes sense to me why this works and gives you something cleaner than !172 (closed). In hindsight, the pure propositions in !172 (closed) shifted by arbitrary ▷^n are maybe crudely trying to mimic plainly. (I would like to better understand if there is a connection and whether we can define a plainly modality as shiftings of pure propositions).

I also think of plainly as the the analogue of pure for step-indexed propositions.

There is most likely a connection between plainly and pure propositions shifted by arbitrary ▷^n. However, I'm pretty sure that is such a connection cannot be provable in the logic without very weird axioms. Also, not that the use of pure propositions is kind of a Coq artifact. In the paper description of the logic we do not really consider them.

My only suggestion is that I would prefer to see the definition moved to the generic bi stuff. It works for any logic with plainly, right? So why not make it an optional module you can import.

Sure, there is kind of a design space there, depending on far we want to generalize things. Note that the definition works for pretty much any type of continuations K and interpretation of those continuations I : K → iProp:

M P  :=  (∀ k : K, (P -∗ I k) -∗ I k)

This modality will be a strong monad, and additionally satisfy the "run" rule:

M (I k) ⊢ I k

To obtain the basic update modality in this MR, simply take K := iProp and I := plainly.

In the case of Iris, if you want to link it to some form of frame preserving updates (which has to be proved in the model), it's crucial that I k is plain. That said, for other logics (e.g. linear versions of Iris) it may make sense to but use something else for K and I, but this all remains to be explored.

So, #161 (closed) lets us define plainly for an arbitrary sbi, !186 (closed) then lets us get basic update.

The more I think of it, the more I believe !161 (merged) is a hack. The only reason it works is that we work in a shallow embedding. The proofs of many of the plainly rules using the definition in #161 (closed) rely on the fact that we can rewrite using logical equivalences in internal equalities P ≡ Q. I don't think you can do this in the deep embedding unless you have some extensionality principle---and we exactly need plainly to state such an extensionality principle.

mentioned in merge request !185 (closed)

This is pretty cool! Do we have an equivalence proof to the old definition? Also, I don't understand anything you are saying about the continuation monad. Could you elaborate?

That said (and without having looked at the details yet), I am not convinced we want to do this.

From this definitions, we can prove all laws of basic updates, apart from those related to frame preserving updates.

That one rule is the most important one for basic updates! You did some bean counting with numbers of connectives and rules, but IMO this proposal also makes the basic update modality void of its most important content, which is frame-preserving updates.

If we lift frame-preserving updates to a relation on sets of resources

P ~~> Q := forall r \in P, r ~~> Q

(using the non-deterministic ~~> we already have), and then interpret this statement in SProp, we have defined the basic update. That is the fundamental nature of basic updates, and it is why they are so useful.

Your proposed definition makes this look like an accident. That's why I don't like using it as the definition. I am fine replacing the existing double-negation characterization of bupd with this, maybe even have a constructor from BiPlainly to BiBUpd, and it certainly seems worth studying, but my feeling is that Iris should not define bupd this way.

@robbertkrebbers and me talked about this a bit on Monday, also in the context of how to scale basic updates to linear Iris.

We came to the conclusion that it doesn't help, and in fact linear logics probably want another (a second) adequacy lemma for basic updates that would not be provable from the definition given here.

@jung @robbertkrebbers: I think we should have a chat about this at POPL.

Sure, sounds good.

@jtassaro will you be at POPL? (I guess not but it's worth asking.^^)

Yes, I'll be there.

mentioned in merge request !172 (closed)

We decided that for now, we'll not change the definition of Iris. However, we are interested in better understanding bupd, so @robbertkrebbers will change this to leave bupd untouched but instead replace the "double negation" file with another one that shows this alternative definition.

mentioned in merge request !211 (merged)

Remove basic updates from the Iris model, and define them using plainly.

Merge request reports

Activity