[Iris-Club] Frame-preserving update and double-negation
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)
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