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