[Iris-Club] Frame-preserving update and double-negation
Joseph Tassarotti
jtassaro at andrew.cmu.edu
Wed Aug 24 19:06:48 CEST 2016
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
More information about the Iris-Club
mailing list