Commit e048a414 authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup

parent 001500e2
......@@ -5,7 +5,7 @@ Require Import iris.prelude.options.
Notation "'⊒' V" := (monPred_in V) (at level 30, format "⊒ V") : bi_scope.
Definition monPred_unseal_eqs :=
Local Definition monPred_unseal_eqs :=
(@monPred_at_embed, @monPred_at_pure, @monPred_at_emp,
@monPred_at_and, @monPred_at_or, @monPred_at_impl,
@monPred_at_sep,
......@@ -15,7 +15,7 @@ Definition monPred_unseal_eqs :=
@monPred_at_fupd, @monPred_at_bupd, @monPred_at_later, @monPred_at_laterN,
@monPred_at_except_0).
Ltac unseal_monpred := rewrite !monPred_unseal_eqs /=.
Local Ltac unseal_monpred := rewrite !monPred_unseal_eqs /=.
Section ExtraMonpred.
Context `{I : biIndex, PROP : bi}.
......@@ -161,6 +161,15 @@ Proof.
by iApply ("W" $! V3 V3 with "[%] P").
Qed.
Lemma monPred_subjectively_later P :
<subj> P <subj> P.
Proof.
constructor => i.
rewrite monPred_subjectively_unfold monPred_at_later !monPred_at_embed.
setoid_rewrite monPred_at_later.
apply bi.later_exist.
Qed.
(** proofmode *)
#[global] Instance into_exist_objectively `{!@BiIndexBottom I bot} {A}
P (Φ : A monPred) name :
......
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import proofmode.
From gpfsl.base_logic Require Import iwp na.
......
From iris.base_logic Require Import lib.invariants.
From stdpp Require Import namespaces.
From iris.proofmode Require Import proofmode.
From gpfsl.gps Require Export middleware_PP.
From gpfsl.logic Require Import subj_invariants relacq.
From gpfsl.logic Require Import subj_invariants.
Require Import iris.prelude.options.
(* TODO: move to Iris *)
Lemma monPred_subjectively_later {I : biIndex} {PROP : bi} (P : monPred I PROP) :
<subj> P <subj> P.
Proof.
constructor => i.
rewrite monPred_subjectively_unfold monPred_at_later !monPred_at_embed.
setoid_rewrite monPred_at_later.
apply bi.later_exist.
Qed.
(** Persistent Plain Protocol *)
Class gpsIPG Σ Prtcl := GPS_IPPG {
gpsIP_proG :> gpsG Σ Prtcl;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment