[Iris-Club] Frame-preserving update and double-negation

[Joseph Tassarotti]

On 08/24/2016 11:54 AM, Ralf Jung wrote:
>> Lemma rvs_ownM_update_nn x (Φ : M → Prop) :
>>    x ~~>: Φ → uPred_ownM x |- (((∃ y, ■ Φ y ∧ uPred_ownM y) -* False) -* False).
> That's funny. On the other hand, we don't get adequacy, so it seems that
> double negation is strictly too weak as a notion for our updates.

Yes, in fact all of the properties you mentioned in your previous email 
hold for the double negation modality. Let me include proofs this time 
to avoid another mistake:

Notation "|=n=> Q" := ((Q -★ False) -★ False)%I
   (at level 99, Q at level 200, format "|=n=>  Q") : uPred_scope.
Notation "P =n=> Q" := (P ⊢ |=n=> Q)
   (at level 99, Q at level 200, only parsing) : C_scope.

Lemma nn_intro P : P =n=> P.
Proof. apply wand_intro_l, wand_elim_l. Qed.
Lemma nn_mono P Q : (P ⊢ Q) → (|=n=> P) =n=> Q.
Proof. intros HPQ. apply wand_intro_l. rewrite -{1}HPQ. apply 
wand_elim_r. Qed.
Lemma nn_trans P : (|=n=> |=n=> P) =n=> P.
Proof. apply wand_intro_l. rewrite {1}(nn_intro (P -★ False)). apply 
wand_elim_r. Qed.
Lemma nn_frame_r P R : (|=n=> P) ★ R =n=> P ★ R.
Proof.
   apply wand_intro_r. rewrite (comm _ P) -wand_curry.
   by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
Lemma nn_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x =n=> ∃ y, ■ Φ y ∧ uPred_ownM y.
Proof. intros. rewrite -rvs_nn. by apply rvs_ownM_updateP. Qed.
Lemma now_True_nn P : ◇ (|=n=> P) ⊢ (|=n=> ◇ P).
Proof.
   rewrite /uPred_now_True. apply or_elim; auto using nn_mono.
   by rewrite -nn_intro -or_intro_l.
Qed.

In fact, I think all of them except for ownM_updateP hold for any 
modality of the form (-- -* Q) -* Q. I guess that is not surprising 
since I believe (-- -> Q) -> Q is a prototypical example of lax modality 
in the non-substructural setting.

-Joe