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

[Joseph Tassarotti]

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).

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
>