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

[Jacques-Henri Jourdan]

On 08/24/2016 08:14 PM, Joseph Tassarotti wrote:
> Actually, I can do you one better.
>
> Define:
>
> Fixpoint laterN n P :=
>   match n with
>   | O => P
>   | S n' => uPred_later (laterN n' P)
>   end.
>
> Then you can prove:
>
> Lemma laterN_False_big n a x: ✓{n} x →  a ≤ n → (laterN a 
> (uPred_pure_def False)) n x → False.
> Lemma laterN_False_small n a x: ✓{n} x →  n < a → (laterN a 
> (uPred_pure_def False)) n x.
> Lemma rvs_nnN P: (|=r=> P) ⊢ ∀ n, (P -★ laterN (n) False) -★ laterN 
> (n) False.
>
> Require Import Coq.Logic.Classical_Pred_Type.
> Lemma nnN_rvs P:  (∀ n, (P -★ laterN (n) False) -★ laterN (n) False) ⊢ 
> (|=r=> P).


Oh, that is very interesting : I wonder wether we can add some laters 
somewhere in those definitions and quantify over n in order to get 
something strong enough to get adequacy.

>
> I will polish these scripts up and submit a merge request.
>
> -Joe
>
> On 08/24/2016 01:30 PM, Ralf Jung wrote:
>> 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
>>
>
>