Skip to content

GitLab

Commit 2d9c5f33 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Seal off all definitions in uPred. 

The performance gain seems neglectable, unfortunatelly...
parent 52d7d275
Hide whitespace changes
Inline Side-by-side
Showing with 244 additions and 142 deletions
algebra/agree.v
View file @ 2d9c5f33
......@@ -134,9 +134,11 @@ 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.
Proof. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
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).
Proof. split=> r n _ ?; by apply: agree_op_inv. Qed.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
End agree.
Arguments agreeC : clear implicits.
......
algebra/auth.v
View file @ 2d9c5f33
......@@ -151,14 +151,14 @@ Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
Proof. done. Qed.
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
(✓ x)%I ≡ (match authoritative x with
| Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
| ExclUnit => ✓ own x
| ExclBot => False
end : uPred M)%I.
Proof. by destruct x as [[]]. Qed.
Proof. uPred.unseal. by destruct x as [[]]. Qed.
(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
what follows, we assume we have an empty element. *)
......
algebra/excl.v
View file @ 2d9c5f33
......@@ -146,10 +146,12 @@ Lemma excl_equivI {M} (x y : excl A) :
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| _, _ => False
end : uPred M)%I.
Proof. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed.
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.
Proof. by destruct x. Qed.
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
Global Instance excl_local_update b :
......
algebra/fin_maps.v
View file @ 2d9c5f33
......@@ -171,9 +171,9 @@ 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.
Proof. done. Qed.
Proof. by uPred.unseal. Qed.
Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
Proof. done. Qed.
Proof. by uPred.unseal. Qed.
End cmra.
Arguments mapRA _ {_ _} _.
......
algebra/iprod.v
View file @ 2d9c5f33
......@@ -171,9 +171,9 @@ Section iprod_cmra.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
Proof. done. Qed.
Proof. by uPred.unseal. Qed.
Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
Proof. done. Qed.
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
Context `{∀ x x' : A, Decision (x = x')}.
......
algebra/option.v
View file @ 2d9c5f33
......@@ -140,10 +140,12 @@ Lemma option_equivI {M} (x y : option A) :
(x ≡ y)%I ≡ (match x, y with
| Some a, Some b => a ≡ b | None, None => True | _, _ => False
end : uPred M)%I.
Proof. do 2 split. by destruct 1. by destruct x, y; try constructor. Qed.
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.
Proof. by destruct x. Qed.
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
......
algebra/upred.v
View file @ 2d9c5f33
......@@ -106,18 +106,31 @@ Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
(** logical connectives *)
Program Definition uPred_const {M} (φ : Prop) : uPred M :=
Program Definition uPred_const_def {M} (φ : Prop) : uPred M :=
{| uPred_holds n x := φ |}.
Solve Obligations with done.
Definition uPred_const_aux : { x | x = @uPred_const_def }. by eexists. Qed.
Definition uPred_const {M} := proj1_sig uPred_const_aux M.
Definition uPred_const_eq :
@uPred_const = @uPred_const_def := proj2_sig uPred_const_aux.
Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∧ Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
Definition uPred_and {M} := proj1_sig uPred_and_aux M.
Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.
Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x ∨ Q n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
Definition uPred_or {M} := proj1_sig uPred_or_aux M.
Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.
Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
Next Obligation.
......@@ -128,19 +141,34 @@ Next Obligation.
eauto using uPred_weaken, uPred_ne.
Qed.
Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
Definition uPred_impl_eq :
@uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
Program Definition uPred_forall {M A} (Ψ : A → uPred M) : uPred M :=
Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := ∀ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Program Definition uPred_exist {M A} (Ψ : A → uPred M) : uPred M :=
Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
Definition uPred_forall_eq :
@uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.
Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
{| uPred_holds n x := ∃ a, Ψ a n x |}.
Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ≡{n}≡ a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
Next Obligation.
by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
......@@ -154,8 +182,11 @@ Next Obligation.
- apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
- apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
Qed.
Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := ∀ n' x',
n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
Next Obligation.
......@@ -168,31 +199,53 @@ Next Obligation.
apply uPred_weaken with n3 (x1 ⋅ x3);
eauto using cmra_validN_included, cmra_preserving_r.
Qed.
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
Definition uPred_wand_eq :
@uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
Program Definition uPred_always {M} (P : uPred M) : uPred M :=
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (unit x) |}.
Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
Next Obligation.
intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
eauto using cmra_unit_preserving, cmra_unit_validN.
Qed.
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
Definition uPred_always {M} := proj1_sig uPred_always_aux M.
Definition uPred_always_eq :
@uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.
Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed.
Next Obligation.
intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
Qed.
Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
Definition uPred_later {M} := proj1_sig uPred_later_aux M.
Definition uPred_later_eq :
@uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
Program Definition uPred_ownM_def {M : cmraT} (a : M) : uPred M :=
{| uPred_holds n x := a ≼{n} x |}.
Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
Next Obligation.
intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
exists (a' ⋅ x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
Qed.
Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
Definition uPred_ownM_eq :
@uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
Program Definition uPred_valid_def {M A : cmraT} (a : A) : uPred M :=
{| uPred_holds n x := ✓{n} a |}.
Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
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.
......@@ -229,7 +282,14 @@ Arguments timelessP {_} _ {_}.
Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
Arguments always_stable {_} _ {_}.
Module uPred. Section uPred_logic.
Module uPred.
Definition unseal :=
(uPred_const_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
uPred_later_eq, uPred_ownM_eq, uPred_valid_eq).
Ltac unseal := rewrite !unseal.
Section uPred_logic.
Context {M : cmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
......@@ -265,10 +325,10 @@ Qed.
(** Non-expansiveness and setoid morphisms *)
Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
Proof. intros φ1 φ2 Hφ. by split=> -[|n] ?; try apply Hφ. Qed.
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.
intros P P' HP Q Q' HQ; split=> x n' ??.
intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
Global Instance and_proper :
......@@ -276,7 +336,7 @@ Global Instance and_proper :
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' ??.
split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
Global Instance or_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_or M) := ne_proper_2 _.
......@@ -284,14 +344,14 @@ Global Instance impl_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Proof.
intros P P' HP Q Q' HQ; split=> x n' ??.
split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
Qed.
Global Instance impl_proper :
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 ??.
split; intros (x1&x2&?&?&?); cofe_subst x;
unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
exists x1, x2; split_and!; try (apply HP || apply HQ);
eauto using cmra_validN_op_l, cmra_validN_op_r.
Qed.
......@@ -300,7 +360,7 @@ Global Instance sep_proper :
Global Instance wand_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
Proof.
intros P P' HP Q Q' HQ; split=> n' x ??; split; intros HPQ x' n'' ???;
intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
......@@ -308,7 +368,7 @@ Global Instance wand_proper :
Global Instance eq_ne (A : cofeT) n :
Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
Proof.
intros x x' Hx y y' Hy; split=> n' z; split; intros; simpl in *.
intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
* by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
* by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.
......@@ -316,42 +376,51 @@ Global Instance eq_proper (A : cofeT) :
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Ψ; split=> n' x; split; intros HP a; apply HΨ. Qed.
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).
Proof. by intros Ψ1 Ψ2 HΨ; split=> n' x; split; intros HP a; apply HΨ. Qed.
Proof.
by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
Qed.
Global Instance exist_ne A n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
Proof.
intros Ψ1 Ψ2 HΨ; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
intros Ψ1 Ψ2 HΨ.
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).
Proof.
intros Ψ1 Ψ2 HΨ; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
intros Ψ1 Ψ2 HΨ.
unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
Qed.
Global Instance later_contractive : Contractive (@uPred_later M).
Proof.
intros n P Q HPQ; split=> -[|n'] x ??; simpl; [done|].
intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
apply (HPQ n'); eauto using cmra_validN_S.
Qed.
Global Instance later_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; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
intros P1 P2 HP.
unseal; split=> n' x; split; apply HP; eauto using cmra_unit_validN.
Qed.
Global Instance always_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; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
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 valid_ne {A : cmraT} n :
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
intros a b Ha; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
intros a b Ha; unseal; split=> n' x ? /=.
by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance valid_proper {A : cmraT} :
Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
......@@ -362,54 +431,59 @@ Global Instance iff_proper :
(** Introduction and elimination rules *)
Lemma const_intro φ P : φ → P ⊑ ■ φ.
Proof. by intros ?; split. Qed.
Proof. by intros ?; unseal; split. Qed.
Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
Proof. intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto. Qed.
Proof.
unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
Lemma False_elim P : False ⊑ P.
Proof. by split=> n x ?. Qed.
Proof. by unseal; split=> n x ?. Qed.
Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
Proof. by split=> n x ? [??]. Qed.
Proof. by unseal; split=> n x ? [??]. Qed.
Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
Proof. by split=> n x ? [??]. Qed.
Proof. by unseal; split=> n x ? [??]. Qed.
Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
Proof. intros HQ HR; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
Proof. split=> n x ??; left; auto. Qed.
Proof. unseal; split=> n x ??; left; auto. Qed.
Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
Proof. split=> n x ??; right; auto. Qed.
Proof. unseal; split=> n x ??; right; auto. Qed.
Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
Proof. intros HP HQ; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
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).
Proof.
intros HQ; split=> n x ?? n' x' ????.
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.
Proof. by intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
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).
Proof. by intros HPΨ; split=> n x ?? a; apply HPΨ. Qed.
Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
Proof. split=> n x ? HP; apply HP. Qed.
Proof. unseal; split=> n x ? HP; apply HP. Qed.
Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
Proof. by split=> n x ??; exists a. Qed.
Proof. unseal; split=> n x ??; by exists a. Qed.
Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
Proof. by intros HΦΨ; split=> n x ? [a ?]; apply HΦΨ with a. Qed.
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).
Proof. by split=> n x ??; simpl. Qed.
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.
Proof.
intros Hab Ha; split=> n x ??.
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, !CMRAIdentity M} {A : cofeT} (a b : A) :
True ⊑ (a ≡ b) → a ≡ b.
Proof.
intros Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
apply cmra_valid_validN, cmra_empty_valid.
Qed.
Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
Proof. by intros HPQ; split=> n x ?; split; intros; apply HPQ with n x. Qed.
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.
......@@ -579,23 +653,24 @@ Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_ne. Q
(* BI connectives *)
Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
Proof.
intros HQ HQ'; split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
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).
Proof.
intros P; split=> n x Hvalid; split.
intros P; unseal; split=> n x Hvalid; split.
- intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
- by intros ?; exists (unit x), x; rewrite cmra_unit_l.
Qed.
Global Instance sep_comm : Comm (≡) (@uPred_sep M).
Proof.
by intros P Q; split=> n x ?; split;
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).
Proof.
intros P Q R; split=> n x ?; split.
intros P Q R; unseal; split=> n x ?; split.
- intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_and?; auto.
+ by rewrite -(assoc op) -Hy -Hx.
+ by exists x1, y1.
......@@ -605,12 +680,14 @@ Proof.
Qed.
Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
Proof.
intros HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
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 : ((P -★ Q) ★ P) ⊑ Q.
Proof. by split; intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
Proof.
unseal; split; intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; by apply HPQ.
Qed.
(* Derived BI Stuff *)
Hint Resolve sep_mono.
......@@ -715,33 +792,37 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
(* Always *)
Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
Proof. done. Qed.
Proof. by unseal. Qed.
Lemma always_elim P : □ P ⊑ P.
Proof. split=> n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
Proof.
unseal; split=> n x ? /=; eauto using uPred_weaken, cmra_included_unit.
Qed.
Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
Proof.
intros HPQ; split=> n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
unseal=> HPQ.
split=> n x ??; apply HPQ; simpl; auto using cmra_unit_validN.
by rewrite cmra_unit_idemp.
Qed.
Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
Proof. done. Qed.
Proof. by unseal. Qed.
Lemma always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
Proof. done. Qed.
Proof. by unseal. Qed.
Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a)%I ≡ (∀ a, □ Ψ a)%I.