diff --git a/algebra/agree.v b/algebra/agree.v
index d739964f321fc94e9dd9dc6c20000cd42cf0fb72..7181e55dde57eb1c12f5f2012c7a194ce3dbf6d7 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -130,11 +130,11 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
(** Internalized properties *)
-Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
+Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b) ⊣⊢ (a ≡ b : uPred M).
Proof.
uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
Qed.
-Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
+Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
End agree.
diff --git a/algebra/auth.v b/algebra/auth.v
index 4fc52b8b2df137d9f873092df64b8c8f06244d88..8abc1dede9ce5bef3a622ede122e13767c679bcd 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -138,14 +138,14 @@ Admitted.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
- (x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
+ (x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
- (✓ x)%I ≡ (match authoritative x with
+ (✓ x) ⊣⊢ (match authoritative x with
| Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
| ExclUnit => ✓ own x
| ExclBot => False
- end : uPred M)%I.
+ end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
(** The notations â—¯ and â— only work for CMRAs with an empty element. So, in
diff --git a/algebra/excl.v b/algebra/excl.v
index 1314471f396eea88065b7bfaf2ae1d32f22ba9d9..89b4f40878f3659702c1fe6a420dde1e4d01514e 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -138,16 +138,16 @@ Qed.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
- (x ≡ y)%I ≡ (match x, y with
+ (x ≡ y) ⊣⊢ (match x, y with
| Excl a, Excl b => a ≡ b
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| _, _ => False
- end : uPred M)%I.
+ end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
- (✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
+ (✓ x) ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 8f302e8db123b35f65c4f6939b59f7af89fe632f..0d51ab668c05a1d810386c06fa387ac89cb41399 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -164,9 +164,9 @@ Global Instance map_cmra_discrete : CMRADiscrete A → CMRADiscrete mapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
(** Internalized properties *)
-Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.
+Lemma map_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
Proof. by uPred.unseal. Qed.
-Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
+Lemma map_validI {M} m : (✓ m) ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
Proof. by uPred.unseal. Qed.
End cmra.
diff --git a/algebra/frac.v b/algebra/frac.v
index 35d7288771a899fb50f5357b031248e3d6bdce27..f504b0c13c71b4e22b8340a984c53f31eddcb9ec 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -177,17 +177,17 @@ Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
- (x ≡ y)%I ≡ (match x, y with
+ (x ≡ y) ⊣⊢ (match x, y with
| Frac q1 a, Frac q2 b => q1 = q2 ∧ a ≡ b
| FracUnit, FracUnit => True
| _, _ => False
- end : uPred M)%I.
+ end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; destruct 1; try constructor.
Qed.
Lemma frac_validI {M} (x : frac A) :
- (✓ x)%I ≡ (if x is Frac q a then ■(q ≤ 1)%Qc ∧ ✓ a else True : uPred M)%I.
+ (✓ x) ⊣⊢ (if x is Frac q a then ■(q ≤ 1)%Qc ∧ ✓ a else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
diff --git a/algebra/iprod.v b/algebra/iprod.v
index e1761819397b231729f2c925dacb966a81c6295c..f08dc8199f7c1c7d1d8a045937886aff8cbacef1 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -164,9 +164,9 @@ Section iprod_cmra.
Qed.
(** Internalized properties *)
- Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
+ Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
Proof. by uPred.unseal. Qed.
- Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
+ Lemma iprod_validI {M} g : (✓ g) ⊣⊢ (∀ i, ✓ g i : uPred M).
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
diff --git a/algebra/option.v b/algebra/option.v
index 76220397cecfbf2c0efb1f34c4762fddd5c2b67d..09d4e94848bd4282e719594ddf8abbc09176ad2b 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -132,14 +132,14 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
- (x ≡ y)%I ≡ (match x, y with
+ (x ≡ y) ⊣⊢ (match x, y with
| Some a, Some b => a ≡ b | None, None => True | _, _ => False
- end : uPred M)%I.
+ end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma option_validI {M} (x : option A) :
- (✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
+ (✓ x) ⊣⊢ (match x with Some a => ✓ a | None => True end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
diff --git a/algebra/upred.v b/algebra/upred.v
index 968d89add18fec3076a7297e8d15d3122d1a6224..df3d271c147cd2d942936b80eb316fc5e098f6fb 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -269,8 +269,10 @@ Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
Definition uPred_valid_eq :
@uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.
-Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
-Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
+Notation "P ⊢ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
+Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I) (at level 70) : C_scope.
+Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
Notation "■φ" := (uPred_const φ%C%type)
(at level 20, right associativity) : uPred_scope.
Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
@@ -299,11 +301,11 @@ Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
Infix "↔" := uPred_iff : uPred_scope.
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
+Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
Arguments timelessP {_} _ {_}.
(* TODO: Derek suggested to call such assertions "persistent", which we now
do in the paper. *)
-Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
+Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊢ □ P.
Arguments always_stable {_} _ {_}.
Module uPred.
@@ -318,7 +320,8 @@ Context {M : cmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
-Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
+Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails.
@@ -328,31 +331,31 @@ Proof.
* by intros P; split=> x i.
* by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
Qed.
-Global Instance: AntiSymm (≡) (@uPred_entails M).
+Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_spec P Q : P ≡ Q ↔ P ⊑ Q ∧ Q ⊑ P.
+Lemma equiv_spec P Q : P ⊣⊢ Q ↔ P ⊢ Q ∧ Q ⊢ P.
Proof.
- split; [|by intros [??]; apply (anti_symm (⊑))].
+ split; [|by intros [??]; apply (anti_symm (⊢))].
intros HPQ; split; split=> x i; apply HPQ.
Qed.
-Lemma equiv_entails P Q : P ≡ Q → P ⊑ Q.
+Lemma equiv_entails P Q : P ⊣⊢ Q → P ⊢ Q.
Proof. apply equiv_spec. Qed.
-Lemma equiv_entails_sym P Q : Q ≡ P → P ⊑ Q.
+Lemma equiv_entails_sym P Q : Q ⊣⊢ P → P ⊢ Q.
Proof. apply equiv_spec. Qed.
Global Instance entails_proper :
- Proper ((≡) ==> (≡) ==> iff) ((⊑) : relation (uPred M)).
+ Proper ((⊣⊢) ==> (⊣⊢) ==> iff) ((⊢) : relation (uPred M)).
Proof.
move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
- by trans P1; [|trans Q1].
- by trans P2; [|trans Q2].
Qed.
-Lemma entails_equiv_l (P Q R : uPred M) : P ≡ Q → Q ⊑ R → P ⊑ R.
+Lemma entails_equiv_l (P Q R : uPred M) : P ⊣⊢ Q → Q ⊢ R → P ⊢ R.
Proof. by intros ->. Qed.
-Lemma entails_equiv_r (P Q R : uPred M) : P ⊑ Q → Q ≡ R → P ⊑ R.
+Lemma entails_equiv_r (P Q R : uPred M) : P ⊢ Q → Q ⊣⊢ R → P ⊢ R.
Proof. by intros ? <-. Qed.
(** Non-expansiveness and setoid morphisms *)
-Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
+Global Instance const_proper : Proper (iff ==> (⊣⊢)) (@uPred_const M).
Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
Proof.
@@ -360,14 +363,14 @@ Proof.
split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
Global Instance and_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_and M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_and M) := ne_proper_2 _.
Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
Proof.
intros P P' HP Q Q' HQ; split=> x n' ??.
unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
Global Instance or_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_or M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_or M) := ne_proper_2 _.
Global Instance impl_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Proof.
@@ -375,7 +378,7 @@ Proof.
unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Qed.
Global Instance impl_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_impl M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_impl M) := ne_proper_2 _.
Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
Proof.
intros P P' HP Q Q' HQ; split=> n' x ??.
@@ -384,7 +387,7 @@ Proof.
eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Global Instance sep_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_sep M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_sep M) := ne_proper_2 _.
Global Instance wand_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Proof.
@@ -392,7 +395,7 @@ Proof.
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_wand M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _.
Global Instance eq_ne (A : cofeT) n :
Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Proof.
@@ -401,14 +404,14 @@ Proof.
* by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.
Global Instance eq_proper (A : cofeT) :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
+ Proper ((≡) ==> (≡) ==> (⊣⊢)) (@uPred_eq M A) := ne_proper_2 _.
Global Instance forall_ne A n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Proof.
by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
Global Instance forall_proper A :
- Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
+ Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_forall M A).
Proof.
by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
@@ -419,7 +422,7 @@ Proof.
unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
Qed.
Global Instance exist_proper A :
- Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_exist M A).
+ Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_exist M A).
Proof.
intros Ψ1 Ψ2 HΨ.
unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
@@ -430,20 +433,20 @@ Proof.
apply (HPQ n'); eauto using cmra_validN_S.
Qed.
Global Instance later_proper :
- Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
+ Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
Proof.
intros P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using cmra_core_validN.
Qed.
Global Instance always_proper :
- Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
+ Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
Proof.
intros a b Ha.
unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
-Global Instance ownM_proper: Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
+Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
Global Instance valid_ne {A : cmraT} n :
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
@@ -451,252 +454,252 @@ Proof.
by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance valid_proper {A : cmraT} :
- Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
+ Proper ((≡) ==> (⊣⊢)) (@uPred_valid M A) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
Proof. unfold uPred_iff; solve_proper. Qed.
Global Instance iff_proper :
- Proper ((≡) ==> (≡) ==> (≡)) (@uPred_iff M) := ne_proper_2 _.
+ Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
(** Introduction and elimination rules *)
-Lemma const_intro φ P : φ → P ⊑ ■φ.
+Lemma const_intro φ P : φ → P ⊢ ■φ.
Proof. by intros ?; unseal; split. Qed.
-Lemma const_elim φ Q R : Q ⊑ ■φ → (φ → Q ⊑ R) → Q ⊑ R.
+Lemma const_elim φ Q R : Q ⊢ ■φ → (φ → Q ⊢ R) → Q ⊢ R.
Proof.
unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
-Lemma False_elim P : False ⊑ P.
+Lemma False_elim P : False ⊢ P.
Proof. by unseal; split=> n x ?. Qed.
-Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
+Lemma and_elim_l P Q : (P ∧ Q) ⊢ P.
Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
+Lemma and_elim_r P Q : (P ∧ Q) ⊢ Q.
Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
+Lemma and_intro P Q R : P ⊢ Q → P ⊢ R → P ⊢ (Q ∧ R).
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
-Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
+Lemma or_intro_l P Q : P ⊢ (P ∨ Q).
Proof. unseal; split=> n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
+Lemma or_intro_r P Q : Q ⊢ (P ∨ Q).
Proof. unseal; split=> n x ??; right; auto. Qed.
-Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
+Lemma or_elim P Q R : P ⊢ R → Q ⊢ R → (P ∨ Q) ⊢ R.
Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
-Lemma impl_intro_r P Q R : (P ∧ Q) ⊑ R → P ⊑ (Q → R).
+Lemma impl_intro_r P Q R : (P ∧ Q) ⊢ R → P ⊢ (Q → R).
Proof.
unseal; intros HQ; split=> n x ?? n' x' ????.
apply HQ; naive_solver eauto using uPred_weaken.
Qed.
-Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
+Lemma impl_elim P Q R : P ⊢ (Q → R) → P ⊢ Q → P ⊢ R.
Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
-Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊑ Ψ a) → P ⊑ (∀ a, Ψ a).
+Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ (∀ a, Ψ a).
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
+Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
Proof. unseal; split=> n x ? HP; apply HP. Qed.
-Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
+Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ (∃ a, Ψ a).
Proof. unseal; split=> n x ??; by exists a. Qed.
-Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
+Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
-Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
+Lemma eq_refl {A : cofeT} (a : A) P : P ⊢ (a ≡ a).
Proof. unseal; by split=> n x ??; simpl. Qed.
Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
- `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊑ (a ≡ b) → P ⊑ Ψ a → P ⊑ Ψ b.
+ `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊢ (a ≡ b) → P ⊢ Ψ a → P ⊢ Ψ b.
Proof.
unseal; intros Hab Ha; split=> n x ??.
apply HΨ with n a; auto. by symmetry; apply Hab with x. by apply Ha.
Qed.
Lemma eq_equiv `{Empty M, !CMRAUnit M} {A : cofeT} (a b : A) :
- True ⊑ (a ≡ b) → a ≡ b.
+ True ⊢ (a ≡ b) → a ≡ b.
Proof.
unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
apply cmra_valid_validN, cmra_unit_valid.
Qed.
-Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
+Lemma iff_equiv P Q : True ⊢ (P ↔ Q) → P ⊣⊢ Q.
Proof.
rewrite /uPred_iff; unseal=> HPQ.
split=> n x ?; split; intros; by apply HPQ with n x.
Qed.
(* Derived logical stuff *)
-Lemma True_intro P : P ⊑ True.
+Lemma True_intro P : P ⊢ True.
Proof. by apply const_intro. Qed.
-Lemma and_elim_l' P Q R : P ⊑ R → (P ∧ Q) ⊑ R.
+Lemma and_elim_l' P Q R : P ⊢ R → (P ∧ Q) ⊢ R.
Proof. by rewrite and_elim_l. Qed.
-Lemma and_elim_r' P Q R : Q ⊑ R → (P ∧ Q) ⊑ R.
+Lemma and_elim_r' P Q R : Q ⊢ R → (P ∧ Q) ⊢ R.
Proof. by rewrite and_elim_r. Qed.
-Lemma or_intro_l' P Q R : P ⊑ Q → P ⊑ (Q ∨ R).
+Lemma or_intro_l' P Q R : P ⊢ Q → P ⊢ (Q ∨ R).
Proof. intros ->; apply or_intro_l. Qed.
-Lemma or_intro_r' P Q R : P ⊑ R → P ⊑ (Q ∨ R).
+Lemma or_intro_r' P Q R : P ⊢ R → P ⊢ (Q ∨ R).
Proof. intros ->; apply or_intro_r. Qed.
-Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊑ Ψ a → P ⊑ (∃ a, Ψ a).
+Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊢ Ψ a → P ⊢ (∃ a, Ψ a).
Proof. intros ->; apply exist_intro. Qed.
-Lemma forall_elim' {A} P (Ψ : A → uPred M) : P ⊑ (∀ a, Ψ a) → (∀ a, P ⊑ Ψ a).
+Lemma forall_elim' {A} P (Ψ : A → uPred M) : P ⊢ (∀ a, Ψ a) → (∀ a, P ⊢ Ψ a).
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
-Lemma impl_intro_l P Q R : (Q ∧ P) ⊑ R → P ⊑ (Q → R).
+Lemma impl_intro_l P Q R : (Q ∧ P) ⊢ R → P ⊢ (Q → R).
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
-Lemma impl_elim_l P Q : ((P → Q) ∧ P) ⊑ Q.
+Lemma impl_elim_l P Q : ((P → Q) ∧ P) ⊢ Q.
Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_r P Q : (P ∧ (P → Q)) ⊑ Q.
+Lemma impl_elim_r P Q : (P ∧ (P → Q)) ⊢ Q.
Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_l' P Q R : P ⊑ (Q → R) → (P ∧ Q) ⊑ R.
+Lemma impl_elim_l' P Q R : P ⊢ (Q → R) → (P ∧ Q) ⊢ R.
Proof. intros; apply impl_elim with Q; auto. Qed.
-Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
+Lemma impl_elim_r' P Q R : Q ⊢ (P → R) → (P ∧ Q) ⊢ R.
Proof. intros; apply impl_elim with P; auto. Qed.
-Lemma impl_entails P Q : True ⊑ (P → Q) → P ⊑ Q.
+Lemma impl_entails P Q : True ⊢ (P → Q) → P ⊢ Q.
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
-Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
+Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ (P → Q).
Proof. auto using impl_intro_l. Qed.
-Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■φ1 ⊑ ■φ2.
+Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■φ1 ⊢ ■φ2.
Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
-Lemma and_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∧ P') ⊑ (Q ∧ Q').
+Lemma and_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ∧ P') ⊢ (Q ∧ Q').
Proof. auto. Qed.
-Lemma and_mono_l P P' Q : P ⊑ Q → (P ∧ P') ⊑ (Q ∧ P').
+Lemma and_mono_l P P' Q : P ⊢ Q → (P ∧ P') ⊢ (Q ∧ P').
Proof. by intros; apply and_mono. Qed.
-Lemma and_mono_r P P' Q' : P' ⊑ Q' → (P ∧ P') ⊑ (P ∧ Q').
+Lemma and_mono_r P P' Q' : P' ⊢ Q' → (P ∧ P') ⊢ (P ∧ Q').
Proof. by apply and_mono. Qed.
-Lemma or_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∨ P') ⊑ (Q ∨ Q').
+Lemma or_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ∨ P') ⊢ (Q ∨ Q').
Proof. auto. Qed.
-Lemma or_mono_l P P' Q : P ⊑ Q → (P ∨ P') ⊑ (Q ∨ P').
+Lemma or_mono_l P P' Q : P ⊢ Q → (P ∨ P') ⊢ (Q ∨ P').
Proof. by intros; apply or_mono. Qed.
-Lemma or_mono_r P P' Q' : P' ⊑ Q' → (P ∨ P') ⊑ (P ∨ Q').
+Lemma or_mono_r P P' Q' : P' ⊢ Q' → (P ∨ P') ⊢ (P ∨ Q').
Proof. by apply or_mono. Qed.
-Lemma impl_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P → P') ⊑ (Q → Q').
+Lemma impl_mono P P' Q Q' : Q ⊢ P → P' ⊢ Q' → (P → P') ⊢ (Q → Q').
Proof.
intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
apply impl_elim with P; eauto.
Qed.
Lemma forall_mono {A} (Φ Ψ : A → uPred M) :
- (∀ a, Φ a ⊑ Ψ a) → (∀ a, Φ a) ⊑ (∀ a, Ψ a).
+ (∀ a, Φ a ⊢ Ψ a) → (∀ a, Φ a) ⊢ (∀ a, Ψ a).
Proof.
intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
Qed.
Lemma exist_mono {A} (Φ Ψ : A → uPred M) :
- (∀ a, Φ a ⊑ Ψ a) → (∃ a, Φ a) ⊑ (∃ a, Ψ a).
+ (∀ a, Φ a ⊢ Ψ a) → (∃ a, Φ a) ⊢ (∃ a, Ψ a).
Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
-Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
+Global Instance const_mono' : Proper (impl ==> (⊢)) (@uPred_const M).
Proof. intros φ1 φ2; apply const_mono. Qed.
-Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
+Global Instance and_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
Global Instance and_flip_mono' :
- Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_and M).
+ Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_and M).
Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
-Global Instance or_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_or M).
+Global Instance or_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance or_flip_mono' :
- Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_or M).
+ Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_or M).
Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
Global Instance impl_mono' :
- Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_impl M).
+ Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_impl M).
Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
Global Instance forall_mono' A :
- Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_forall M A).
+ Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_forall M A).
Proof. intros P1 P2; apply forall_mono. Qed.
Global Instance exist_mono' A :
- Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_exist M A).
+ Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A).
Proof. intros P1 P2; apply exist_mono. Qed.
-Global Instance and_idem : IdemP (≡) (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_idem : IdemP (≡) (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_comm : Comm (≡) (@uPred_and M).
-Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_and : LeftId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_True : RightId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance False_and : LeftAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_False : RightAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_or : LeftAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_True : RightAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance False_or : LeftId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_False : RightId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_assoc : Assoc (≡) (@uPred_and M).
-Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_comm : Comm (≡) (@uPred_or M).
-Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_assoc : Assoc (≡) (@uPred_or M).
-Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M).
-Proof.
- intros P; apply (anti_symm (⊑)).
+Global Instance and_idem : IdemP (⊣⊢) (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance or_idem : IdemP (⊣⊢) (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance and_comm : Comm (⊣⊢) (@uPred_and M).
+Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
+Global Instance True_and : LeftId (⊣⊢) True%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance and_True : RightId (⊣⊢) True%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance and_False : RightAbsorb (⊣⊢) False%I (@uPred_and M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance or_True : RightAbsorb (⊣⊢) True%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance False_or : LeftId (⊣⊢) False%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance or_False : RightId (⊣⊢) False%I (@uPred_or M).
+Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
+Global Instance and_assoc : Assoc (⊣⊢) (@uPred_and M).
+Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
+Global Instance or_comm : Comm (⊣⊢) (@uPred_or M).
+Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
+Global Instance or_assoc : Assoc (⊣⊢) (@uPred_or M).
+Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
+Global Instance True_impl : LeftId (⊣⊢) True%I (@uPred_impl M).
+Proof.
+ intros P; apply (anti_symm (⊢)).
- by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
- by apply impl_intro_l; rewrite left_id.
Qed.
-Lemma iff_refl Q P : Q ⊑ (P ↔ P).
+Lemma iff_refl Q P : Q ⊢ (P ↔ P).
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
+Lemma or_and_l P Q R : (P ∨ Q ∧ R) ⊣⊢ ((P ∨ Q) ∧ (P ∨ R)).
Proof.
- apply (anti_symm (⊑)); first auto.
+ apply (anti_symm (⊢)); first auto.
do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
Qed.
-Lemma or_and_r P Q R : (P ∧ Q ∨ R)%I ≡ ((P ∨ R) ∧ (Q ∨ R))%I.
+Lemma or_and_r P Q R : (P ∧ Q ∨ R) ⊣⊢ ((P ∨ R) ∧ (Q ∨ R)).
Proof. by rewrite -!(comm _ R) or_and_l. Qed.
-Lemma and_or_l P Q R : (P ∧ (Q ∨ R))%I ≡ (P ∧ Q ∨ P ∧ R)%I.
+Lemma and_or_l P Q R : (P ∧ (Q ∨ R)) ⊣⊢ (P ∧ Q ∨ P ∧ R).
Proof.
- apply (anti_symm (⊑)); last auto.
+ apply (anti_symm (⊢)); last auto.
apply impl_elim_r', or_elim; apply impl_intro_l; auto.
Qed.
-Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I.
+Lemma and_or_r P Q R : ((P ∨ Q) ∧ R) ⊣⊢ (P ∧ R ∨ Q ∧ R).
Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Ψ : A → uPred M) : (P ∧ ∃ a, Ψ a)%I ≡ (∃ a, P ∧ Ψ a)%I.
+Lemma and_exist_l {A} P (Ψ : A → uPred M) : (P ∧ ∃ a, Ψ a) ⊣⊢ (∃ a, P ∧ Ψ a).
Proof.
- apply (anti_symm (⊑)).
+ apply (anti_symm (⊢)).
- apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
by rewrite -(exist_intro a).
- apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
by rewrite -(exist_intro a) and_elim_r.
Qed.
-Lemma and_exist_r {A} P (Φ: A → uPred M) : ((∃ a, Φ a) ∧ P)%I ≡ (∃ a, Φ a ∧ P)%I.
+Lemma and_exist_r {A} P (Φ: A → uPred M) : ((∃ a, Φ a) ∧ P) ⊣⊢ (∃ a, Φ a ∧ P).
Proof.
rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
Qed.
-Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
+Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊢ R → Q ⊢ R.
Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
+Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊢ R → Q ⊢ R.
Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_impl φ Q R : φ → Q ⊑ (■φ → R) → Q ⊑ R.
+Lemma const_intro_impl φ Q R : φ → Q ⊢ (■φ → R) → Q ⊢ R.
Proof. intros ? ->. eauto using const_intro_l, impl_elim_r. Qed.
-Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■φ ∧ Q) ⊑ R.
+Lemma const_elim_l φ Q R : (φ → Q ⊢ R) → (■φ ∧ Q) ⊢ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■φ) ⊑ R.
+Lemma const_elim_r φ Q R : (φ → Q ⊢ R) → (Q ∧ ■φ) ⊢ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_equiv (φ : Prop) : φ → (■φ : uPred M)%I ≡ True%I.
+Lemma const_equiv (φ : Prop) : φ → (■φ) ⊣⊢ True.
Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
+Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ (a ≡ b).
Proof. intros ->; apply eq_refl. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
+Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊢ (b ≡ a).
Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_proper. Qed.
(* BI connectives *)
-Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
+Lemma sep_mono P P' Q Q' : P ⊢ Q → P' ⊢ Q' → (P ★ P') ⊢ (Q ★ Q').
Proof.
intros HQ HQ'; unseal.
split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
Qed.
-Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
+Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M).
Proof.
intros P; unseal; split=> n x Hvalid; split.
- intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- by intros ?; exists (core x), x; rewrite cmra_core_l.
Qed.
-Global Instance sep_comm : Comm (≡) (@uPred_sep M).
+Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
Proof.
by intros P Q; unseal; split=> n x ?; split;
intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
Qed.
-Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
+Global Instance sep_assoc : Assoc (⊣⊢) (@uPred_sep M).
Proof.
intros P Q R; unseal; split=> n x ?; split.
- intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_and?; auto.
@@ -706,13 +709,13 @@ Proof.
+ by rewrite (assoc op) -Hy -Hx.
+ by exists y2, x2.
Qed.
-Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
+Lemma wand_intro_r P Q R : (P ★ Q) ⊢ R → P ⊢ (Q -★ R).
Proof.
unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
exists x, x'; split_and?; auto.
eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
Qed.
-Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
+Lemma wand_elim_l' P Q R : P ⊢ (Q -★ R) → (P ★ Q) ⊢ R.
Proof.
unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
eapply HPQR; eauto using cmra_validN_op_l.
@@ -720,224 +723,224 @@ Qed.
(* Derived BI Stuff *)
Hint Resolve sep_mono.
-Lemma sep_mono_l P P' Q : P ⊑ Q → (P ★ P') ⊑ (Q ★ P').
+Lemma sep_mono_l P P' Q : P ⊢ Q → (P ★ P') ⊢ (Q ★ P').
Proof. by intros; apply sep_mono. Qed.
-Lemma sep_mono_r P P' Q' : P' ⊑ Q' → (P ★ P') ⊑ (P ★ Q').
+Lemma sep_mono_r P P' Q' : P' ⊢ Q' → (P ★ P') ⊢ (P ★ Q').
Proof. by apply sep_mono. Qed.
-Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
+Global Instance sep_mono' : Proper ((⊢) ==> (⊢) ==> (⊢)) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
Global Instance sep_flip_mono' :
- Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_sep M).
+ Proper (flip (⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_sep M).
Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Lemma wand_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P -★ P') ⊑ (Q -★ Q').
+Lemma wand_mono P P' Q Q' : Q ⊢ P → P' ⊢ Q' → (P -★ P') ⊢ (Q -★ Q').
Proof.
intros HP HQ; apply wand_intro_r. rewrite HP -HQ. by apply wand_elim_l'.
Qed.
-Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wand M).
+Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_wand M).
Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
-Global Instance sep_True : RightId (≡) True%I (@uPred_sep M).
+Global Instance sep_True : RightId (⊣⊢) True%I (@uPred_sep M).
Proof. by intros P; rewrite comm left_id. Qed.
-Lemma sep_elim_l P Q : (P ★ Q) ⊑ P.
+Lemma sep_elim_l P Q : (P ★ Q) ⊢ P.
Proof. by rewrite (True_intro Q) right_id. Qed.
-Lemma sep_elim_r P Q : (P ★ Q) ⊑ Q.
+Lemma sep_elim_r P Q : (P ★ Q) ⊢ Q.
Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
-Lemma sep_elim_l' P Q R : P ⊑ R → (P ★ Q) ⊑ R.
+Lemma sep_elim_l' P Q R : P ⊢ R → (P ★ Q) ⊢ R.
Proof. intros ->; apply sep_elim_l. Qed.
-Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
+Lemma sep_elim_r' P Q R : Q ⊢ R → (P ★ Q) ⊢ R.
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
-Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
+Lemma sep_intro_True_l P Q R : True ⊢ P → R ⊢ Q → R ⊢ (P ★ Q).
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
+Lemma sep_intro_True_r P Q R : R ⊢ P → True ⊢ Q → R ⊢ (P ★ Q).
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_elim_True_l P Q R : True ⊑ P → (P ★ R) ⊑ Q → R ⊑ Q.
+Lemma sep_elim_True_l P Q R : True ⊢ P → (P ★ R) ⊢ Q → R ⊢ Q.
Proof. by intros HP; rewrite -HP left_id. Qed.
-Lemma sep_elim_True_r P Q R : True ⊑ P → (R ★ P) ⊑ Q → R ⊑ Q.
+Lemma sep_elim_True_r P Q R : True ⊢ P → (R ★ P) ⊢ Q → R ⊢ Q.
Proof. by intros HP; rewrite -HP right_id. Qed.
-Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
+Lemma wand_intro_l P Q R : (Q ★ P) ⊢ R → P ⊢ (Q -★ R).
Proof. rewrite comm; apply wand_intro_r. Qed.
-Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
+Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊢ Q.
Proof. by apply wand_elim_l'. Qed.
-Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.
+Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊢ Q.
Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
-Lemma wand_elim_r' P Q R : Q ⊑ (P -★ R) → (P ★ Q) ⊑ R.
+Lemma wand_elim_r' P Q R : Q ⊢ (P -★ R) → (P ★ Q) ⊢ R.
Proof. intros ->; apply wand_elim_r. Qed.
-Lemma wand_apply_l P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Lemma wand_apply_l P Q Q' R R' : P ⊢ (Q' -★ R') → R' ⊢ R → Q ⊢ Q' → (P ★ Q) ⊢ R.
Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : P ⊑ (Q' -★ R') → R' ⊑ R → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Lemma wand_apply_r P Q Q' R R' : P ⊢ (Q' -★ R') → R' ⊢ R → Q ⊢ Q' → (Q ★ P) ⊢ R.
Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (P ★ Q) ⊑ R.
+Lemma wand_apply_l' P Q Q' R : P ⊢ (Q' -★ R) → Q ⊢ Q' → (P ★ Q) ⊢ R.
Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : P ⊑ (Q' -★ R) → Q ⊑ Q' → (Q ★ P) ⊑ R.
+Lemma wand_apply_r' P Q Q' R : P ⊢ (Q' -★ R) → Q ⊢ Q' → (Q ★ P) ⊢ R.
Proof. intros -> <-; apply wand_elim_r. Qed.
-Lemma wand_frame_l P Q R : (Q -★ R) ⊑ (P ★ Q -★ P ★ R).
+Lemma wand_frame_l P Q R : (Q -★ R) ⊢ (P ★ Q -★ P ★ R).
Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
-Lemma wand_frame_r P Q R : (Q -★ R) ⊑ (Q ★ P -★ R ★ P).
+Lemma wand_frame_r P Q R : (Q -★ R) ⊢ (Q ★ P -★ R ★ P).
Proof.
apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
apply sep_mono_r, wand_elim_r.
Qed.
-Lemma wand_diag P : (P -★ P)%I ≡ True%I.
+Lemma wand_diag P : (P -★ P) ⊣⊢ True.
Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
-Lemma wand_True P : (True -★ P)%I ≡ P.
+Lemma wand_True P : (True -★ P) ⊣⊢ P.
Proof.
apply (anti_symm _); last by auto using wand_intro_l.
eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
Qed.
-Lemma wand_entails P Q : True ⊑ (P -★ Q) → P ⊑ Q.
+Lemma wand_entails P Q : True ⊢ (P -★ Q) → P ⊢ Q.
Proof.
intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
-Lemma entails_wand P Q : (P ⊑ Q) → True ⊑ (P -★ Q).
+Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ (P -★ Q).
Proof. auto using wand_intro_l. Qed.
-Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
+Lemma sep_and P Q : (P ★ Q) ⊢ (P ∧ Q).
Proof. auto. Qed.
-Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
+Lemma impl_wand P Q : (P → Q) ⊢ (P -★ Q).
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
-Lemma const_elim_sep_l φ Q R : (φ → Q ⊑ R) → (■φ ★ Q) ⊑ R.
+Lemma const_elim_sep_l φ Q R : (φ → Q ⊢ R) → (■φ ★ Q) ⊢ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_sep_r φ Q R : (φ → Q ⊑ R) → (Q ★ ■φ) ⊑ R.
+Lemma const_elim_sep_r φ Q R : (φ → Q ⊢ R) → (Q ★ ■φ) ⊢ R.
Proof. intros; apply const_elim with φ; eauto. Qed.
-Global Instance sep_False : LeftAbsorb (≡) False%I (@uPred_sep M).
+Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto. Qed.
-Global Instance False_sep : RightAbsorb (≡) False%I (@uPred_sep M).
+Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
Proof. intros P; apply (anti_symm _); auto. Qed.
-Lemma sep_and_l P Q R : (P ★ (Q ∧ R)) ⊑ ((P ★ Q) ∧ (P ★ R)).
+Lemma sep_and_l P Q R : (P ★ (Q ∧ R)) ⊢ ((P ★ Q) ∧ (P ★ R)).
Proof. auto. Qed.
-Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊑ ((P ★ R) ∧ (Q ★ R)).
+Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊢ ((P ★ R) ∧ (Q ★ R)).
Proof. auto. Qed.
-Lemma sep_or_l P Q R : (P ★ (Q ∨ R))%I ≡ ((P ★ Q) ∨ (P ★ R))%I.
+Lemma sep_or_l P Q R : (P ★ (Q ∨ R)) ⊣⊢ ((P ★ Q) ∨ (P ★ R)).
Proof.
- apply (anti_symm (⊑)); last by eauto 8.
+ apply (anti_symm (⊢)); last by eauto 8.
apply wand_elim_r', or_elim; apply wand_intro_l.
- by apply or_intro_l.
- by apply or_intro_r.
Qed.
-Lemma sep_or_r P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
+Lemma sep_or_r P Q R : ((P ∨ Q) ★ R) ⊣⊢ ((P ★ R) ∨ (Q ★ R)).
Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Ψ : A → uPred M) : (P ★ ∃ a, Ψ a)%I ≡ (∃ a, P ★ Ψ a)%I.
+Lemma sep_exist_l {A} P (Ψ : A → uPred M) : (P ★ ∃ a, Ψ a) ⊣⊢ (∃ a, P ★ Ψ a).
Proof.
- intros; apply (anti_symm (⊑)).
+ intros; apply (anti_symm (⊢)).
- apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
by rewrite -(exist_intro a).
- apply exist_elim=> a; apply sep_mono; auto using exist_intro.
Qed.
-Lemma sep_exist_r {A} (Φ: A → uPred M) Q: ((∃ a, Φ a) ★ Q)%I ≡ (∃ a, Φ a ★ Q)%I.
+Lemma sep_exist_r {A} (Φ: A → uPred M) Q: ((∃ a, Φ a) ★ Q) ⊣⊢ (∃ a, Φ a ★ Q).
Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
-Lemma sep_forall_l {A} P (Ψ : A → uPred M) : (P ★ ∀ a, Ψ a) ⊑ (∀ a, P ★ Ψ a).
+Lemma sep_forall_l {A} P (Ψ : A → uPred M) : (P ★ ∀ a, Ψ a) ⊢ (∀ a, P ★ Ψ a).
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊑ (∀ a, Φ a ★ Q).
+Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊢ (∀ a, Φ a ★ Q).
Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Always *)
-Lemma always_const φ : (□ ■φ : uPred M)%I ≡ (■φ)%I.
+Lemma always_const φ : (□ ■φ) ⊣⊢ (■φ).
Proof. by unseal. Qed.
-Lemma always_elim P : □ P ⊑ P.
+Lemma always_elim P : □ P ⊢ P.
Proof.
unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_core.
Qed.
-Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
+Lemma always_intro' P Q : □ P ⊢ Q → □ P ⊢ □ Q.
Proof.
unseal=> HPQ.
split=> n x ??; apply HPQ; simpl; auto using cmra_core_validN.
by rewrite cmra_core_idemp.
Qed.
-Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
+Lemma always_and P Q : (□ (P ∧ Q)) ⊣⊢ (□ P ∧ □ Q).
Proof. by unseal. Qed.
-Lemma always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
+Lemma always_or P Q : (□ (P ∨ Q)) ⊣⊢ (□ P ∨ □ Q).
Proof. by unseal. Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a)%I ≡ (∀ a, □ Ψ a)%I.
+Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
Proof. by unseal. Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a, □ Ψ a)%I.
+Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
Proof. by unseal. Qed.
-Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
+Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ★ Q).
Proof.
unseal; split=> n x ? [??].
exists (core x), (core x); rewrite cmra_core_core; auto.
Qed.
-Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
+Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊢ (□ P ★ Q).
Proof.
unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
by rewrite cmra_core_l cmra_core_idemp.
Qed.
-Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
+Lemma always_later P : (□ ▷ P) ⊣⊢ (▷ □ P).
Proof. by unseal. Qed.
(* Always derived *)
-Lemma always_mono P Q : P ⊑ Q → □ P ⊑ □ Q.
+Lemma always_mono P Q : P ⊢ Q → □ P ⊢ □ Q.
Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
Hint Resolve always_mono.
-Global Instance always_mono' : Proper ((⊑) ==> (⊑)) (@uPred_always M).
+Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
Global Instance always_flip_mono' :
- Proper (flip (⊑) ==> flip (⊑)) (@uPred_always M).
+ Proper (flip (⊢) ==> flip (⊢)) (@uPred_always M).
Proof. intros P Q; apply always_mono. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊑ (□ P → □ Q).
+Lemma always_impl P Q : □ (P → Q) ⊢ (□ P → □ Q).
Proof.
apply impl_intro_l; rewrite -always_and.
apply always_mono, impl_elim with P; auto.
Qed.
-Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b))%I ≡ (a ≡ b : uPred M)%I.
+Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b)) ⊣⊢ (a ≡ b).
Proof.
- apply (anti_symm (⊑)); auto using always_elim.
+ apply (anti_symm (⊢)); auto using always_elim.
apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
rewrite -(eq_refl a True) always_const; auto.
Qed.
-Lemma always_and_sep P Q : (□ (P ∧ Q))%I ≡ (□ (P ★ Q))%I.
-Proof. apply (anti_symm (⊑)); auto using always_and_sep_1. Qed.
-Lemma always_and_sep_l' P Q : (□ P ∧ Q)%I ≡ (□ P ★ Q)%I.
-Proof. apply (anti_symm (⊑)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : (P ∧ □ Q)%I ≡ (P ★ □ Q)%I.
+Lemma always_and_sep P Q : (□ (P ∧ Q)) ⊣⊢ (□ (P ★ Q)).
+Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
+Lemma always_and_sep_l' P Q : (□ P ∧ Q) ⊣⊢ (□ P ★ Q).
+Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
+Lemma always_and_sep_r' P Q : (P ∧ □ Q) ⊣⊢ (P ★ □ Q).
Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep P Q : (□ (P ★ Q))%I ≡ (□ P ★ □ Q)%I.
+Lemma always_sep P Q : (□ (P ★ Q)) ⊣⊢ (□ P ★ □ Q).
Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_wand P Q : □ (P -★ Q) ⊑ (□ P -★ □ Q).
+Lemma always_wand P Q : □ (P -★ Q) ⊢ (□ P -★ □ Q).
Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_sep_dup' P : (□ P)%I ≡ (□ P ★ □ P)%I.
+Lemma always_sep_dup' P : (□ P) ⊣⊢ (□ P ★ □ P).
Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
-Lemma always_wand_impl P Q : (□ (P -★ Q))%I ≡ (□ (P → Q))%I.
+Lemma always_wand_impl P Q : (□ (P -★ Q)) ⊣⊢ (□ (P → Q)).
Proof.
- apply (anti_symm (⊑)); [|by rewrite -impl_wand].
+ apply (anti_symm (⊢)); [|by rewrite -impl_wand].
apply always_intro', impl_intro_r.
by rewrite always_and_sep_l' always_elim wand_elim_l.
Qed.
-Lemma always_entails_l' P Q : (P ⊑ □ Q) → P ⊑ (□ Q ★ P).
+Lemma always_entails_l' P Q : (P ⊢ □ Q) → P ⊢ (□ Q ★ P).
Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
+Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ (P ★ □ Q).
Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
(* Later *)
-Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
+Lemma later_mono P Q : P ⊢ Q → ▷ P ⊢ ▷ Q.
Proof.
unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
Qed.
-Lemma later_intro P : P ⊑ ▷ P.
+Lemma later_intro P : P ⊢ ▷ P.
Proof.
unseal; split=> -[|n] x ??; simpl in *; [done|].
apply uPred_weaken with (S n) x; eauto using cmra_validN_S.
Qed.
-Lemma löb P : (▷ P → P) ⊑ P.
+Lemma löb P : (▷ P → P) ⊢ P.
Proof.
unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S.
Qed.
-Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
+Lemma later_and P Q : (▷ (P ∧ Q)) ⊣⊢ (▷ P ∧ ▷ Q).
Proof. unseal; split=> -[|n] x; by split. Qed.
-Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
+Lemma later_or P Q : (▷ (P ∨ Q)) ⊣⊢ (▷ P ∨ ▷ Q).
Proof. unseal; split=> -[|n] x; simpl; tauto. Qed.
-Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
+Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
Proof. unseal; by split=> -[|n] x. Qed.
-Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
+Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a).
Proof. unseal; by split=> -[|[|n]] x. Qed.
Lemma later_exist' `{Inhabited A} (Φ : A → uPred M) :
- (▷ ∃ a, Φ a)%I ⊑ (∃ a, ▷ Φ a)%I.
+ (▷ ∃ a, Φ a)%I ⊢ (∃ a, ▷ Φ a)%I.
Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed.
-Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
+Lemma later_sep P Q : (▷ (P ★ Q)) ⊣⊢ (▷ P ★ ▷ Q).
Proof.
unseal; split=> n x ?; split.
- destruct n as [|n]; simpl.
@@ -950,33 +953,33 @@ Proof.
Qed.
(* Later derived *)
-Global Instance later_mono' : Proper ((⊑) ==> (⊑)) (@uPred_later M).
+Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
- Proper (flip (⊑) ==> flip (⊑)) (@uPred_later M).
+ Proper (flip (⊢) ==> flip (⊢)) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
-Lemma later_True : (▷ True : uPred M)%I ≡ True%I.
-Proof. apply (anti_symm (⊑)); auto using later_intro. Qed.
-Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q).
+Lemma later_True : (▷ True) ⊣⊢ True.
+Proof. apply (anti_symm (⊢)); auto using later_intro. Qed.
+Lemma later_impl P Q : ▷ (P → Q) ⊢ (▷ P → ▷ Q).
Proof.
apply impl_intro_l; rewrite -later_and.
apply later_mono, impl_elim with P; auto.
Qed.
Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
- (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
+ (▷ ∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed.
-Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
+Lemma later_wand P Q : ▷ (P -★ Q) ⊢ (▷ P -★ ▷ Q).
Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
-Lemma later_iff P Q : (▷ (P ↔ Q)) ⊑ (▷ P ↔ ▷ Q).
+Lemma later_iff P Q : (▷ (P ↔ Q)) ⊢ (▷ P ↔ ▷ Q).
Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
-Lemma löb_strong P Q : (P ∧ ▷ Q) ⊑ Q → P ⊑ Q.
+Lemma löb_strong P Q : (P ∧ ▷ Q) ⊢ Q → P ⊢ Q.
Proof.
intros Hlöb. apply impl_entails. rewrite -(löb (P → Q)).
apply entails_impl, impl_intro_l. rewrite -{2}Hlöb.
apply and_intro; first by eauto.
by rewrite {1}(later_intro P) later_impl impl_elim_r.
Qed.
-Lemma löb_strong_sep P Q : (P ★ ▷ (P -★ Q)) ⊑ Q → P ⊑ Q.
+Lemma löb_strong_sep P Q : (P ★ ▷ (P -★ Q)) ⊢ Q → P ⊢ Q.
Proof.
move/wand_intro_l=>Hlöb. apply impl_entails.
rewrite -[(_ → _)%I]always_elim. apply löb_strong.
@@ -985,7 +988,7 @@ Qed.
(* Own *)
Lemma ownM_op (a1 a2 : M) :
- uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
+ uPred_ownM (a1 ⋅ a2) ⊣⊢ (uPred_ownM a1 ★ uPred_ownM a2).
Proof.
unseal; split=> n x ?; split.
- intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
@@ -994,60 +997,60 @@ Proof.
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
-Lemma always_ownM_core (a : M) : (□ uPred_ownM (core a))%I ≡ uPred_ownM (core a).
+Lemma always_ownM_core (a : M) : (□ uPred_ownM (core a)) ⊣⊢ uPred_ownM (core a).
Proof.
split=> n x; split; [by apply always_elim|unseal; intros [a' Hx]]; simpl.
rewrite -(cmra_core_idemp a) Hx.
apply cmra_core_preservingN, cmra_includedN_l.
Qed.
-Lemma always_ownM (a : M) : core a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
+Lemma always_ownM (a : M) : core a ≡ a → (□ uPred_ownM a) ⊣⊢ uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_core. Qed.
-Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
+Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
-Lemma ownM_empty `{Empty M, !CMRAUnit M} : True ⊑ uPred_ownM ∅.
+Lemma ownM_empty `{Empty M, !CMRAUnit M} : True ⊢ uPred_ownM ∅.
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
(* Valid *)
-Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
+Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
Qed.
-Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
+Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
+Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
+Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a)) ⊣⊢ (✓ a).
Proof. by unseal. Qed.
-Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
+Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
(* Own and valid derived *)
-Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
+Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed.
-Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
+Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
(* Products *)
Lemma prod_equivI {A B : cofeT} (x y : A * B) :
- (x ≡ y)%I ≡ (x.1 ≡ y.1 ∧ x.2 ≡ y.2 : uPred M)%I.
+ (x ≡ y) ⊣⊢ (x.1 ≡ y.1 ∧ x.2 ≡ y.2).
Proof. by unseal. Qed.
Lemma prod_validI {A B : cmraT} (x : A * B) :
- (✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
+ (✓ x) ⊣⊢ (✓ x.1 ∧ ✓ x.2).
Proof. by unseal. Qed.
(* Later *)
Lemma later_equivI {A : cofeT} (x y : later A) :
- (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
+ (x ≡ y) ⊣⊢ (▷ (later_car x ≡ later_car y)).
Proof. by unseal. Qed.
(* Discrete *)
Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) :
- (✓ a)%I ≡ (■✓ a : uPred M)%I.
+ (✓ a) ⊣⊢ (■✓ a).
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma timeless_eq {A : cofeT} (a b : A) :
- Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
+ Timeless a → (a ≡ b) ⊣⊢ (■(a ≡ b)).
Proof.
- unseal=> ?. apply (anti_symm (⊑)); split=> n x ?; by apply (timeless_iff n).
+ unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
Qed.
(* Timeless *)
@@ -1148,19 +1151,19 @@ Global Instance default_always_stable {A} P (Ψ : A → uPred M) (mx : option A)
Proof. destruct mx; apply _. Qed.
(* Derived lemmas for always stable *)
-Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P.
-Proof. apply (anti_symm (⊑)); auto using always_elim. Qed.
-Lemma always_intro P Q `{!AlwaysStable P} : P ⊑ Q → P ⊑ □ Q.
+Lemma always_always P `{!AlwaysStable P} : (□ P) ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
+Lemma always_intro P Q `{!AlwaysStable P} : P ⊢ Q → P ⊢ □ Q.
Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!AlwaysStable P} : (P ∧ Q)%I ≡ (P ★ Q)%I.
+Lemma always_and_sep_l P Q `{!AlwaysStable P} : (P ∧ Q) ⊣⊢ (P ★ Q).
Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
+Lemma always_and_sep_r P Q `{!AlwaysStable Q} : (P ∧ Q) ⊣⊢ (P ★ Q).
Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
+Lemma always_sep_dup P `{!AlwaysStable P} : P ⊣⊢ (P ★ P).
Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (Q ★ P).
+Lemma always_entails_l P Q `{!AlwaysStable Q} : (P ⊢ Q) → P ⊢ (Q ★ P).
Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
+Lemma always_entails_r P Q `{!AlwaysStable Q} : (P ⊢ Q) → P ⊢ (P ★ Q).
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End uPred_logic.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index d9e700cb35b1177902e865f4ad20ffb06465b074..048af4aa2a1aebf5727779702db2e405fe72d44e 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -39,9 +39,9 @@ Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
(* Big ops *)
-Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).
+Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M).
+Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_ne n :
@@ -51,19 +51,19 @@ Global Instance big_sep_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_and_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_and M).
+Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_sep M).
+Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M).
+Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
-Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
+Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
@@ -71,26 +71,26 @@ Proof.
- etrans; eauto.
Qed.
-Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
+Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs)) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
+Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs)) ⊣⊢ (Π★ Ps ★ Π★ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps)%I ⊑ (Π∧ Qs)%I.
+Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps) ⊢ (Π∧ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps)%I ⊑ (Π★ Qs)%I.
+Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps) ⊢ (Π★ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
Qed.
-Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
+Lemma big_sep_and Ps : (Π★ Ps) ⊢ (Π∧ Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
-Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P.
+Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
+Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *)
@@ -100,8 +100,8 @@ Section gmap.
Implicit Types Φ Ψ : K → A → uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 :
- m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) →
- (Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ).
+ m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
+ (Π★{map m1} Φ) ⊢ (Π★{map m2} Ψ).
Proof.
intros HX HΦ. trans (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
@@ -117,36 +117,36 @@ Section gmap.
apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper m :
- Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
+ Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
Qed.
Global Instance big_sepM_mono' m :
- Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑))
+ Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
- Lemma big_sepM_empty Φ : (Π★{map ∅} Φ)%I ≡ True%I.
+ Lemma big_sepM_empty Φ : (Π★{map ∅} Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
- m !! i = None → (Π★{map <[i:=x]> m} Φ)%I ≡ (Φ i x ★ Π★{map m} Φ)%I.
+ m !! i = None → (Π★{map <[i:=x]> m} Φ) ⊣⊢ (Φ i x ★ Π★{map m} Φ).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
- Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I ≡ (Φ i x)%I.
+ Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ) ⊣⊢ (Φ i x).
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_sepM Φ Ψ m :
- (Π★{map m} (λ i x, Φ i x ★ Ψ i x))%I ≡ (Π★{map m} Φ ★ Π★{map m} Ψ)%I.
+ (Π★{map m} (λ i x, Φ i x ★ Ψ i x)) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
Qed.
- Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ)%I ≡ (Π★{map m} (λ i x, ▷ Φ i x))%I.
+ Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ) ⊣⊢ (Π★{map m} (λ i x, ▷ Φ i x)).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
@@ -161,7 +161,7 @@ Section gset.
Implicit Types Φ : A → uPred M.
Lemma big_sepS_mono Φ Ψ X Y :
- Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ).
+ Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → (Π★{set X} Φ) ⊢ (Π★{set Y} Ψ).
Proof.
intros HX HΦ. trans (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
@@ -176,38 +176,38 @@ Section gset.
apply Forall2_Forall, Forall_true=> x; apply HΦ.
Qed.
Lemma big_sepS_proper X :
- Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X).
+ Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepS_ne=> x; apply equiv_dist, HΦ.
Qed.
Lemma big_sepS_mono' X :
- Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X).
+ Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
- Lemma big_sepS_empty Φ : (Π★{set ∅} Φ)%I ≡ True%I.
+ Lemma big_sepS_empty Φ : (Π★{set ∅} Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
- x ∉ X → (Π★{set {[ x ]} ∪ X} Φ)%I ≡ (Φ x ★ Π★{set X} Φ)%I.
+ x ∉ X → (Π★{set {[ x ]} ∪ X} Φ) ⊣⊢ (Φ x ★ Π★{set X} Φ).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
- x ∈ X → (Π★{set X} Φ)%I ≡ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ)%I.
+ x ∈ X → (Π★{set X} Φ) ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ).
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
- Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I ≡ (Φ x)%I.
+ Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ) ⊣⊢ (Φ x).
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
- (Π★{set X} (λ x, Φ x ★ Ψ x))%I ≡ (Π★{set X} Φ ★ Π★{set X} Ψ)%I.
+ (Π★{set X} (λ x, Φ x ★ Ψ x)) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
- Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ)%I ≡ (Π★{set X} (λ x, ▷ Φ x))%I.
+ Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ) ⊣⊢ (Π★{set X} (λ x, ▷ Φ x)).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
diff --git a/algebra/upred_tactics.v b/algebra/upred_tactics.v
index 5fc479b605dfa96201de5f687a44971505712c29..f4b2f7bb818aad17642ef1776dc1e6b82c90a6ee 100644
--- a/algebra/upred_tactics.v
+++ b/algebra/upred_tactics.v
@@ -24,18 +24,18 @@ Module uPred_reflection. Section uPred_reflection.
Notation eval_list Σ l :=
(uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
- Lemma eval_flatten Σ e : eval Σ e ≡ eval_list Σ (flatten e).
+ Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed.
Lemma flatten_entails Σ e1 e2 :
- flatten e2 `contains` flatten e1 → eval Σ e1 ⊑ eval Σ e2.
+ flatten e2 `contains` flatten e1 → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
Qed.
Lemma flatten_equiv Σ e1 e2 :
- flatten e2 ≡ₚ flatten e1 → eval Σ e1 ≡ eval Σ e2.
+ flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Fixpoint prune (e : expr) : expr :=
@@ -54,7 +54,7 @@ Module uPred_reflection. Section uPred_reflection.
induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
Qed.
- Lemma prune_correct Σ e : eval Σ (prune e) ≡ eval Σ e.
+ Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
Proof. by rewrite !eval_flatten flatten_prune. Qed.
Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
@@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
- eval Σ e1' ⊑ eval Σ e2' → eval Σ e1 ⊑ eval Σ e2.
+ eval Σ e1' ⊢ eval Σ e2' → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
@@ -100,20 +100,20 @@ Module uPred_reflection. Section uPred_reflection.
| n :: l => ESep (EVar n) (to_expr l)
end.
Arguments to_expr !_ / : simpl nomatch.
- Lemma eval_to_expr Σ l : eval Σ (to_expr l) ≡ eval_list Σ l.
+ Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
Proof.
induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
by rewrite IH.
Qed.
Lemma split_l Σ e ns e' :
- cancel ns e = Some e' → eval Σ e ≡ (eval Σ (to_expr ns) ★ eval Σ e')%I.
+ cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ★ eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
- cancel ns e = Some e' → eval Σ e ≡ (eval Σ e' ★ eval Σ (to_expr ns))%I.
+ cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ★ eval Σ (to_expr ns)).
Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
@@ -132,16 +132,16 @@ Module uPred_reflection. Section uPred_reflection.
Ltac quote :=
match goal with
- | |- ?P1 ⊑ ?P2 =>
+ | |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
- change (eval Σ3 e1 ⊑ eval Σ3 e2) end end
+ change (eval Σ3 e1 ⊢ eval Σ3 e2) end end
end.
Ltac quote_l :=
match goal with
- | |- ?P1 ⊑ ?P2 =>
+ | |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
- change (eval Σ2 e1 ⊑ P2) end
+ change (eval Σ2 e1 ⊢ P2) end
end.
End uPred_reflection.
@@ -162,7 +162,7 @@ Ltac close_uPreds Ps tac :=
Tactic Notation "cancel" constr(Ps) :=
uPred_reflection.quote;
- let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
+ let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
@@ -172,12 +172,12 @@ Tactic Notation "cancel" constr(Ps) :=
Tactic Notation "ecancel" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Qs => cancel Qs).
-(** [to_front [P1, P2, ..]] rewrites in the premise of ⊑ such that
+(** [to_front [P1, P2, ..]] rewrites in the premise of ⊢ such that
the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
- let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
+ let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
@@ -188,7 +188,7 @@ Tactic Notation "to_front" open_constr(Ps) :=
Tactic Notation "to_back" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
- let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
+ let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
@@ -205,46 +205,46 @@ Tactic Notation "sep_split" "right:" open_constr(Ps) :=
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
to_front Ps; apply sep_mono.
-(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
+(** Assumes a goal of the shape P ⊢ ▷ Q. Alterantively, if Q
is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
- Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
+ Will turn this goal into P ⊢ Q and strip ▷ in P below ★, ∧, ∨. *)
Ltac strip_later :=
let rec strip :=
lazymatch goal with
- | |- (_ ★ _) ⊑ ▷ _ =>
+ | |- (_ ★ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_sep);
apply sep_mono; strip
- | |- (_ ∧ _) ⊑ ▷ _ =>
+ | |- (_ ∧ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_and);
apply sep_mono; strip
- | |- (_ ∨ _) ⊑ ▷ _ =>
+ | |- (_ ∨ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_or);
apply sep_mono; strip
- | |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
- | |- _ ⊑ ▷ _ => apply later_intro; reflexivity
+ | |- ▷ _ ⊢ ▷ _ => apply later_mono; reflexivity
+ | |- _ ⊢ ▷ _ => apply later_intro; reflexivity
end
in let rec shape_Q :=
lazymatch goal with
- | |- _ ⊑ (_ ★ _) =>
+ | |- _ ⊢ (_ ★ _) =>
(* Force the later on the LHS to be top-level, matching laters
below ★ on the RHS *)
etrans; first (apply equiv_entails, later_sep; reflexivity);
(* Match the arm recursively *)
apply sep_mono; shape_Q
- | |- _ ⊑ (_ ∧ _) =>
+ | |- _ ⊢ (_ ∧ _) =>
etrans; first (apply equiv_entails, later_and; reflexivity);
apply sep_mono; shape_Q
- | |- _ ⊑ (_ ∨ _) =>
+ | |- _ ⊢ (_ ∨ _) =>
etrans; first (apply equiv_entails, later_or; reflexivity);
apply sep_mono; shape_Q
- | |- _ ⊑ ▷ _ => apply later_mono; reflexivity
+ | |- _ ⊢ ▷ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in intros_revert ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
-(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
- into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
+(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2
+ into True ⊢ ∀..., ■?0... → ?1 → ?2, applies tac, and
the moves all the assumptions back. *)
(* TODO: this name may be a big too general *)
Ltac revert_all :=
@@ -256,20 +256,20 @@ Ltac revert_all :=
on the sort of the argument, which is suboptimal. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
- | |- _ ⊑ _ => apply impl_entails
+ | |- _ ⊢ _ => apply impl_entails
end.
-(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
+(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2.
It applies löb where all the Coq assumptions have been turned into logical
assumptions, then moves all the Coq assumptions back out to the context,
- applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
+ applies [tac] on the goal (now of the form _ ⊢ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started,
but with an additional assumption ★-ed to the context *)
Ltac löb tac :=
revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
- (* We now have a goal for the form True ⊑ P, with the "original" conclusion
+ (* We now have a goal for the form True ⊢ P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
@@ -278,13 +278,13 @@ Ltac löb tac :=
do the work *)
let rec go :=
lazymatch goal with
- | |- _ ⊑ (∀ _, _) =>
+ | |- _ ⊢ (∀ _, _) =>
apply forall_intro; let H := fresh in intro H; go; revert H
- | |- _ ⊑ (■_ → _) =>
+ | |- _ ⊢ (■_ → _) =>
apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)
- | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l;
+ | |- ▷ □ ?R ⊢ (?L → _) => apply impl_intro_l;
trans (L ★ ▷ □ R)%I;
[eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]
end
diff --git a/barrier/client.v b/barrier/client.v
index c630e7da05f3a23d6ddfa94d2c529c1d7068778f..e68492fb9070d15d35fe41010bfa1f8f1ba90d0e 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -16,19 +16,19 @@ Section client.
Local Notation iProp := (iPropG heap_lang Σ).
Definition y_inv q y : iProp :=
- (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, #> f #n {{ λ v, v = #(n + 42) }})%I.
+ (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, WP f #n {{ λ v, v = #(n + 42) }})%I.
Lemma y_inv_split q y :
- y_inv q y ⊑ (y_inv (q/2) y ★ y_inv (q/2) y).
+ y_inv q y ⊢ (y_inv (q/2) y ★ y_inv (q/2) y).
Proof.
rewrite /y_inv. apply exist_elim=>f.
rewrite -!(exist_intro f). rewrite heap_mapsto_op_split.
- ecancel [y ↦{_} _; y ↦{_} _]%I. by rewrite [X in X ⊑ _]always_sep_dup.
+ ecancel [y ↦{_} _; y ↦{_} _]%I. by rewrite [X in X ⊢ _]always_sep_dup.
Qed.
Lemma worker_safe q (n : Z) (b y : loc) :
(heap_ctx heapN ★ recv heapN N b (y_inv q y))
- ⊑ #> worker n (%b) (%y) {{ λ _, True }}.
+ ⊢ WP worker n (%b) (%y) {{ λ _, True }}.
Proof.
rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
rewrite comm. apply sep_mono_r. apply wand_intro_l.
@@ -42,7 +42,7 @@ Section client.
Qed.
Lemma client_safe :
- heapN ⊥ N → heap_ctx heapN ⊑ #> client {{ λ _, True }}.
+ heapN ⊥ N → heap_ctx heapN ⊢ WP client {{ λ _, True }}.
Proof.
intros ?. rewrite /client.
(ewp eapply wp_alloc); eauto with I. strip_later. apply forall_intro=>y.
diff --git a/barrier/proof.v b/barrier/proof.v
index 40b99c0ade2c1ae5b6c41d4d8ab7ea628e0e90fe..378b5cfafe19382ea5595478105ff9683b412304 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
(saved_prop_own i2 R2 ★
saved_prop_own i1 R1 ★ saved_prop_own i Q ★
(Q -★ R1 ★ R2) ★ ress P I)
- ⊑ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
+ ⊢ ress P ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))).
Proof.
intros. rewrite /ress !sep_exist_l. apply exist_elim=>Ψ.
rewrite -(exist_intro (<[i1:=R1]> (<[i2:=R2]> Ψ))).
@@ -112,7 +112,7 @@ Qed.
Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
heapN ⊥ N →
(heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l))
- ⊑ #> newbarrier #() {{ Φ }}.
+ ⊢ WP newbarrier #() {{ Φ }}.
Proof.
intros HN. rewrite /newbarrier. wp_seq.
rewrite -wp_pvs. wp eapply wp_alloc; eauto with I ndisj.
@@ -151,7 +151,7 @@ Proof.
Qed.
Lemma signal_spec l P (Φ : val → iProp) :
- (send l P ★ P ★ Φ #()) ⊑ #> signal (%l) {{ Φ }}.
+ (send l P ★ P ★ Φ #()) ⊢ WP signal (%l) {{ Φ }}.
Proof.
rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
@@ -176,7 +176,7 @@ Proof.
Qed.
Lemma wait_spec l P (Φ : val → iProp) :
- (recv l P ★ (P -★ Φ #())) ⊑ #> wait (%l) {{ Φ }}.
+ (recv l P ★ (P -★ Φ #())) ⊢ WP wait (%l) {{ Φ }}.
Proof.
rename P into R. wp_rec.
rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
@@ -226,7 +226,7 @@ Qed.
Lemma recv_split E l P1 P2 :
nclose N ⊆ E →
- recv l (P1 ★ P2) ⊑ |={E}=> recv l P1 ★ recv l P2.
+ recv l (P1 ★ P2) ⊢ |={E}=> recv l P1 ★ recv l P2.
Proof.
rename P1 into R1. rename P2 into R2. intros HN.
rewrite {1}/recv /barrier_ctx.
@@ -277,7 +277,7 @@ Proof.
Qed.
Lemma recv_weaken l P1 P2 :
- (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
+ (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2).
Proof.
apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
@@ -287,7 +287,7 @@ Proof.
Qed.
Lemma recv_mono l P1 P2 :
- P1 ⊑ P2 → recv l P1 ⊑ recv l P2.
+ P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
Proof.
intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed.
diff --git a/barrier/specification.v b/barrier/specification.v
index 2f57dc41d98aba127016c3fae8239e9ca722b329..68631962e4e5ceb4d0e43bfd3845d59bbd8df56c 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -12,12 +12,12 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma barrier_spec (heapN N : namespace) :
heapN ⊥ N →
∃ recv send : loc → iProp -n> iProp,
- (∀ P, heap_ctx heapN ⊑ {{ True }} newbarrier #() {{ λ v,
+ (∀ P, heap_ctx heapN ⊢ {{ True }} newbarrier #() {{ λ v,
∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧
(∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧
(∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧
(∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧
- (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
+ (∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)).
Proof.
intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 568a937c306d5aade9cbcba1c58b0028165ddd65..32060a7df6eeba196449c02a390c52854f9d12d5 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -51,7 +51,7 @@ Note that $\COFEs$ is cartesian closed.
\begin{defn}
A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \mathbb{N}}, \mcore{-}: \monoid \nfn \monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid, (\mdiv) : \monoid \times \monoid \nfn \monoid)$ satisfying
\begin{align*}
- \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-nonexp} \\
+ \All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
\All n, m.& n \geq m \Ra V_n \subseteq V_m \tagH{cmra-valid-mono} \\
\All \melt, \meltB, \meltC.& (\melt \mtimes \meltB) \mtimes \meltC = \melt \mtimes (\meltB \mtimes \meltC) \tagH{cmra-assoc} \\
\All \melt, \meltB.& \melt \mtimes \meltB = \meltB \mtimes \melt \tagH{cmra-comm} \\
@@ -67,30 +67,16 @@ Note that $\COFEs$ is cartesian closed.
\end{align*}
\end{defn}
-\ralf{Copy the rest of the explanation from the paper, when that one is more polished.}
-
-\paragraph{The division operator $\mdiv$.}
-One way to describe $\mdiv$ is to say that it extracts the witness from the extension order: If $\melt \leq \meltB$, then $\melt \mdiv \meltB$ computes the difference between the two elements (\ruleref{cmra-div-op}).
-Otherwise, $\mdiv$ can have arbitrary behavior.
-This means that, in classical logic, the division operator can be defined for any PCM using the axiom of choice, and it will trivially satisfy \ruleref{cmra-div-op}.
-However, notice that the division operator also has to be \emph{non-expansive} --- so if the carrier $\monoid$ is equipped with a non-trivial $\nequiv{n}$, there is an additional proof obligation here.
-This is crucial, for the following reason:
-Considering that the extension order is defined using \emph{equality}, there is a natural notion of a \emph{step-indexed extension} order using the step-indexed equivalence of the underlying COFE:
-\[ \melt \mincl{n} \meltB \eqdef \Exists \meltC. \meltB \nequiv{n} \melt \mtimes \meltC \tagH{cmra-inclM} \]
-One of the properties we would expect to hold is the usual correspondence between a step-indexed predicate and its non-step-indexed counterpart:
-\[ \All \melt, \meltB. \melt \leq \meltB \Lra (\All n. \melt \mincl{n} \meltB) \tagH{cmra-incl-limit} \]
-The right-to-left direction here is trick.
-For every $n$, we obtain a proof that $\melt \mincl{n} \meltB$.
-From this, we could extract a sequence of witnesses $(\meltC_m)_{m}$, and we need to arrive at a single witness $\meltC$ showing that $\melt \leq \meltB$.
-Without the division operator, there is no reason to believe that such a witness exists.
-However, since we can use the division operator, and since we know that this operator is \emph{non-expansive}, we can pick $\meltC \eqdef \meltB \mdiv \melt$, and then we can prove that this is indeed the desired witness.
-\ralf{The only reason we actually have division is that we are working constructively \emph{and}, at the same time, remain compatible with a classic interpretation of the existential. This is pretty silly.}
+This is a natural generalization of RAs over COFEs.
+All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
+
+\ralf{TODO: Get rid of division.}
\paragraph{The extension axiom (\ruleref{cmra-extend}).}
Notice that the existential quantification in this axiom is \emph{constructive}, \ie it is a sigma type in Coq.
The purpose of this axiom is to compute $\melt_1$, $\melt_2$ completing the following square:
-\ralf{Needs some magic to fix the baseline of the $\nequiv{n}$, or so}
+% RJ FIXME: Needs some magic to fix the baseline of the $\nequiv{n}$, or so
\begin{center}
\begin{tikzpicture}[every edge/.style={draw=none}]
\node (a) at (0, 0) {$\melt$};
diff --git a/docs/derived.tex b/docs/derived.tex
index 1c832481e0c97d96a2bbcdddb2c0440bbf4a7810..738a87bef2ca24dc77447175b5bdde8753ccc517 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -204,7 +204,7 @@ We can derive some specialized forms of the lifting axioms for the operational s
\ralf{Add these.}
-\subsection{Global Functor and ghost ownership}
+\subsection{Global functor and ghost ownership}
\ralf{Describe this.}
% \subsection{Global monoid}
@@ -364,7 +364,7 @@ We can derive some specialized forms of the lifting axioms for the operational s
% \subsection{Ghost heap}
% \label{sec:ghostheap}%
-
+% FIXME use the finmap provided by the global ghost ownership, instead of adding our own
% We define a simple ghost heap with fractional permissions.
% Some modules require a few ghost names per module instance to properly manage ghost state, but would like to expose to clients a single logical name (avoiding clutter).
% In such cases we use these ghost heaps.
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 327bb7cc431823e0de931615ffb59918bf4ade1c..ac9b0fa0d82eafbab8fb357de536c5ece162d9b6 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -19,54 +19,54 @@ Implicit Types Φ : val → iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E x ef e v Φ :
to_val e = Some v →
- ▷ #> subst' x e ef @ E {{ Φ }} ⊑ #> App (Lam x ef) e @ E {{ Φ }}.
+ ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
Proof. intros. by rewrite -wp_rec. Qed.
Lemma wp_let E x e1 e2 v Φ :
to_val e1 = Some v →
- ▷ #> subst' x e1 e2 @ E {{ Φ }} ⊑ #> Let x e1 e2 @ E {{ Φ }}.
+ ▷ WP subst' x e1 e2 @ E {{ Φ }} ⊢ WP Let x e1 e2 @ E {{ Φ }}.
Proof. apply wp_lam. Qed.
Lemma wp_seq E e1 e2 v Φ :
to_val e1 = Some v →
- ▷ #> e2 @ E {{ Φ }} ⊑ #> Seq e1 e2 @ E {{ Φ }}.
+ ▷ WP e2 @ E {{ Φ }} ⊢ WP Seq e1 e2 @ E {{ Φ }}.
Proof. intros ?. by rewrite -wp_let. Qed.
-Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊑ #> Skip @ E {{ Φ }}.
+Lemma wp_skip E Φ : ▷ Φ (LitV LitUnit) ⊢ WP Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq // -wp_value //. Qed.
Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ #> subst' x1 e0 e1 @ E {{ Φ }} ⊑ #> Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊑ X]later_intro -wp_let. Qed.
+ ▷ WP subst' x1 e0 e1 @ E {{ Φ }} ⊢ WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
to_val e0 = Some v0 →
- ▷ #> subst' x2 e0 e2 @ E {{ Φ }} ⊑ #> Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊑ X]later_intro -wp_let. Qed.
+ ▷ WP subst' x2 e0 e2 @ E {{ Φ }} ⊢ WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊢ X]later_intro -wp_let. Qed.
Lemma wp_le E (n1 n2 : Z) P Φ :
- (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
- (n2 < n1 → P ⊑ ▷ Φ (LitV (LitBool false))) →
- P ⊑ #> BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+ (n1 ≤ n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (n2 < n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+ P ⊢ WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
Qed.
Lemma wp_lt E (n1 n2 : Z) P Φ :
- (n1 < n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
- (n2 ≤ n1 → P ⊑ ▷ Φ (LitV (LitBool false))) →
- P ⊑ #> BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+ (n1 < n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (n2 ≤ n1 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+ P ⊢ WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.
Lemma wp_eq E (n1 n2 : Z) P Φ :
- (n1 = n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
- (n1 ≠n2 → P ⊑ ▷ Φ (LitV (LitBool false))) →
- P ⊑ #> BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
+ (n1 = n2 → P ⊢ ▷ Φ (LitV (LitBool true))) →
+ (n1 ≠n2 → P ⊢ ▷ Φ (LitV (LitBool false))) →
+ P ⊢ WP BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 7f31f37b54206545ea9fe15027f778f038e852d4..875064db4f5f73475f704ecd2fee150d65579aa1 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -31,7 +31,7 @@ Section definitions.
Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
auth_ctx heap_name N heap_inv.
- Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv.
+ Global Instance heap_inv_proper : Proper ((≡) ==> (⊣⊢)) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : AlwaysStable (heap_ctx N).
Proof. apply _. Qed.
@@ -97,7 +97,7 @@ Section heap.
(** Allocation *)
Lemma heap_alloc N E σ :
authG heap_lang Σ heapR → nclose N ⊆ E →
- ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
+ ownP σ ⊢ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
Proof.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
@@ -119,30 +119,30 @@ Section heap.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v :
- (l ↦{q1} v ★ l ↦{q2} v)%I ≡ (l ↦{q1+q2} v)%I.
+ (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ (l ↦{q1+q2} v).
Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
- (l ↦{q1} v1 ★ l ↦{q2} v2)%I ≡ (v1 = v2 ∧ l ↦{q1+q2} v1)%I.
+ (l ↦{q1} v1 ★ l ↦{q2} v2) ⊣⊢ (v1 = v2 ∧ l ↦{q1+q2} v1).
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq const_equiv // left_id. }
rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
- apply (anti_symm (⊑)); last by apply const_elim_l.
+ apply (anti_symm (⊢)); last by apply const_elim_l.
rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v :
- (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
+ (l ↦{q} v) ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
(** Weakest precondition *)
Lemma wp_alloc N E e v P Φ :
to_val e = Some v →
- P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
- P ⊑ #> Alloc e @ E {{ Φ }}.
+ P ⊢ heap_ctx N → nclose N ⊆ E →
+ P ⊢ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
+ P ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HP.
trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
@@ -165,9 +165,9 @@ Section heap.
Qed.
Lemma wp_load N E l q v P Φ :
- P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) →
- P ⊑ #> Load (Loc l) @ E {{ Φ }}.
+ P ⊢ heap_ctx N → nclose N ⊆ E →
+ P ⊢ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) →
+ P ⊢ WP Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -182,9 +182,9 @@ Section heap.
Lemma wp_store N E l v' e v P Φ :
to_val e = Some v →
- P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
- P ⊑ #> Store (Loc l) e @ E {{ Φ }}.
+ P ⊢ heap_ctx N → nclose N ⊆ E →
+ P ⊢ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
+ P ⊢ WP Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
@@ -199,9 +199,9 @@ Section heap.
Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠v1 →
- P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
- P ⊑ #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
+ P ⊢ heap_ctx N → nclose N ⊆ E →
+ P ⊢ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
+ P ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
@@ -216,9 +216,9 @@ Section heap.
Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- P ⊑ heap_ctx N → nclose N ⊆ E →
- P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
- P ⊑ #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
+ P ⊢ heap_ctx N → nclose N ⊆ E →
+ P ⊢ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
+ P ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ???? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 5df7f53b56a627f6e7851e889a4335c8dfe6a93b..4cbc79cdaf7afb4d20a23b9489356e8e2089e59d 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -15,14 +15,14 @@ Implicit Types ef : option (expr []).
(** Bind. *)
Lemma wp_bind {E e} K Φ :
- #> e @ E {{ λ v, #> fill K (of_val v) @ E {{ Φ }}}} ⊑ #> fill K e @ E {{ Φ }}.
+ WP e @ E {{ λ v, WP fill K (of_val v) @ E {{ Φ }}}} ⊢ WP fill K e @ E {{ Φ }}.
Proof. apply weakestpre.wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_alloc_pst E σ e v Φ :
to_val e = Some v →
(▷ ownP σ ★ ▷ (∀ l, σ !! l = None ∧ ownP (<[l:=v]>σ) -★ Φ (LocV l)))
- ⊑ #> Alloc e @ E {{ Φ }}.
+ ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
(* TODO RJ: This works around ssreflect bug #22. *)
intros. set (φ v' σ' ef := ∃ l,
@@ -39,7 +39,7 @@ Qed.
Lemma wp_load_pst E σ l v Φ :
σ !! l = Some v →
- (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊑ #> Load (Loc l) @ E {{ Φ }}.
+ (▷ ownP σ ★ ▷ (ownP σ -★ Φ v)) ⊢ WP Load (Loc l) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ v σ None) ?right_id //;
last by intros; inv_step; eauto using to_of_val.
@@ -48,7 +48,7 @@ Qed.
Lemma wp_store_pst E σ l e v v' Φ :
to_val e = Some v → σ !! l = Some v' →
(▷ ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Φ (LitV LitUnit)))
- ⊑ #> Store (Loc l) e @ E {{ Φ }}.
+ ⊢ WP Store (Loc l) e @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto.
@@ -57,7 +57,7 @@ Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠v1 →
(▷ ownP σ ★ ▷ (ownP σ -★ Φ (LitV $ LitBool false)))
- ⊑ #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
+ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
?right_id //; last by intros; inv_step; eauto.
@@ -66,7 +66,7 @@ Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
(▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (LitV $ LitBool true)))
- ⊑ #> CAS (Loc l) e1 e2 @ E {{ Φ }}.
+ ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true)
(<[l:=v2]>σ) None) ?right_id //; last by intros; inv_step; eauto.
@@ -74,7 +74,7 @@ Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e Φ :
- (▷ Φ (LitV LitUnit) ★ ▷ #> e {{ λ _, True }}) ⊑ #> Fork e @ E {{ Φ }}.
+ (▷ Φ (LitV LitUnit) ★ ▷ WP e {{ λ _, True }}) ⊢ WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
@@ -83,8 +83,8 @@ Qed.
Lemma wp_rec E f x e1 e2 v Φ :
to_val e2 = Some v →
- ▷ #> subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
- ⊑ #> App (Rec f x e1) e2 @ E {{ Φ }}.
+ ▷ WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
+ ⊢ WP App (Rec f x e1) e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (App _ _)
(subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
@@ -94,13 +94,13 @@ Qed.
Lemma wp_rec' E f x erec e1 e2 v2 Φ :
e1 = Rec f x erec →
to_val e2 = Some v2 →
- ▷ #> subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
- ⊑ #> App e1 e2 @ E {{ Φ }}.
+ ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
+ ⊢ WP App e1 e2 @ E {{ Φ }}.
Proof. intros ->. apply wp_rec. Qed.
Lemma wp_un_op E op l l' Φ :
un_op_eval op l = Some l' →
- ▷ Φ (LitV l') ⊑ #> UnOp op (Lit l) @ E {{ Φ }}.
+ ▷ Φ (LitV l') ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
?right_id -?wp_value //; intros; inv_step; eauto.
@@ -108,21 +108,21 @@ Qed.
Lemma wp_bin_op E op l1 l2 l' Φ :
bin_op_eval op l1 l2 = Some l' →
- ▷ Φ (LitV l') ⊑ #> BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+ ▷ Φ (LitV l') ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
Proof.
intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
?right_id -?wp_value //; intros; inv_step; eauto.
Qed.
Lemma wp_if_true E e1 e2 Φ :
- ▷ #> e1 @ E {{ Φ }} ⊑ #> If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
+ ▷ WP e1 @ E {{ Φ }} ⊢ WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
?right_id //; intros; inv_step; eauto.
Qed.
Lemma wp_if_false E e1 e2 Φ :
- ▷ #> e2 @ E {{ Φ }} ⊑ #> If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
+ ▷ WP e2 @ E {{ Φ }} ⊢ WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
?right_id //; intros; inv_step; eauto.
@@ -130,7 +130,7 @@ Qed.
Lemma wp_fst E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- ▷ Φ v1 ⊑ #> Fst (Pair e1 e2) @ E {{ Φ }}.
+ ▷ Φ v1 ⊢ WP Fst (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
?right_id -?wp_value //; intros; inv_step; eauto.
@@ -138,7 +138,7 @@ Qed.
Lemma wp_snd E e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
- ▷ Φ v2 ⊑ #> Snd (Pair e1 e2) @ E {{ Φ }}.
+ ▷ Φ v2 ⊢ WP Snd (Pair e1 e2) @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
?right_id -?wp_value //; intros; inv_step; eauto.
@@ -146,7 +146,7 @@ Qed.
Lemma wp_case_inl E e0 v0 e1 e2 Φ :
to_val e0 = Some v0 →
- ▷ #> App e1 e0 @ E {{ Φ }} ⊑ #> Case (InjL e0) e1 e2 @ E {{ Φ }}.
+ ▷ WP App e1 e0 @ E {{ Φ }} ⊢ WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
(App e1 e0) None) ?right_id //; intros; inv_step; eauto.
@@ -154,7 +154,7 @@ Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Φ :
to_val e0 = Some v0 →
- ▷ #> App e2 e0 @ E {{ Φ }} ⊑ #> Case (InjR e0) e1 e2 @ E {{ Φ }}.
+ ▷ WP App e2 e0 @ E {{ Φ }} ⊢ WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _)
(App e2 e0) None) ?right_id //; intros; inv_step; eauto.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 200cccb7d1c1c20d382a11993f1d1d12608d9312..77fa2998f7f4777d1209e41ae159acfbb80cad79 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -2,12 +2,12 @@ From iris.heap_lang Require Export derived.
Export heap_lang.
Arguments wp {_ _} _ _%E _.
-Notation "#> e @ E {{ Φ } }" := (wp E e%E Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
(at level 20, e, Φ at level 200,
- format "#> e @ E {{ Φ } }") : uPred_scope.
-Notation "#> e {{ Φ } }" := (wp ⊤ e%E Φ)
+ format "'WP' e @ E {{ Φ } }") : uPred_scope.
+Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
(at level 20, e, Φ at level 200,
- format "#> e {{ Φ } }") : uPred_scope.
+ format "'WP' e {{ Φ } }") : uPred_scope.
Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit.
diff --git a/heap_lang/par.v b/heap_lang/par.v
index f65ac187fcba3059751689a55f4cc436b8f3f5ff..219cb74e8377c75adf5663d5e2275ca4ba91fa1f 100644
--- a/heap_lang/par.v
+++ b/heap_lang/par.v
@@ -21,9 +21,9 @@ Local Notation iProp := (iPropG heap_lang Σ).
Lemma par_spec (Ψ1 Ψ2 : val → iProp) e (f1 f2 : val) (Φ : val → iProp) :
heapN ⊥ N → to_val e = Some (f1,f2)%V →
- (heap_ctx heapN ★ #> f1 #() {{ Ψ1 }} ★ #> f2 #() {{ Ψ2 }} ★
+ (heap_ctx heapN ★ WP f1 #() {{ Ψ1 }} ★ WP f2 #() {{ Ψ2 }} ★
∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
- ⊑ #> par e {{ Φ }}.
+ ⊢ WP par e {{ Φ }}.
Proof.
intros. rewrite /par. ewp (by eapply wp_value). wp_let. wp_proj.
ewp (eapply spawn_spec; wp_done).
@@ -38,9 +38,9 @@ Qed.
Lemma wp_par (Ψ1 Ψ2 : val → iProp) (e1 e2 : expr []) (Φ : val → iProp) :
heapN ⊥ N →
- (heap_ctx heapN ★ #> e1 {{ Ψ1 }} ★ #> e2 {{ Ψ2 }} ★
+ (heap_ctx heapN ★ WP e1 {{ Ψ1 }} ★ WP e2 {{ Ψ2 }} ★
∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
- ⊑ #> ParV e1 e2 {{ Φ }}.
+ ⊢ WP ParV e1 e2 {{ Φ }}.
Proof.
intros. rewrite -par_spec //. repeat apply sep_mono; done || by wp_seq.
Qed.
diff --git a/heap_lang/spawn.v b/heap_lang/spawn.v
index e3db4ef0e14b1d7198754e597151ed64ee2c19a9..0db99e0b726cd4d8737fbbcb64dafa8ed5a1746f 100644
--- a/heap_lang/spawn.v
+++ b/heap_lang/spawn.v
@@ -50,8 +50,8 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
to_val e = Some f →
heapN ⊥ N →
- (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
- ⊑ #> spawn e {{ Φ }}.
+ (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ (%l))
+ ⊢ WP spawn e {{ Φ }}.
Proof.
intros Hval Hdisj. rewrite /spawn. ewp (by eapply wp_value). wp_let.
wp eapply wp_alloc; eauto with I.
@@ -61,9 +61,9 @@ Proof.
rewrite !pvs_frame_r. eapply wp_strip_pvs. rewrite !sep_exist_r.
apply exist_elim=>γ.
(* TODO: Figure out a better way to say "I want to establish â–· spawn_inv". *)
- trans (heap_ctx heapN ★ #> f #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
+ trans (heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (join_handle l Ψ -★ Φ (%l)%V) ★
own γ (Excl ()) ★ ▷ (spawn_inv γ l Ψ))%I.
- { ecancel [ #> _ {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
+ { ecancel [ WP _ {{ _ }}; _ -★ _; heap_ctx _; own _ _]%I.
rewrite -later_intro /spawn_inv -(exist_intro (InjLV #0)).
cancel [l ↦ InjLV #0]%I. by apply or_intro_l', const_intro. }
rewrite (inv_alloc N) // !pvs_frame_l. eapply wp_strip_pvs.
@@ -88,7 +88,7 @@ Qed.
Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v)
- ⊑ #> join (%l) {{ Φ }}.
+ ⊢ WP join (%l) {{ Φ }}.
Proof.
wp_rec. wp_focus (! _)%E.
rewrite {1}/join_handle sep_exist_l !sep_exist_r. apply exist_elim=>γ.
@@ -97,7 +97,7 @@ Proof.
apply wand_intro_l. rewrite /spawn_inv {1}later_exist !sep_exist_r.
apply exist_elim=>lv. rewrite later_sep.
eapply wp_load; eauto with I ndisj. cancel [▷ (l ↦ lv)]%I. strip_later.
- apply wand_intro_l. rewrite -later_intro -[X in _ ⊑ (X ★ _)](exist_intro lv).
+ apply wand_intro_l. rewrite -later_intro -[X in _ ⊢ (X ★ _)](exist_intro lv).
cancel [l ↦ lv]%I. rewrite sep_or_r. apply or_elim.
- (* Case 1 : nothing sent yet, we wait. *)
rewrite -or_intro_l. apply const_elim_sep_l=>-> {lv}.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index ce5d9c930668964ac2b4590a5ea50be39ac606a1..3745177b0ef1f48b7c6532bb3e8eaa27472e9e4b 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -24,7 +24,7 @@ Section LiftingTests.
Definition heap_e : expr [] :=
let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
Lemma heap_e_spec E N :
- nclose N ⊆ E → heap_ctx N ⊑ #> heap_e @ E {{ λ v, v = #2 }}.
+ nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ λ v, v = #2 }}.
Proof.
rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
@@ -44,7 +44,7 @@ Section LiftingTests.
Lemma FindPred_spec n1 n2 E Φ :
n1 < n2 →
- Φ #(n2 - 1) ⊑ #> FindPred #n2 #n1 @ E {{ Φ }}.
+ Φ #(n2 - 1) ⊢ WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof.
revert n1. wp_rec=>n1 Hn.
wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
@@ -53,7 +53,7 @@ Section LiftingTests.
- assert (n1 = n2 - 1) as -> by omega; auto with I.
Qed.
- Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊑ #> Pred #n @ E {{ Φ }}.
+ Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊢ WP Pred #n @ E {{ Φ }}.
Proof.
wp_lam. wp_op=> ?; wp_if.
- wp_op. wp_op.
@@ -63,7 +63,7 @@ Section LiftingTests.
Qed.
Lemma Pred_user E :
- (True : iProp) ⊑ #> let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
+ (True : iProp) ⊢ WP let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
Proof.
intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
Qed.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 8d438899ad7d89cf65cb82d54f81aea9362120a2..119a23e07f02a1d4bef97a28a1b2965f80e77862 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -11,13 +11,13 @@ Ltac wp_bind K :=
Ltac wp_finish :=
let rec go :=
match goal with
- | |- _ ⊑ ▷ _ => etrans; [|fast_by apply later_mono; go]
- | |- _ ⊑ wp _ _ _ =>
+ | |- _ ⊢ ▷ _ => etrans; [|fast_by apply later_mono; go]
+ | |- _ ⊢ wp _ _ _ =>
etrans; [|eapply wp_value_pvs; fast_done];
(* sometimes, we will have to do a final view shift, so only apply
pvs_intro if we obtain a consecutive wp *)
try (eapply pvs_intro;
- match goal with |- _ ⊑ wp _ _ _ => simpl | _ => fail end)
+ match goal with |- _ ⊢ wp _ _ _ => simpl | _ => fail end)
| _ => idtac
end in simpl; intros_revert go.
@@ -28,7 +28,7 @@ Tactic Notation "wp_rec" ">" :=
(* Find the redex and apply wp_rec *)
idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
lazymatch goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* hnf does not reduce through an of_val *)
(* match eval hnf in e1 with Rec _ _ _ => *)
@@ -39,7 +39,7 @@ Tactic Notation "wp_rec" := wp_rec>; try strip_later.
Tactic Notation "wp_lam" ">" :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with App ?e1 _ =>
(* match eval hnf in e1 with Rec BAnon _ _ => *)
wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish
@@ -54,7 +54,7 @@ Tactic Notation "wp_seq" := wp_let.
Tactic Notation "wp_op" ">" :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
| BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
@@ -69,7 +69,7 @@ Tactic Notation "wp_op" := wp_op>; try strip_later.
Tactic Notation "wp_proj" ">" :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with
| Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish
| Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish
@@ -79,7 +79,7 @@ Tactic Notation "wp_proj" := wp_proj>; try strip_later.
Tactic Notation "wp_if" ">" :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with If _ _ _ =>
wp_bind K;
etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish
@@ -89,7 +89,7 @@ Tactic Notation "wp_if" := wp_if>; try strip_later.
Tactic Notation "wp_case" ">" :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match eval hnf in e' with Case _ _ _ =>
wp_bind K;
etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
@@ -100,13 +100,13 @@ Tactic Notation "wp_case" := wp_case>; try strip_later.
Tactic Notation "wp_focus" open_constr(efoc) :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
match e' with efoc => unify e' efoc; wp_bind K end)
end.
Tactic Notation "wp" ">" tactic(tac) :=
match goal with
- | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
+ | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => wp_bind K; tac)
end.
Tactic Notation "wp" tactic(tac) := (wp> tac); [try strip_later|..].
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 7cdfcea5b93afe1852e92b3f0fff193bf4cd2dc2..0e66aca5cc8a0c65cdba3942dd3348fbbc6dddd3 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -55,7 +55,7 @@ Proof.
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
- P ⊑ #> e1 {{ Φ }} →
+ P ⊢ WP e1 {{ Φ }} →
nsteps step k ([e1],σ1) (t2,σ2) →
1 < n → wsat (k + n) ⊤ σ1 r1 →
P (k + n) r1 →
@@ -69,7 +69,7 @@ Qed.
Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
✓ m →
- (ownP σ1 ★ ownG m) ⊑ #> e1 {{ Φ }} →
+ (ownP σ1 ★ ownG m) ⊢ WP e1 {{ Φ }} →
rtc step ([e1],σ1) (t2,σ2) →
∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
Proof.
@@ -84,7 +84,7 @@ Qed.
Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
✓ m →
- (ownP σ1 ★ ownG m) ⊑ #> e @ E {{ λ v', ■φ v' }} →
+ (ownP σ1 ★ ownG m) ⊢ WP e @ E {{ λ v', ■φ v' }} →
rtc step ([e], σ1) (of_val v :: t2, σ2) →
φ v.
Proof.
@@ -110,7 +110,7 @@ Qed.
Lemma wp_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
✓ m →
- (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
+ (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2).
Proof.
@@ -128,7 +128,7 @@ Qed.
(* Connect this up to the threadpool-semantics. *)
Theorem wp_adequacy_safe E Φ e1 t2 σ1 m σ2 :
✓ m →
- (ownP σ1 ★ ownG m) ⊑ #> e1 @ E {{ Φ }} →
+ (ownP σ1 ★ ownG m) ⊢ WP e1 @ E {{ Φ }} →
rtc step ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 5189460abfe1acc2717fa4f623e71ed7d86da89e..10a3a1eaf6cf8b1605052f39f69bf9420c767047 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -26,7 +26,7 @@ Section definitions.
Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
Proof. solve_proper. Qed.
- Global Instance auth_own_proper : Proper ((≡) ==> (≡)) auth_own.
+ Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless a : TimelessP (auth_own a).
Proof. apply _. Qed.
@@ -41,21 +41,21 @@ Instance: Params (@auth_ctx) 7.
Section auth.
Context `{AuthI : authG Λ Σ A}.
- Context (φ : A → iPropG Λ Σ) {φ_proper : Proper ((≡) ==> (≡)) φ}.
+ Context (φ : A → iPropG Λ Σ) {φ_proper : Proper ((≡) ==> (⊣⊢)) φ}.
Implicit Types N : namespace.
Implicit Types P Q R : iPropG Λ Σ.
Implicit Types a b : A.
Implicit Types γ : gname.
Lemma auth_own_op γ a b :
- auth_own γ (a ⋅ b) ≡ (auth_own γ a ★ auth_own γ b)%I.
+ auth_own γ (a ⋅ b) ⊣⊢ (auth_own γ a ★ auth_own γ b).
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
- Lemma auth_own_valid γ a : auth_own γ a ⊑ ✓ a.
+ Lemma auth_own_valid γ a : auth_own γ a ⊢ ✓ a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc N E a :
✓ a → nclose N ⊆ E →
- ▷ φ a ⊑ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
+ ▷ φ a ⊢ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
Proof.
intros Ha HN. eapply sep_elim_True_r.
{ by eapply (own_alloc (Auth (Excl a) a) E). }
@@ -69,12 +69,12 @@ Section auth.
by rewrite always_and_sep_l.
Qed.
- Lemma auth_empty γ E : True ⊑ |={E}=> auth_own γ ∅.
+ Lemma auth_empty γ E : True ⊢ |={E}=> auth_own γ ∅.
Proof. by rewrite -own_empty. Qed.
Lemma auth_opened E γ a :
(▷ auth_inv γ φ ★ auth_own γ a)
- ⊑ (|={E}=> ∃ a', ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (◠(a ⋅ a') ⋅ ◯ a)).
+ ⊢ (|={E}=> ∃ a', ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (◠(a ⋅ a') ⋅ ◯ a)).
Proof.
rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
rewrite later_sep [(â–· own _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -93,7 +93,7 @@ Section auth.
Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
Lv a → ✓ (L a ⋅ a') →
(▷ φ (L a ⋅ a') ★ own γ (◠(a ⋅ a') ⋅ ◯ a))
- ⊑ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
+ ⊢ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
Proof.
intros HL Hv. rewrite /auth_inv -(exist_intro (L a â‹… a')).
(* TODO it would be really nice to use cancel here *)
@@ -108,13 +108,13 @@ Section auth.
Lemma auth_fsa E N P (Ψ : V → iPropG Λ Σ) γ a :
fsaV →
nclose N ⊆ E →
- P ⊑ auth_ctx γ N φ →
- P ⊑ (▷ auth_own γ a ★ ∀ a',
+ P ⊢ auth_ctx γ N φ →
+ P ⊢ (▷ auth_own γ a ★ ∀ a',
■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
fsa (E ∖ nclose N) (λ x, ∃ L Lv (Hup : LocalUpdate Lv L),
■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
(auth_own γ (L a) -★ Ψ x))) →
- P ⊑ fsa E Ψ.
+ P ⊢ fsa E Ψ.
Proof.
rewrite /auth_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
@@ -140,13 +140,13 @@ Section auth.
Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V → iPropG Λ Σ) γ a :
fsaV →
nclose N ⊆ E →
- P ⊑ auth_ctx γ N φ →
- P ⊑ (▷ auth_own γ a ★ (∀ a',
+ P ⊢ auth_ctx γ N φ →
+ P ⊢ (▷ auth_own γ a ★ (∀ a',
■✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') -★
fsa (E ∖ nclose N) (λ x,
■(Lv a ∧ ✓ (L a ⋅ a')) ★ ▷ φ (L a ⋅ a') ★
(auth_own γ (L a) -★ Ψ x)))) →
- P ⊑ fsa E Ψ.
+ P ⊢ fsa E Ψ.
Proof.
intros ??? HP. eapply auth_fsa with N γ a; eauto.
rewrite HP; apply sep_mono_r, forall_mono=> a'.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 380ba99397b92b67d747250a120b2f62dff6c38e..ba7f4e2ce0eaf0edbbd22aac8f2073966ed0da5f 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -30,17 +30,17 @@ Qed.
(** * Properties of own *)
Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
Proof. solve_proper. Qed.
-Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own γ) := ne_proper _.
+Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_proper _.
-Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ≡ (own γ a1 ★ own γ a2)%I.
+Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ (own γ a1 ★ own γ a2).
Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
-Global Instance own_mono γ : Proper (flip (≼) ==> (⊑)) (own γ).
+Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
-Lemma always_own_core γ a : (□ own γ (core a))%I ≡ own γ (core a).
+Lemma always_own_core γ a : (□ own γ (core a)) ⊣⊢ own γ (core a).
Proof. by rewrite /own -to_globalF_core always_ownG_core. Qed.
-Lemma always_own γ a : core a ≡ a → (□ own γ a)%I ≡ own γ a.
+Lemma always_own γ a : core a ≡ a → (□ own γ a) ⊣⊢ own γ a.
Proof. by intros <-; rewrite always_own_core. Qed.
-Lemma own_valid γ a : own γ a ⊑ ✓ a.
+Lemma own_valid γ a : own γ a ⊢ ✓ a.
Proof.
rewrite /own ownG_valid /to_globalF.
rewrite iprod_validI (forall_elim inG_id) iprod_lookup_singleton.
@@ -48,11 +48,11 @@ Proof.
(* implicit arguments differ a bit *)
by trans (✓ cmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf.
Qed.
-Lemma own_valid_r γ a : own γ a ⊑ (own γ a ★ ✓ a).
+Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ✓ a).
Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
-Lemma own_valid_l γ a : own γ a ⊑ (✓ a ★ own γ a).
+Lemma own_valid_l γ a : own γ a ⊢ (✓ a ★ own γ a).
Proof. by rewrite comm -own_valid_r. Qed.
-Lemma own_empty `{CMRAUnit A} γ : True ⊑ own γ ∅.
+Lemma own_empty `{CMRAUnit A} γ : True ⊢ own γ ∅.
Proof.
rewrite ownG_empty /own. apply equiv_spec, ownG_proper.
(* FIXME: rewrite to_globalF_empty. *)
@@ -65,7 +65,7 @@ Proof. by rewrite /AlwaysStable always_own_core. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a E (G : gset gname) :
- ✓ a → True ⊑ (|={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a).
+ ✓ a → True ⊢ (|={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a).
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■(∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
@@ -75,14 +75,14 @@ Proof.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
by rewrite -(exist_intro γ) const_equiv // left_id.
Qed.
-Lemma own_alloc a E : ✓ a → True ⊑ (|={E}=> ∃ γ, own γ a).
+Lemma own_alloc a E : ✓ a → True ⊢ (|={E}=> ∃ γ, own γ a).
Proof.
intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono.
apply exist_mono=>?. eauto with I.
Qed.
Lemma own_updateP P γ a E :
- a ~~>: P → own γ a ⊑ (|={E}=> ∃ a', ■P a' ∧ own γ a').
+ a ~~>: P → own γ a ⊢ (|={E}=> ∃ a', ■P a' ∧ own γ a').
Proof.
intros Ha.
rewrite -(pvs_mono _ _ (∃ m, ■(∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
@@ -93,14 +93,14 @@ Proof.
rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|].
Qed.
-Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ (|={E}=> own γ a').
+Lemma own_update γ a a' E : a ~~> a' → own γ a ⊢ (|={E}=> own γ a').
Proof.
intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->.
Qed.
Lemma own_empty `{Empty A, !CMRAUnit A} γ E :
- True ⊑ (|={E}=> own γ ∅).
+ True ⊢ (|={E}=> own γ ∅).
Proof.
rewrite ownG_empty /own. apply pvs_ownG_update, cmra_update_updateP.
eapply iprod_singleton_updateP_empty;
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index b89becfd19414838c96454f3d4490bb4a6335ad2..9f124b2d019f699a6744c56fb1e3233fa6a1de3d 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre viewshifts.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Φ : val Λ → iProp Λ Σ) : iProp Λ Σ :=
- (□ (P → #> e @ E {{ Φ }}))%I.
+ (□ (P → WP e @ E {{ Φ }}))%I.
Instance: Params (@ht) 3.
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
@@ -11,10 +11,10 @@ Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P e Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : uPred_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (True ⊑ ht E P e Φ)
+Notation "{{ P } } e @ E {{ Φ } }" := (True ⊢ ht E P e Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (True ⊑ ht ⊤ P e Φ)
+Notation "{{ P } } e {{ Φ } }" := (True ⊢ ht ⊤ P e Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : C_scope.
@@ -32,13 +32,13 @@ Global Instance ht_proper E :
Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (@ht Λ Σ E).
Proof. solve_proper. Qed.
Lemma ht_mono E P P' Φ Φ' e :
- P ⊑ P' → (∀ v, Φ' v ⊑ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊑ {{ P }} e @ E {{ Φ }}.
+ P ⊢ P' → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
Global Instance ht_mono' E :
- Proper (flip (⊑) ==> eq ==> pointwise_relation _ (⊑) ==> (⊑)) (@ht Λ Σ E).
+ Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (@ht Λ Σ E).
Proof. solve_proper. Qed.
-Lemma ht_alt E P Φ e : (P ⊑ #> e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
+Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
Proof.
intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
by rewrite always_const right_id.
@@ -50,7 +50,7 @@ Proof. apply ht_alt. by rewrite -wp_value'; apply const_intro. Qed.
Lemma ht_vs E P P' Φ Φ' e :
((P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ ∀ v, Φ' v ={E}=> Φ v)
- ⊑ {{ P }} e @ E {{ Φ }}.
+ ⊢ {{ P }} e @ E {{ Φ }}.
Proof.
apply: always_intro. apply impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
@@ -62,7 +62,7 @@ Qed.
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
E2 ⊆ E1 → atomic e →
((P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ ∀ v, Φ' v ={E2,E1}=> Φ v)
- ⊑ {{ P }} e @ E1 {{ Φ }}.
+ ⊢ {{ P }} e @ E1 {{ Φ }}.
Proof.
intros ??; apply: always_intro. apply impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
@@ -73,7 +73,7 @@ Qed.
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
({{ P }} e @ E {{ Φ }} ∧ ∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
- ⊑ {{ P }} K e @ E {{ Φ' }}.
+ ⊢ {{ P }} K e @ E {{ Φ' }}.
Proof.
intros; apply: always_intro. apply impl_intro_l.
rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
@@ -82,11 +82,11 @@ Proof.
Qed.
Lemma ht_mask_weaken E1 E2 P Φ e :
- E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊑ {{ P }} e @ E2 {{ Φ }}.
+ E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
Lemma ht_frame_l E P Φ R e :
- {{ P }} e @ E {{ Φ }} ⊑ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
+ {{ P }} e @ E {{ Φ }} ⊢ {{ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
Proof.
apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
@@ -94,12 +94,12 @@ Proof.
Qed.
Lemma ht_frame_r E P Φ R e :
- {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}.
+ {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ R }} e @ E {{ λ v, Φ v ★ R }}.
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_step_l E P R e Φ :
to_val e = None →
- {{ P }} e @ E {{ Φ }} ⊑ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
+ {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ★ P }} e @ E {{ λ v, R ★ Φ v }}.
Proof.
intros; apply always_intro', impl_intro_l.
rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
@@ -108,7 +108,7 @@ Qed.
Lemma ht_frame_step_r E P Φ R e :
to_val e = None →
- {{ P }} e @ E {{ Φ }} ⊑ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}.
+ {{ P }} e @ E {{ Φ }} ⊢ {{ P ★ ▷ R }} e @ E {{ λ v, Φ v ★ R }}.
Proof.
rewrite (comm _ _ (â–· R)%I); setoid_rewrite (comm _ _ R).
apply ht_frame_step_l.
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index a054226babfdbe12ba899396a4d8297e9e4313c3..7318ff8e960d159739fa33be49bfdd469ec1a64f 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -8,7 +8,7 @@ Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
(at level 20, P, ef, Φ at level 200,
format "{{ P } } ef ?@ E {{ Φ } }") : uPred_scope.
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
- (True ⊑ default True ef (λ e, ht E P e Φ))
+ (True ⊢ default True ef (λ e, ht E P e Φ))
(at level 20, P, ef, Φ at level 200,
format "{{ P } } ef ?@ E {{ Φ } }") : C_scope.
@@ -27,7 +27,7 @@ Lemma ht_lift_step E1 E2
(■φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧
{{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }} ∧
{{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ P }} e1 @ E1 {{ Ψ }}.
+ ⊢ {{ P }} e1 @ E1 {{ Ψ }}.
Proof.
intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
@@ -53,7 +53,7 @@ Lemma ht_lift_atomic_step
atomic e1 →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
- (∀ e2 σ2 ef, {{ ■φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ λ _, True }}) ⊑
+ (∀ e2 σ2 ef, {{ ■φ e2 σ2 ef ★ P }} ef ?@ ⊤ {{ λ _, True }}) ⊢
{{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■φ (of_val v) σ2 ef }}.
Proof.
intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
@@ -82,7 +82,7 @@ Lemma ht_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) P P' Ψ e
(∀ e2 ef,
{{ ■φ e2 ef ★ P }} e2 @ E {{ Ψ }} ∧
{{ ■φ e2 ef ★ P' }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
+ ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
rewrite -(wp_lift_pure_step E φ _ e1) //.
@@ -102,7 +102,7 @@ Lemma ht_lift_pure_det_step
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
({{ P }} e2 @ E {{ Ψ }} ∧ {{ P' }} ef ?@ ⊤ {{ λ _, True }})
- ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
+ ⊢ {{ ▷(P ★ P') }} e1 @ E {{ Ψ }}.
Proof.
intros ? Hsafe Hdet.
rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 86d68258839e438455cd3391eb8f8024295b62d3..2ea51465021ed0601caa9d3b8f937ae037528d08 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -26,15 +26,15 @@ Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Proof. rewrite /inv; apply _. Qed.
-Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
+Lemma always_inv N P : (□ inv N P) ⊣⊢ inv N P.
Proof. by rewrite always_always. Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
fsaV → nclose N ⊆ E →
- R ⊑ inv N P →
- R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
- R ⊑ fsa E Ψ.
+ R ⊢ inv N P →
+ R ⊢ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Ψ a)) →
+ R ⊢ fsa E Ψ.
Proof.
intros ? HN Hinv Hinner.
rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
@@ -56,19 +56,19 @@ Qed.
Lemma pvs_open_close E N P Q R :
nclose N ⊆ E →
- R ⊑ inv N P →
- R ⊑ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
- R ⊑ (|={E}=> Q).
+ R ⊢ inv N P →
+ R ⊢ (▷ P -★ |={E ∖ nclose N}=> (▷ P ★ Q)) →
+ R ⊢ (|={E}=> Q).
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
Lemma wp_open_close E e N P Φ R :
atomic e → nclose N ⊆ E →
- R ⊑ inv N P →
- R ⊑ (▷ P -★ #> e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
- R ⊑ #> e @ E {{ Φ }}.
+ R ⊢ inv N P →
+ R ⊢ (▷ P -★ WP e @ E ∖ nclose N {{ λ v, ▷ P ★ Φ v }}) →
+ R ⊢ WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
-Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊑ |={E}=> inv N P.
+Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊢ |={E}=> inv N P.
Proof.
intros. rewrite -(pvs_mask_weaken N) //.
by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 425c10f4e57968dedef5ffe48d36d39947cd6c99..e50e251368687daac2e76e2dafeefaed74d2be3d 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -23,8 +23,8 @@ Lemma wp_lift_step E1 E2
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
(|={E1,E2}=> ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef,
- (■φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> #> e2 @ E1 {{ Φ }} ★ wp_fork ef)
- ⊑ #> e1 @ E1 {{ Φ }}.
+ (■φ e2 σ2 ef ∧ ownP σ2) -★ |={E2,E1}=> WP e2 @ E1 {{ Φ }} ★ wp_fork ef)
+ ⊢ WP e1 @ E1 {{ Φ }}.
Proof.
intros ? He Hsafe Hstep. rewrite pvs_eq wp_eq.
uPred.unseal; split=> n r ? Hvs; constructor; auto.
@@ -45,7 +45,7 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
- (▷ ∀ e2 ef, ■φ e2 ef → #> e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ #> e1 @ E {{ Φ }}.
+ (▷ ∀ e2 ef, ■φ e2 ef → WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal.
split=> n r ? Hwp; constructor; auto.
@@ -67,7 +67,7 @@ Lemma wp_lift_atomic_step {E Φ} e1
(∀ e2 σ2 ef,
prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) →
(▷ ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■φ v2 σ2 ef ∧ ownP σ2 -★ Φ v2 ★ wp_fork ef)
- ⊑ #> e1 @ E {{ Φ }}.
+ ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2,
to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; [].
@@ -86,7 +86,7 @@ Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
reducible e1 σ1 →
(∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' →
σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') →
- (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊑ #> e1 @ E {{ Φ }}.
+ (▷ ownP σ1 ★ ▷ (ownP σ2 -★ Φ v2 ★ wp_fork ef)) ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef',
σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver.
@@ -101,7 +101,7 @@ Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
(∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
- ▷ (#> e2 @ E {{ Φ }} ★ wp_fork ef) ⊑ #> e1 @ E {{ Φ }}.
+ ▷ (WP e2 @ E {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}.
Proof.
intros.
rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index ec9813df808902e8b3fc41d6f02ee49733d5635a..c1ba7897fe2757ed95985daa229032d4447234de 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -25,18 +25,18 @@ Proof.
apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
by apply Next_contractive=> j ?; rewrite (HPQ j).
Qed.
-Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
+Lemma always_ownI i P : (□ ownI i P) ⊣⊢ ownI i P.
Proof.
apply uPred.always_ownM.
by rewrite Res_core !cmra_core_unit map_core_singleton.
Qed.
Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_ownI. Qed.
-Lemma ownI_sep_dup i P : ownI i P ≡ (ownI i P ★ ownI i P)%I.
+Lemma ownI_sep_dup i P : ownI i P ⊣⊢ (ownI i P ★ ownI i P).
Proof. apply (uPred.always_sep_dup _). Qed.
(* physical state *)
-Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊑ False.
+Lemma ownP_twice σ1 σ2 : (ownP σ1 ★ ownP σ2 : iProp Λ Σ) ⊢ False.
Proof.
rewrite /ownP -uPred.ownM_op Res_op.
by apply uPred.ownM_invalid; intros (_&?&_).
@@ -47,25 +47,25 @@ Proof. rewrite /ownP; apply _. Qed.
(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. solve_proper. Qed.
-Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
-Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ≡ (ownG m1 ★ ownG m2)%I.
+Global Instance ownG_proper : Proper ((≡) ==> (⊣⊢)) (@ownG Λ Σ) := ne_proper _.
+Lemma ownG_op m1 m2 : ownG (m1 ⋅ m2) ⊣⊢ (ownG m1 ★ ownG m2).
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
-Global Instance ownG_mono : Proper (flip (≼) ==> (⊑)) (@ownG Λ Σ).
+Global Instance ownG_mono : Proper (flip (≼) ==> (⊢)) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
-Lemma always_ownG_core m : (□ ownG (core m))%I ≡ ownG (core m).
+Lemma always_ownG_core m : (□ ownG (core m)) ⊣⊢ ownG (core m).
Proof.
apply uPred.always_ownM.
by rewrite Res_core !cmra_core_unit -{2}(cmra_core_idemp m).
Qed.
-Lemma always_ownG m : core m ≡ m → (□ ownG m)%I ≡ ownG m.
+Lemma always_ownG m : core m ≡ m → (□ ownG m) ⊣⊢ ownG m.
Proof. by intros <-; rewrite always_ownG_core. Qed.
-Lemma ownG_valid m : ownG m ⊑ ✓ m.
+Lemma ownG_valid m : ownG m ⊢ ✓ m.
Proof.
rewrite /ownG uPred.ownM_valid res_validI /=; auto with I.
Qed.
-Lemma ownG_valid_r m : ownG m ⊑ (ownG m ★ ✓ m).
+Lemma ownG_valid_r m : ownG m ⊢ (ownG m ★ ✓ m).
Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
-Lemma ownG_empty : True ⊑ (ownG ∅ : iProp Λ Σ).
+Lemma ownG_empty : True ⊢ (ownG ∅ : iProp Λ Σ).
Proof. apply uPred.ownM_empty. Qed.
Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index ed0900943c5768d852684bad25db9da3a2b8257c..803cd9962a130b48557d244a9e768e77a1573ec1 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -54,18 +54,18 @@ Qed.
Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
Proof. apply ne_proper, _. Qed.
-Lemma pvs_intro E P : P ⊑ |={E}=> P.
+Lemma pvs_intro E P : P ⊢ |={E}=> P.
Proof.
rewrite pvs_eq. split=> n r ? HP rf k Ef σ ???; exists r; split; last done.
apply uPred_weaken with n r; eauto.
Qed.
-Lemma pvs_mono E1 E2 P Q : P ⊑ Q → (|={E1,E2}=> P) ⊑ (|={E1,E2}=> Q).
+Lemma pvs_mono E1 E2 P Q : P ⊢ Q → (|={E1,E2}=> P) ⊢ (|={E1,E2}=> Q).
Proof.
rewrite pvs_eq. intros HPQ; split=> n r ? HP rf k Ef σ ???.
destruct (HP rf k Ef σ) as (r2&?&?); eauto.
exists r2; eauto using uPred_in_entails.
Qed.
-Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ (|={E}=> P).
+Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊢ (|={E}=> P).
Proof.
rewrite pvs_eq uPred.timelessP_spec=> HP.
uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
@@ -73,19 +73,19 @@ Proof.
apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
Qed.
Lemma pvs_trans E1 E2 E3 P :
- E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊑ (|={E1,E3}=> P).
+ E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊢ (|={E1,E3}=> P).
Proof.
rewrite pvs_eq. intros ?; split=> n r1 ? HP1 rf k Ef σ ???.
destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
- Ef ∩ (E1 ∪ E2) = ∅ → (|={E1,E2}=> P) ⊑ (|={E1 ∪ Ef,E2 ∪ Ef}=> P).
+ Ef ∩ (E1 ∪ E2) = ∅ → (|={E1,E2}=> P) ⊢ (|={E1 ∪ Ef,E2 ∪ Ef}=> P).
Proof.
rewrite pvs_eq. intros ?; split=> n r ? HP rf k Ef' σ ???.
destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto.
by exists r'; rewrite -(assoc_L _).
Qed.
-Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊑ (|={E1,E2}=> P ★ Q).
+Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊢ (|={E1,E2}=> P ★ Q).
Proof.
rewrite pvs_eq. uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
@@ -93,7 +93,7 @@ Proof.
exists (r' â‹… r2); split; last by rewrite -assoc.
exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
Qed.
-Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
+Lemma pvs_openI i P : ownI i P ⊢ (|={{[i]},∅}=> ▷ P).
Proof.
rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
apply ownI_spec in Hinv; last auto.
@@ -102,7 +102,7 @@ Proof.
exists (rP â‹… r); split; last by rewrite (left_id_L _ _) -assoc.
eapply uPred_weaken with (S k) rP; eauto using cmra_included_l.
Qed.
-Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ (|={∅,{[i]}}=> True).
+Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊢ (|={∅,{[i]}}=> True).
Proof.
rewrite pvs_eq. uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
exists ∅; split; [done|].
@@ -113,7 +113,7 @@ Proof.
- apply uPred_weaken with n r; auto.
Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
- m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■P m' ∧ ownG m').
+ m ~~>: P → ownG m ⊢ (|={E}=> ∃ m', ■P m' ∧ ownG m').
Proof.
rewrite pvs_eq. intros Hup.
uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
@@ -121,7 +121,7 @@ Proof.
{ apply cmra_includedN_le with (S n); auto. }
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
-Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■(i ∈ E) ∧ ownI i P).
+Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊢ (|={E}=> ∃ i, ■(i ∈ E) ∧ ownI i P).
Proof.
rewrite pvs_eq. intros ?; rewrite /ownI; uPred.unseal.
split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
@@ -133,40 +133,40 @@ Qed.
(** * Derived rules *)
Import uPred.
-Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
+Global Instance pvs_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
Global Instance pvs_flip_mono' E1 E2 :
- Proper (flip (⊑) ==> flip (⊑)) (@pvs Λ Σ E1 E2).
+ Proper (flip (⊢) ==> flip (⊢)) (@pvs Λ Σ E1 E2).
Proof. intros P Q; apply pvs_mono. Qed.
-Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ⊑ (|={E}=> P).
+Lemma pvs_trans' E P : (|={E}=> |={E}=> P) ⊢ (|={E}=> P).
Proof. apply pvs_trans; set_solver. Qed.
-Lemma pvs_strip_pvs E P Q : P ⊑ (|={E}=> Q) → (|={E}=> P) ⊑ (|={E}=> Q).
+Lemma pvs_strip_pvs E P Q : P ⊢ (|={E}=> Q) → (|={E}=> P) ⊢ (|={E}=> Q).
Proof. move=>->. by rewrite pvs_trans'. Qed.
-Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊑ (|={E1,E2}=> P ★ Q).
+Lemma pvs_frame_l E1 E2 P Q : (P ★ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ★ Q).
Proof. rewrite !(comm _ P); apply pvs_frame_r. Qed.
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
- (P ∧ |={E1,E2}=> Q) ⊑ (|={E1,E2}=> P ∧ Q).
+ (P ∧ |={E1,E2}=> Q) ⊢ (|={E1,E2}=> P ∧ Q).
Proof. by rewrite !always_and_sep_l pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
- ((|={E1,E2}=> P) ∧ Q) ⊑ (|={E1,E2}=> P ∧ Q).
+ ((|={E1,E2}=> P) ∧ Q) ⊢ (|={E1,E2}=> P ∧ Q).
Proof. by rewrite !always_and_sep_r pvs_frame_r. Qed.
-Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊑ (|={E1,E2}=> Q).
+Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ (|={E1,E2}=> P)) ⊢ (|={E1,E2}=> Q).
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
-Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P) ∧ □ (P → Q)) ⊑ (|={E1,E2}=> Q).
+Lemma pvs_impl_r E1 E2 P Q : ((|={E1,E2}=> P) ∧ □ (P → Q)) ⊢ (|={E1,E2}=> Q).
Proof. by rewrite comm pvs_impl_l. Qed.
Lemma pvs_wand_l E1 E2 P Q R :
- P ⊑ (|={E1,E2}=> Q) → ((Q -★ R) ★ P) ⊑ (|={E1,E2}=> R).
+ P ⊢ (|={E1,E2}=> Q) → ((Q -★ R) ★ P) ⊢ (|={E1,E2}=> R).
Proof. intros ->. rewrite pvs_frame_l. apply pvs_mono, wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q R :
- P ⊑ (|={E1,E2}=> Q) → (P ★ (Q -★ R)) ⊑ (|={E1,E2}=> R).
+ P ⊢ (|={E1,E2}=> Q) → (P ★ (Q -★ R)) ⊢ (|={E1,E2}=> R).
Proof. rewrite comm. apply pvs_wand_l. Qed.
Lemma pvs_sep E P Q:
- ((|={E}=> P) ★ (|={E}=> Q)) ⊑ (|={E}=> P ★ Q).
+ ((|={E}=> P) ★ (|={E}=> Q)) ⊢ (|={E}=> P ★ Q).
Proof. rewrite pvs_frame_r pvs_frame_l pvs_trans //. set_solver. Qed.
Lemma pvs_mask_frame' E1 E1' E2 E2' P :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
- (|={E1',E2'}=> P) ⊑ (|={E1,E2}=> P).
+ (|={E1',E2'}=> P) ⊢ (|={E1,E2}=> P).
Proof.
intros HE1 HE2 HEE.
rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
@@ -175,7 +175,7 @@ Qed.
Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
- P ⊑ Q → (|={E1',E2'}=> P) ⊑ (|={E1,E2}=> Q).
+ P ⊢ Q → (|={E1',E2'}=> P) ⊢ (|={E1,E2}=> Q).
Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
(** It should be possible to give a stronger version of this rule
@@ -184,13 +184,13 @@ Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
mask becomes really ugly then, and we have not found an instance
where that would be useful. *)
Lemma pvs_trans3 E1 E2 Q :
- E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ⊑ (|={E1}=> Q).
+ E2 ⊆ E1 → (|={E1,E2}=> |={E2}=> |={E2,E1}=> Q) ⊢ (|={E1}=> Q).
Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
-Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊑ (|={E2}=> P).
+Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊢ (|={E2}=> P).
Proof. auto using pvs_mask_frame'. Qed.
-Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ (|={E}=> ownG m').
+Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊢ (|={E}=> ownG m').
Proof.
intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
@@ -205,29 +205,29 @@ End pvs.
Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
fsa_mask_frame_mono E1 E2 Φ Ψ :
- E1 ⊆ E2 → (∀ a, Φ a ⊑ Ψ a) → fsa E1 Φ ⊑ fsa E2 Ψ;
- fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊑ fsa E Φ;
+ E1 ⊆ E2 → (∀ a, Φ a ⊢ Ψ a) → fsa E1 Φ ⊢ fsa E2 Ψ;
+ fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊢ fsa E Φ;
fsa_open_close E1 E2 Φ :
- fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊑ fsa E1 Φ;
- fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊑ fsa E (λ a, Φ a ★ P)
+ fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊢ fsa E1 Φ;
+ fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊢ fsa E (λ a, Φ a ★ P)
}.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
Implicit Types Φ Ψ : A → iProp Λ Σ.
-Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊑ Ψ a) → fsa E Φ ⊑ fsa E Ψ.
+Lemma fsa_mono E Φ Ψ : (∀ a, Φ a ⊢ Ψ a) → fsa E Φ ⊢ fsa E Ψ.
Proof. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊑ fsa E2 Φ.
+Lemma fsa_mask_weaken E1 E2 Φ : E1 ⊆ E2 → fsa E1 Φ ⊢ fsa E2 Φ.
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
-Lemma fsa_frame_l E P Φ : (P ★ fsa E Φ) ⊑ fsa E (λ a, P ★ Φ a).
+Lemma fsa_frame_l E P Φ : (P ★ fsa E Φ) ⊢ fsa E (λ a, P ★ Φ a).
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
-Lemma fsa_strip_pvs E P Φ : P ⊑ fsa E Φ → (|={E}=> P) ⊑ fsa E Φ.
+Lemma fsa_strip_pvs E P Φ : P ⊢ fsa E Φ → (|={E}=> P) ⊢ fsa E Φ.
Proof.
move=>->. rewrite -{2}fsa_trans3.
apply pvs_mono, fsa_mono=>a; apply pvs_intro.
Qed.
-Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊑ (|={E}=> Ψ a)) → fsa E Φ ⊑ fsa E Ψ.
+Lemma fsa_mono_pvs E Φ Ψ : (∀ a, Φ a ⊢ (|={E}=> Ψ a)) → fsa E Φ ⊢ fsa E Ψ.
Proof. intros. rewrite -[fsa E Ψ]fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
End fsa.
@@ -239,6 +239,6 @@ Proof.
Qed.
Lemma pvs_mk_fsa {Λ Σ} E (P Q : iProp Λ Σ) :
- P ⊑ pvs_fsa E (λ _, Q) →
- P ⊑ |={E}=> Q.
+ P ⊢ pvs_fsa E (λ _, Q) →
+ P ⊢ |={E}=> Q.
Proof. by intros ?. Qed.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index f96c02db68f32f68e1c720259214cc876f1922e9..e95aef904878a0b4693d4e19cdde568e0526d8b8 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -156,12 +156,12 @@ Proof. by intros ? ? [???]; constructor; apply: timeless. Qed.
(** Internalized properties *)
Lemma res_equivI {M'} r1 r2 :
- (r1 ≡ r2)%I
- ≡ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M')%I.
+ (r1 ≡ r2)
+ ⊣⊢ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2: uPred M').
Proof.
uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
Qed.
-Lemma res_validI {M'} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M')%I.
+Lemma res_validI {M'} r : (✓ r) ⊣⊢ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M').
Proof. by uPred.unseal. Qed.
End res.
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 22cecf668e26fb65ce41d9f7ba6b86de1448b500..e4c247046d96cb02816efb17aafe1e47ff2a7c8b 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -25,14 +25,14 @@ Section saved_prop.
Proof. by rewrite /AlwaysStable always_own. Qed.
Lemma saved_prop_alloc_strong N x (G : gset gname) :
- True ⊑ pvs N N (∃ γ, ■(γ ∉ G) ∧ saved_prop_own γ x).
+ True ⊢ pvs N N (∃ γ, ■(γ ∉ G) ∧ saved_prop_own γ x).
Proof. by apply own_alloc_strong. Qed.
- Lemma saved_prop_alloc N x : True ⊑ pvs N N (∃ γ, saved_prop_own γ x).
+ Lemma saved_prop_alloc N x : True ⊢ pvs N N (∃ γ, saved_prop_own γ x).
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y :
- (saved_prop_own γ x ★ saved_prop_own γ y) ⊑ ▷(x ≡ y).
+ (saved_prop_own γ x ★ saved_prop_own γ y) ⊢ ▷(x ≡ y).
Proof.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 76a00f4228c2c1968cef2e97bc762893f63ac2e6..f03b5cbb23ef8cc9ccb0864c3be102184e3e8be6 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -32,15 +32,15 @@ Section definitions.
Global Instance sts_inv_proper :
Proper (pointwise_relation _ (≡) ==> (≡)) sts_inv.
Proof. solve_proper. Qed.
- Global Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (≡)) sts_ownS.
+ Global Instance sts_ownS_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) sts_ownS.
Proof. solve_proper. Qed.
- Global Instance sts_own_proper s : Proper ((≡) ==> (≡)) (sts_own s).
+ Global Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s).
Proof. solve_proper. Qed.
Global Instance sts_ctx_ne n N :
Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_proper N :
- Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx N).
+ Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_always_stable N φ : AlwaysStable (sts_ctx N φ).
Proof. apply _. Qed.
@@ -63,22 +63,22 @@ Section sts.
sts_frag_included. *)
Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
- sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2).
+ sts_ownS γ S1 T1 ⊢ (|={E}=> sts_ownS γ S2 T2).
Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
Lemma sts_own_weaken E γ s S T1 T2 :
T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
- sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2).
+ sts_own γ s T1 ⊢ (|={E}=> sts_ownS γ S T2).
Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
Lemma sts_ownS_op γ S1 S2 T1 T2 :
T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
- sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
+ sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2).
Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Lemma sts_alloc E N s :
nclose N ⊆ E →
- ▷ φ s ⊑ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
+ ▷ φ s ⊢ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
Proof.
intros HN. eapply sep_elim_True_r.
{ apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) E).
@@ -95,7 +95,7 @@ Section sts.
Lemma sts_opened E γ S T :
(▷ sts_inv γ φ ★ sts_ownS γ S T)
- ⊑ (|={E}=> ∃ s, ■(s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
+ ⊢ (|={E}=> ∃ s, ■(s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
Proof.
rewrite /sts_inv later_exist sep_exist_r. apply exist_elim=>s.
rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
@@ -109,7 +109,7 @@ Section sts.
Lemma sts_closing E γ s T s' T' :
sts.steps (s, T) (s', T') →
- (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
+ (▷ φ s' ★ own γ (sts_auth s T)) ⊢ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T').
Proof.
intros Hstep. rewrite /sts_inv -(exist_intro s') later_sep.
(* TODO it would be really nice to use cancel here *)
@@ -125,13 +125,13 @@ Section sts.
Lemma sts_fsaS E N P (Ψ : V → iPropG Λ Σ) γ S T :
fsaV → nclose N ⊆ E →
- P ⊑ sts_ctx γ N φ →
- P ⊑ (sts_ownS γ S T ★ ∀ s,
+ P ⊢ sts_ctx γ N φ →
+ P ⊢ (sts_ownS γ S T ★ ∀ s,
■(s ∈ S) ★ ▷ φ s -★
fsa (E ∖ nclose N) (λ x, ∃ s' T',
■sts.steps (s, T) (s', T') ★ ▷ φ s' ★
(sts_own γ s' T' -★ Ψ x))) →
- P ⊑ fsa E Ψ.
+ P ⊢ fsa E Ψ.
Proof.
rewrite /sts_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
@@ -154,12 +154,12 @@ Section sts.
Lemma sts_fsa E N P (Ψ : V → iPropG Λ Σ) γ s0 T :
fsaV → nclose N ⊆ E →
- P ⊑ sts_ctx γ N φ →
- P ⊑ (sts_own γ s0 T ★ ∀ s,
+ P ⊢ sts_ctx γ N φ →
+ P ⊢ (sts_own γ s0 T ★ ∀ s,
■(s ∈ sts.up s0 T) ★ ▷ φ s -★
fsa (E ∖ nclose N) (λ x, ∃ s' T',
■(sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
(sts_own γ s' T' -★ Ψ x))) →
- P ⊑ fsa E Ψ.
+ P ⊢ fsa E Ψ.
Proof. by apply sts_fsaS. Qed.
End sts.
diff --git a/program_logic/tactics.v b/program_logic/tactics.v
index 2ac6a67cd56086e44958c84e785001a7a34f80a4..d155bdc349eb43b342723aa4c518f9519e9591d7 100644
--- a/program_logic/tactics.v
+++ b/program_logic/tactics.v
@@ -11,7 +11,7 @@ Module uPred_reflection_pvs.
Lemma cancel_entails_pvs Σ' E1 E2 e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
- eval Σ' e1' ⊑ pvs E1 E2 (eval Σ' e2' : iProp) → eval Σ' e1 ⊑ pvs E1 E2 (eval Σ' e2).
+ eval Σ' e1' ⊢ pvs E1 E2 (eval Σ' e2' : iProp) → eval Σ' e1 ⊢ pvs E1 E2 (eval Σ' e2).
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
@@ -22,16 +22,16 @@ Module uPred_reflection_pvs.
Ltac quote_pvs :=
match goal with
- | |- ?P1 ⊑ pvs ?E1 ?E2 ?P2 =>
+ | |- ?P1 ⊢ pvs ?E1 ?E2 ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
- change (eval Σ3 e1 ⊑ pvs E1 E2 (eval Σ3 e2)) end end
+ change (eval Σ3 e1 ⊢ pvs E1 E2 (eval Σ3 e2)) end end
end.
End uPred_reflection_pvs.
Tactic Notation "cancel_pvs" constr(Ps) :=
uPred_reflection_pvs.quote_pvs;
- let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
+ let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 4ac9228ac0f103a49f1a785d0a4d4bc679c100e2..639e34a687e4c5156d5f60287be5aa060f9e9c2f 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -9,12 +9,12 @@ Instance: Params (@vs) 4.
Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P%I Q%I)
(at level 199, E1,E2 at level 50,
format "P ={ E1 , E2 }=> Q") : uPred_scope.
-Notation "P ={ E1 , E2 }=> Q" := (True ⊑ vs E1 E2 P%I Q%I)
+Notation "P ={ E1 , E2 }=> Q" := (True ⊢ vs E1 E2 P%I Q%I)
(at level 199, E1, E2 at level 50,
format "P ={ E1 , E2 }=> Q") : C_scope.
Notation "P ={ E }=> Q" := (vs E E P%I Q%I)
(at level 199, E at level 50, format "P ={ E }=> Q") : uPred_scope.
-Notation "P ={ E }=> Q" := (True ⊑ vs E E P%I Q%I)
+Notation "P ={ E }=> Q" := (True ⊢ vs E E P%I Q%I)
(at level 199, E at level 50, format "P ={ E }=> Q") : C_scope.
Section vs.
@@ -22,7 +22,7 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q R : iProp Λ Σ.
Implicit Types N : namespace.
-Lemma vs_alt E1 E2 P Q : P ⊑ (|={E1,E2}=> Q) → P ={E1,E2}=> Q.
+Lemma vs_alt E1 E2 P Q : P ⊢ (|={E1,E2}=> Q) → P ={E1,E2}=> Q.
Proof.
intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
by rewrite always_const right_id.
@@ -36,11 +36,11 @@ Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (@vs Λ Σ
Proof. apply ne_proper_2, _. Qed.
Lemma vs_mono E1 E2 P P' Q Q' :
- P ⊑ P' → Q' ⊑ Q → (P' ={E1,E2}=> Q') ⊑ (P ={E1,E2}=> Q).
+ P ⊢ P' → Q' ⊢ Q → (P' ={E1,E2}=> Q') ⊢ (P ={E1,E2}=> Q).
Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
Global Instance vs_mono' E1 E2 :
- Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@vs Λ Σ E1 E2).
+ Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@vs Λ Σ E1 E2).
Proof. solve_proper. Qed.
Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
@@ -49,47 +49,47 @@ Lemma vs_timeless E P : TimelessP P → ▷ P ={E}=> P.
Proof. by intros ?; apply vs_alt, pvs_timeless. Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
- E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊑ (P ={E1,E3}=> R).
+ E2 ⊆ E1 ∪ E3 → ((P ={E1,E2}=> Q) ∧ (Q ={E2,E3}=> R)) ⊢ (P ={E1,E3}=> R).
Proof.
intros; rewrite -always_and; apply: always_intro. apply impl_intro_l.
rewrite always_and assoc (always_elim (P → _)) impl_elim_r.
by rewrite pvs_impl_r; apply pvs_trans.
Qed.
-Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊑ (P ={E}=> R).
+Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊢ (P ={E}=> R).
Proof. apply vs_transitive; set_solver. Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Proof. apply vs_alt, pvs_intro. Qed.
-Lemma vs_impl E P Q : □ (P → Q) ⊑ (P ={E}=> Q).
+Lemma vs_impl E P Q : □ (P → Q) ⊢ (P ={E}=> Q).
Proof.
apply always_intro', impl_intro_l.
by rewrite always_elim impl_elim_r -pvs_intro.
Qed.
-Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊑ (R ★ P ={E1,E2}=> R ★ Q).
+Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (R ★ P ={E1,E2}=> R ★ Q).
Proof.
apply always_intro', impl_intro_l.
rewrite -pvs_frame_l always_and_sep_r -always_wand_impl -assoc.
by rewrite always_elim wand_elim_r.
Qed.
-Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊑ (P ★ R ={E1,E2}=> Q ★ R).
+Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (P ★ R ={E1,E2}=> Q ★ R).
Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed.
Lemma vs_mask_frame E1 E2 Ef P Q :
- Ef ∩ (E1 ∪ E2) = ∅ → (P ={E1,E2}=> Q) ⊑ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
+ Ef ∩ (E1 ∪ E2) = ∅ → (P ={E1,E2}=> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q).
Proof.
intros ?; apply always_intro', impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//.
by rewrite always_elim impl_elim_r.
Qed.
-Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊑ (P ={E ∪ Ef}=> Q).
+Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q).
Proof. intros; apply vs_mask_frame; set_solver. Qed.
Lemma vs_open_close N E P Q R :
nclose N ⊆ E →
- (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊑ (P ={E}=> Q).
+ (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q).
Proof.
intros; apply: always_intro. apply impl_intro_l.
rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index a0244cdb48d7bb7da99ec1930df723444fc5a493..f19cd66df0425c5a1b585f62dc9d581bdba70e2a 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -57,13 +57,12 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
Arguments wp {_ _} _ _ _.
Instance: Params (@wp) 4.
-(* TODO: On paper, 'wp' is turned into a keyword. *)
-Notation "#> e @ E {{ Φ } }" := (wp E e Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
(at level 20, e, Φ at level 200,
- format "#> e @ E {{ Φ } }") : uPred_scope.
-Notation "#> e {{ Φ } }" := (wp ⊤ e Φ)
+ format "'WP' e @ E {{ Φ } }") : uPred_scope.
+Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
(at level 20, e, Φ at level 200,
- format "#> e {{ Φ } }") : uPred_scope.
+ format "'WP' e {{ Φ } }") : uPred_scope.
Section wp.
Context {Λ : language} {Σ : iFunctor}.
@@ -94,7 +93,7 @@ Proof.
by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
- E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → #> e @ E1 {{ Φ }} ⊑ #> e @ E2 {{ Ψ }}.
+ E1 ⊆ E2 → (∀ v, Φ v ⊢ Ψ v) → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
Proof.
rewrite wp_eq. intros HE HΦ; split=> n r.
revert e r; induction n as [n IH] using lt_wf_ind=> e r.
@@ -122,9 +121,9 @@ Proof.
intros He; destruct 3; [by rewrite ?to_of_val in He|eauto].
Qed.
-Lemma wp_value' E Φ v : Φ v ⊑ #> of_val v @ E {{ Φ }}.
+Lemma wp_value' E Φ v : Φ v ⊢ WP of_val v @ E {{ Φ }}.
Proof. rewrite wp_eq. split=> n r; constructor; by apply pvs_intro. Qed.
-Lemma pvs_wp E e Φ : (|={E}=> #> e @ E {{ Φ }}) ⊑ #> e @ E {{ Φ }}.
+Lemma pvs_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split=> n r ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
@@ -134,7 +133,7 @@ Proof.
rewrite pvs_eq in Hvs. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
eapply wp_step_inv with (S k) r'; eauto.
Qed.
-Lemma wp_pvs E e Φ : #> e @ E {{ λ v, |={E}=> Φ v }} ⊑ #> e @ E {{ Φ }}.
+Lemma wp_pvs E e Φ : WP e @ E {{ λ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split=> n r; revert e r;
induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
@@ -148,7 +147,7 @@ Proof.
Qed.
Lemma wp_atomic E1 E2 e Φ :
E2 ⊆ E1 → atomic e →
- (|={E1,E2}=> #> e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ #> e @ E1 {{ Φ }}.
+ (|={E1,E2}=> WP e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
Proof.
rewrite wp_eq pvs_eq. intros ? He; split=> n r ? Hvs; constructor.
eauto using atomic_not_val. intros rf k Ef σ1 ???.
@@ -165,7 +164,7 @@ Proof.
- by rewrite -assoc.
- constructor; apply pvs_intro; auto.
Qed.
-Lemma wp_frame_r E e Φ R : (#> e @ E {{ Φ }} ★ R) ⊑ #> e @ E {{ λ v, Φ v ★ R }}.
+Lemma wp_frame_r E e Φ R : (WP e @ E {{ Φ }} ★ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}.
Proof.
rewrite wp_eq. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
revert Hvalid. rewrite Hr; clear Hr; revert e r Hwp.
@@ -184,7 +183,7 @@ Proof.
- apply IH; eauto using uPred_weaken.
Qed.
Lemma wp_frame_step_r E e Φ R :
- to_val e = None → (#> e @ E {{ Φ }} ★ ▷ R) ⊑ #> e @ E {{ λ v, Φ v ★ R }}.
+ to_val e = None → (WP e @ E {{ Φ }} ★ ▷ R) ⊢ WP e @ E {{ λ v, Φ v ★ R }}.
Proof.
rewrite wp_eq. intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
revert Hvalid; rewrite Hr; clear Hr.
@@ -200,7 +199,7 @@ Proof.
eapply uPred_weaken with n rR; eauto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
- #> e @ E {{ λ v, #> K (of_val v) @ E {{ Φ }} }} ⊑ #> K e @ E {{ Φ }}.
+ WP e @ E {{ λ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
Proof.
rewrite wp_eq. split=> n r; revert e r;
induction n as [n IH] using lt_wf_ind=> e r ?.
@@ -219,44 +218,44 @@ Qed.
(** * Derived rules *)
Import uPred.
-Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊑ Ψ v) → #> e @ E {{ Φ }} ⊑ #> e @ E {{ Ψ }}.
+Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
Proof. by apply wp_mask_frame_mono. Qed.
Global Instance wp_mono' E e :
- Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e).
+ Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ E e).
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
Lemma wp_strip_pvs E e P Φ :
- P ⊑ #> e @ E {{ Φ }} → (|={E}=> P) ⊑ #> e @ E {{ Φ }}.
+ P ⊢ WP e @ E {{ Φ }} → (|={E}=> P) ⊢ WP e @ E {{ Φ }}.
Proof. move=>->. by rewrite pvs_wp. Qed.
-Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ #> e @ E {{ Φ }}.
+Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊢ WP e @ E {{ Φ }}.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
Lemma wp_value_pvs E Φ e v :
- to_val e = Some v → (|={E}=> Φ v) ⊑ #> e @ E {{ Φ }}.
+ to_val e = Some v → (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
-Lemma wp_frame_l E e Φ R : (R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}.
+Lemma wp_frame_l E e Φ R : (R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}.
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Lemma wp_frame_step_l E e Φ R :
- to_val e = None → (▷ R ★ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ★ Φ v }}.
+ to_val e = None → (▷ R ★ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ★ Φ v }}.
Proof.
rewrite (comm _ (â–· R)%I); setoid_rewrite (comm _ R).
apply wp_frame_step_r.
Qed.
Lemma wp_always_l E e Φ R `{!AlwaysStable R} :
- (R ∧ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ λ v, R ∧ Φ v }}.
+ (R ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ λ v, R ∧ Φ v }}.
Proof. by setoid_rewrite (always_and_sep_l _ _); rewrite wp_frame_l. Qed.
Lemma wp_always_r E e Φ R `{!AlwaysStable R} :
- (#> e @ E {{ Φ }} ∧ R) ⊑ #> e @ E {{ λ v, Φ v ∧ R }}.
+ (WP e @ E {{ Φ }} ∧ R) ⊢ WP e @ E {{ λ v, Φ v ∧ R }}.
Proof. by setoid_rewrite (always_and_sep_r _ _); rewrite wp_frame_r. Qed.
Lemma wp_impl_l E e Φ Ψ :
- ((□ ∀ v, Φ v → Ψ v) ∧ #> e @ E {{ Φ }}) ⊑ #> e @ E {{ Ψ }}.
+ ((□ ∀ v, Φ v → Ψ v) ∧ WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Ψ }}.
Proof.
rewrite wp_always_l; apply wp_mono=> // v.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Φ Ψ :
- (#> e @ E {{ Φ }} ∧ □ (∀ v, Φ v → Ψ v)) ⊑ #> e @ E {{ Ψ }}.
+ (WP e @ E {{ Φ }} ∧ □ (∀ v, Φ v → Ψ v)) ⊢ WP e @ E {{ Ψ }}.
Proof. by rewrite comm wp_impl_l. Qed.
Lemma wp_mask_weaken E1 E2 e Φ :
- E1 ⊆ E2 → #> e @ E1 {{ Φ }} ⊑ #> e @ E2 {{ Φ }}.
+ E1 ⊆ E2 → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Φ }}.
Proof. auto using wp_mask_frame_mono. Qed.
(** * Weakest-pre is a FSA. *)