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

[Ralf Jung]

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