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

Robbert Krebbers mail at robbertkrebbers.nl
Wed Aug 24 21:11:38 CEST 2016

On 08/24/2016 08:14 PM, Joseph Tassarotti wrote:
> Fixpoint laterN n P :=
>   match n with
>   | O => P
>   | S n' => uPred_later (laterN n' P)
>   end.
I thought I needed the iterated later a while ago, so I defined it and 
proved a bunch of lemmas about it, see commit cdce49a7. But then, since 
it turned out to be unneeded -- and I did not want to maintain it -- I 
reverted that commit.

I can revert my revert, if you like.

> Require Import Coq.Logic.Classical_Pred_Type.
> Lemma nnN_rvs P:  (∀ n, (P -★ laterN (n) False) -★ laterN (n) False) ⊢
> (|=r=> P).
That is a nice observation!

By the way, Lars and Ales told me that the ¬¬-closure is often used to 
make propositions timeless in step-indexed logics without resources. 
That is, when using a classical meta theory, ¬¬P is semantically 
equivalent to λ _, P 0.

Since we also have resources in Iris, this trick does not work. Does any 
of you know whether there is a similar trick in Iris?


More information about the Iris-Club mailing list