[Iris-Club] Frame-preserving update and double-negation
Ralf Jung
jung at mpi-sws.org
Wed Aug 24 19:30:42 CEST 2016
Hi,
> 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.
That's cute. We should put this somewhere in the repo. Could you put
it into some file (algebra/double_negation or so?) and submit a merge
request in GitLab?
Kind regards,
Ralf
More information about the Iris-Club
mailing list