Commit 1650c2a0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Move FUpd and BUpd classes to bi/interface.v

parent 51b61ebb
...@@ -7,33 +7,12 @@ Set Default Proof Using "Type". ...@@ -7,33 +7,12 @@ Set Default Proof Using "Type".
Export invG. Export invG.
Import uPred. Import uPred.
Class FUpd (A : Type) : Type := fupd : coPset coPset A A.
Instance: Params (@fupd) 4.
Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ := Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ownE E1 == (wsat ownE E2 P))%I. (wsat ownE E1 == (wsat ownE E2 P))%I.
Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed. Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux. Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux. Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
Section fupd. Section fupd.
Context `{invG Σ}. Context `{invG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
......
...@@ -317,9 +317,6 @@ Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A. ...@@ -317,9 +317,6 @@ Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A.
Definition uPred_cmra_valid_eq : Definition uPred_cmra_valid_eq :
@uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux. @uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
Class BUpd (A : Type) : Type := bupd : A A.
Instance : Params (@bupd) 2.
Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M := Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{| uPred_holds n x := k yf, {| uPred_holds n x := k yf,
k n {k} (x yf) x', {k} (x' yf) Q k x' |}. k n {k} (x yf) x', {k} (x' yf) Q k x' |}.
...@@ -570,12 +567,6 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid. ...@@ -570,12 +567,6 @@ Coercion uPred_valid {M} : uPred M → Prop := bi_valid.
(* Latest notation *) (* Latest notation *)
Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope. Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : bi_scope.
Notation "|==> Q" := (bupd Q)
(at level 99, Q at level 200, format "|==> Q") : bi_scope.
Notation "P ==∗ Q" := (P |==> Q)
(at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
Module uPred. Module uPred.
Include uPred_unseal. Include uPred_unseal.
......
From stdpp Require Import coPset.
From iris.algebra Require Export ofe. From iris.algebra Require Export ofe.
Set Primitive Projections. Set Primitive Projections.
...@@ -522,4 +523,36 @@ Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed. ...@@ -522,4 +523,36 @@ Proof. eapply (sbi_mixin_later_persistently_2 bi_entails), sbi_sbi_mixin. Qed.
Lemma later_false_em P : P False ( False P). Lemma later_false_em P : P False ( False P).
Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed. Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
End sbi_laws. End sbi_laws.
End bi. End bi.
Class BUpd (A : Type) : Type := bupd : A A.
Instance : Params (@bupd) 2.
Notation "|==> Q" := (bupd Q)
(at level 99, Q at level 200, format "|==> Q") : bi_scope.
Notation "P ==∗ Q" := (P |==> Q)
(at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : bi_scope.
Class FUpd (A : Type) : Type := fupd : coPset coPset A A.
Instance: Params (@fupd) 4.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)
(at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
format "|={ E }=> Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
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