From 2d9c5f33a2e4bbcfece823637a873dd3ffd45976 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Feb 2016 01:35:52 +0100
Subject: [PATCH] Seal off all definitions in uPred.
The performance gain seems neglectable, unfortunatelly...
---
algebra/agree.v | 6 +-
algebra/auth.v | 4 +-
algebra/excl.v | 6 +-
algebra/fin_maps.v | 4 +-
algebra/iprod.v | 4 +-
algebra/option.v | 6 +-
algebra/upred.v | 286 +++++++++++++++++++++-----------
program_logic/adequacy.v | 12 +-
program_logic/ghost_ownership.v | 2 +-
program_logic/lifting.v | 12 +-
program_logic/ownership.v | 7 +-
program_logic/pviewshifts.v | 19 ++-
program_logic/resources.v | 6 +-
program_logic/sts.v | 2 +-
program_logic/weakestpre.v | 10 +-
15 files changed, 244 insertions(+), 142 deletions(-)
diff --git a/algebra/agree.v b/algebra/agree.v
index 982b59974..1271e9aba 100644
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -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.
diff --git a/algebra/auth.v b/algebra/auth.v
index fc20e68fd..69c0ca216 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -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. *)
diff --git a/algebra/excl.v b/algebra/excl.v
index c58861286..da9deda4e 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -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 :
diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index ac3c6a5f3..d8faf339d 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -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 _ {_ _} _.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 2590ae8c9..5222fad1d 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -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')}.
diff --git a/algebra/option.v b/algebra/option.v
index 678ced6db..ad179c513 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -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 :
diff --git a/algebra/upred.v b/algebra/upred.v
index f18d8e31b..94b8bbc7b 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -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.
-Proof. done. Qed.
+Proof. by unseal. Qed.
Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a, □ Ψ a)%I.
-Proof. done. Qed.
+Proof. by unseal. Qed.
Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
Proof.
- split=> n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
+ unseal; split=> n x ? [??].
+ exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
Qed.
Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
Proof.
- split=> n x ? [??]; exists (unit x), x; simpl in *.
+ unseal; split=> n x ? [??]; exists (unit x), x; simpl in *.
by rewrite cmra_unit_l cmra_unit_idemp.
Qed.
Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
-Proof. done. Qed.
+Proof. by unseal. Qed.
(* Always derived *)
Lemma always_mono P Q : P ⊑ Q → □ P ⊑ □ Q.
@@ -790,34 +871,34 @@ Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
(* Later *)
Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
Proof.
- intros HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
+ unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
Qed.
Lemma later_intro P : P ⊑ ▷ P.
Proof.
- split=> -[|n] x ??; simpl in *; [done|].
+ 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.
Proof.
- split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
+ 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_True' : True ⊑ (▷ True : uPred M).
-Proof. by split=> -[|n] x. Qed.
+Proof. unseal; by split=> -[|n] x. Qed.
Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
-Proof. by split=> -[|n] x; split. Qed.
+Proof. unseal; split=> -[|n] x; by split. Qed.
Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
-Proof. split=> -[|n] x; simpl; tauto. Qed.
+Proof. unseal; split=> -[|n] x; simpl; tauto. Qed.
Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
-Proof. by split=> -[|n] x. Qed.
+Proof. unseal; by split=> -[|n] x. Qed.
Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
-Proof. by split=> -[|[|n]] x. Qed.
+Proof. unseal; by split=> -[|[|n]] x. Qed.
Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
(▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
-Proof. split=> -[|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
+Proof. unseal; split=> -[|[|n]] x; split; done || by exists inhabitant. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
- split=> n x ?; split.
+ unseal; split=> n x ?; split.
- destruct n as [|n]; simpl.
{ by exists x, (unit x); rewrite cmra_unit_r. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
@@ -862,7 +943,7 @@ Qed.
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
Proof.
- split=> n x ?; split.
+ unseal; split=> n x ?; split.
- intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (assoc op)|].
split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
- intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 â‹… z2).
@@ -871,28 +952,30 @@ Proof.
Qed.
Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
Proof.
- split=> n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
+ split=> n x; split; [by apply always_elim|unseal; intros [a' Hx]]; simpl.
rewrite -(cmra_unit_idemp a) Hx.
apply cmra_unit_preservingN, cmra_includedN_l.
Qed.
Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
Proof. by intros <-; rewrite always_ownM_unit. Qed.
Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
-Proof. split=> n x ??. by exists x; simpl. Qed.
+Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
-Proof. split=> n x ??; by exists x; rewrite left_id. Qed.
+Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
(* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
-Proof. split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
+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.
-Proof. by intros ?; split=> n x ? _; simpl; apply cmra_valid_validN. Qed.
+Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
-Proof. intros Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
+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.
-Proof. done. Qed.
+Proof. by unseal. Qed.
Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
-Proof. split=> n x _; apply cmra_validN_op_l. Qed.
+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.
@@ -903,26 +986,24 @@ 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.
-Proof. done. Qed.
+Proof. by unseal. Qed.
Lemma prod_validI {A B : cmraT} (x : A * B) :
(✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
-Proof. done. Qed.
+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.
-Proof. done. Qed.
+Proof. by unseal. Qed.
(* Discrete *)
Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) :
(✓ a)%I ≡ (■✓ a : uPred M)%I.
-Proof. split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
+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.
Proof.
- intros ?. apply (anti_symm (⊑)).
- - split=> n x ? ? /=. by apply (timeless_iff n a).
- - eapply const_elim; first done. move=>->. apply eq_refl.
+ unseal=> ?. apply (anti_symm (⊑)); split=> n x ?; by apply (timeless_iff n).
Qed.
(* Timeless *)
@@ -930,16 +1011,19 @@ Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
Proof.
split.
- intros HP n x ??; induction n as [|n]; auto.
- by destruct (uPred_in_entails _ _ HP (S n) x); auto using cmra_validN_S.
- - move=> HP; split=> -[|n] x /=; auto; left.
+ move: HP; rewrite /TimelessP; unseal=> /uPred_in_entails /(_ (S n) x).
+ by destruct 1; auto using cmra_validN_S.
+ - move=> HP; rewrite /TimelessP; unseal; split=> -[|n] x /=; auto; left.
apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
Qed.
Global Instance const_timeless φ : TimelessP (■φ : uPred M)%I.
-Proof. by apply timelessP_spec=> -[|n] x. Qed.
+Proof. by apply timelessP_spec; unseal => -[|n] x. Qed.
Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
TimelessP (✓ a : uPred M)%I.
-Proof. apply timelessP_spec=> n x /=. by rewrite -!cmra_discrete_valid_iff. Qed.
+Proof.
+ apply timelessP_spec; unseal=> n x /=. by rewrite -!cmra_discrete_valid_iff.
+Qed.
Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
@@ -948,7 +1032,7 @@ Proof.
Qed.
Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
Proof.
- rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ????; auto.
+ rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto.
apply HP, HPQ, uPred_weaken with (S n') x'; eauto using cmra_validN_le.
Qed.
Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
@@ -960,17 +1044,17 @@ Proof.
Qed.
Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
Proof.
- rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ???; auto.
+ rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto.
apply HP, HPQ, uPred_weaken with (S n') x';
eauto 3 using cmra_validN_le, cmra_validN_op_r.
Qed.
Global Instance forall_timeless {A} (Ψ : A → uPred M) :
(∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
-Proof. by setoid_rewrite timelessP_spec=> HΨ n x ?? a; apply HΨ. Qed.
+Proof. by setoid_rewrite timelessP_spec; unseal=> HΨ n x ?? a; apply HΨ. Qed.
Global Instance exist_timeless {A} (Ψ : A → uPred M) :
(∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
Proof.
- by setoid_rewrite timelessP_spec=> HΨ [|n] x ?;
+ by setoid_rewrite timelessP_spec; unseal=> HΨ [|n] x ?;
[|intros [a ?]; exists a; apply HΨ].
Qed.
Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
@@ -980,10 +1064,12 @@ Proof.
Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) :
Timeless a → TimelessP (a ≡ b : uPred M)%I.
-Proof. by intro; apply timelessP_spec=> n x ??; apply equiv_dist, timeless. Qed.
+Proof.
+ intro; apply timelessP_spec; unseal=> n x ??; by apply equiv_dist, timeless.
+Qed.
Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
Proof.
- intros ?; apply timelessP_spec=> n x ??; apply cmra_included_includedN,
+ intro; apply timelessP_spec; unseal=> n x ??; apply cmra_included_includedN,
cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 6ddf73e2f..3d55dbad6 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -62,8 +62,8 @@ Proof.
intros Hht ????; apply (nsteps_wptp [Φ] k n ([e1],σ1) (t2,σ2) [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
- apply Hht with (k + n) r1; eauto using cmra_included_unit.
- eapply uPred.const_intro; eauto.
+ move: Hht; rewrite /ht; uPred.unseal=> Hht.
+ apply Hht with (k + n) r1; by eauto using cmra_included_unit.
Qed.
Lemma ht_adequacy_own Φ e1 t2 σ1 m σ2 :
✓ m →
@@ -74,9 +74,9 @@ Proof.
intros Hv ? [k ?]%rtc_nsteps.
eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
{ by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
- exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
+ uPred.unseal; exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- - by rewrite /uPred_holds /=.
+ - rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
- by apply ownG_spec.
Qed.
Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 :
@@ -90,8 +90,8 @@ Proof.
as (rs2&Qs&Hwptp&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst.
- apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; auto.
- by rewrite right_id_L.
+ move: Hwp. uPred.unseal=> /wp_value_inv Hwp.
+ destruct (Hwp (big_op rs) 2 ∅ σ2) as [r' []]; rewrite ?right_id_L; auto.
Qed.
Lemma ht_adequacy_reducible E Φ e1 e2 t2 σ1 m σ2 :
✓ m →
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 623d79489..9e580abf9 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -102,7 +102,7 @@ Proof.
first (eapply map_updateP_alloc_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
- by rewrite -(exist_intro γ) const_equiv.
+ by rewrite -(exist_intro γ) const_equiv // left_id.
Qed.
Lemma own_alloc a E : ✓ a → True ⊑ (|={E}=> ∃ γ, own γ a).
Proof.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 1bce6182c..8860136a5 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -16,7 +16,7 @@ Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Transparent uPred_holds.
-Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I.
+Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, ■True)))%I.
Lemma wp_lift_step E1 E2
(φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 σ1 :
@@ -27,7 +27,7 @@ Lemma wp_lift_step E1 E2
(■φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> || e2 @ E2 {{ Φ }} ★ wp_fork ef)
⊑ || e1 @ E2 {{ Φ }}.
Proof.
- intros ? He Hsafe Hstep; split=> n r ? Hvs; constructor; auto.
+ intros ? He Hsafe Hstep. uPred.unseal; split=> n r ? Hvs; constructor; auto.
intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1')
as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'.
destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws'].
@@ -38,7 +38,7 @@ Proof.
as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
{ split. by eapply Hstep. apply ownP_spec; auto. }
{ rewrite (comm _ r2) -assoc; eauto using wsat_le. }
- by exists r1', r2'; split_and?; [| |by intros ? ->].
+ exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->.
Qed.
Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
@@ -47,11 +47,13 @@ Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
(∀ σ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 {{ Φ }}.
Proof.
- intros He Hsafe Hstep; split=> n r ? Hwp; constructor; auto.
+ intros He Hsafe Hstep; uPred.unseal; split=> n r ? Hwp; constructor; auto.
intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
- exists r1,r2; split_and?; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
+ exists r1,r2; split_and?; try done.
+ - rewrite -Hr; eauto using wsat_le.
+ - uPred.unseal; by intros ? ->.
Qed.
(** Derived lifting lemmas. *)
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index ce69c6dff..4b2c543bb 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -75,7 +75,8 @@ Lemma ownI_spec n r i P :
✓{n} r →
(ownI i P) n r ↔ wld r !! i ≡{n}≡ Some (to_agree (Next (iProp_unfold P))).
Proof.
- intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
+ intros (?&?&?). rewrite /ownI; uPred.unseal.
+ rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
- intros [(P'&Hi&HP) _]; rewrite Hi.
by apply Some_dist, symmetry, agree_valid_includedN,
(cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
@@ -83,11 +84,13 @@ Proof.
Qed.
Lemma ownP_spec n r σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡ Excl σ.
Proof.
- intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
+ intros (?&?&?). rewrite /ownP; uPred.unseal.
+ rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply cmra_empty_leastN).
Qed.
Lemma ownG_spec n r m : (ownG m) n r ↔ Some m ≼{n} gst r.
Proof.
+ rewrite /ownG; uPred.unseal.
rewrite /uPred_holds /= res_includedN; naive_solver (apply cmra_empty_leastN).
Qed.
End ownership.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index 936168700..f2b597942 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -63,7 +63,7 @@ Qed.
Lemma pvs_timeless E P : TimelessP P → (▷ P) ⊑ (|={E}=> P).
Proof.
rewrite uPred.timelessP_spec=> HP.
- split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
+ uPred.unseal; split=>-[|n] r ? HP' rf k Ef σ ???; first lia.
exists r; split; last done.
apply HP, uPred_weaken with n r; eauto using cmra_validN_le.
Qed.
@@ -82,7 +82,7 @@ Proof.
Qed.
Lemma pvs_frame_r E1 E2 P Q : ((|={E1,E2}=> P) ★ Q) ⊑ (|={E1,E2}=> P ★ Q).
Proof.
- split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
+ uPred.unseal; split; intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
{ by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
exists (r' â‹… r2); split; last by rewrite -assoc.
@@ -90,7 +90,7 @@ Proof.
Qed.
Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
Proof.
- split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
+ uPred.unseal; split=> -[|n] r ? Hinv rf [|k] Ef σ ???; try lia.
apply ownI_spec in Hinv; last auto.
destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
{ rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
@@ -99,7 +99,7 @@ Proof.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ (|={∅,{[i]}}=> True).
Proof.
- split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
+ uPred.unseal; split=> -[|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia.
exists ∅; split; [done|].
rewrite left_id; apply wsat_close with P r.
- apply ownI_spec, uPred_weaken with (S n) r; auto.
@@ -111,7 +111,7 @@ Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■P m' ∧ ownG m').
Proof.
intros Hup%option_updateP'.
- split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
+ uPred.unseal; split=> -[|n] r ? /ownG_spec Hinv rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
{ apply cmra_includedN_le with (S n); auto. }
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
@@ -120,20 +120,21 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
E (P : iGst Λ Σ → Prop) :
∅ ~~>: P → True ⊑ (|={E}=> ∃ m', ■P m' ∧ ownG m').
Proof.
- intros Hup; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
+ intros Hup; uPred.unseal; split=> -[|n] r ? _ rf [|k] Ef σ ???; try lia.
destruct (wsat_update_gst k (E ∪ Ef) σ r rf ∅ P) as (m'&?&?); eauto.
{ apply cmra_empty_leastN. }
{ apply cmra_updateP_compose_l with (Some ∅), option_updateP with P;
auto using option_update_None. }
- by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
+ exists (update_gst m' r); by split; [exists m'; split; [|apply ownG_spec]|].
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■(i ∈ E) ∧ ownI i P).
Proof.
- intros ?; split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
+ intros ?; rewrite /ownI; uPred.unseal.
+ split=> -[|n] r ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
{ apply uPred_weaken with n r; eauto. }
exists (Res {[ i := to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
- by split; [by exists i; split; rewrite /uPred_holds /=|].
+ split; [|done]. by exists i; split; rewrite /uPred_holds /=.
Qed.
(** * Derived rules *)
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 565fbc4b4..e15b59ba6 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -162,9 +162,11 @@ 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.
-Proof. do 2 split. by destruct 1. by intros (?&?&?); constructor. Qed.
+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.
-Proof. done. Qed.
+Proof. by uPred.unseal. Qed.
End res.
Arguments resC : clear implicits.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 8c9480ab5..2d369c1b2 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -179,7 +179,7 @@ Section sts.
(sts_own γ s' T' -★ Ψ x))) →
P ⊑ fsa E Ψ.
Proof.
- rewrite sts_own_eq. intros. eapply sts_fsaS; try done; []. (* FIXME: slow *)
+ rewrite sts_own_eq. intros. eapply sts_fsaS; try done; [].
by rewrite sts_ownS_eq sts_own_eq.
Qed.
End sts.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index ce191a7dd..213bbcbb4 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -158,11 +158,12 @@ Proof.
Qed.
Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} ★ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
Proof.
- split; intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
+ uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
rewrite Hr; clear Hr; revert e r Hwp.
induction n as [n IH] using lt_wf_ind; intros e r1.
destruct 1 as [|n r e ? Hgo]=>?.
- { constructor; apply pvs_frame_r; auto. exists r, rR; eauto. }
+ { constructor. rewrite -uPred_sep_eq; apply pvs_frame_r; auto.
+ uPred.unseal; exists r, rR; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep]; auto.
{ by rewrite assoc. }
@@ -176,7 +177,7 @@ Qed.
Lemma wp_frame_later_r E e Φ R :
to_val e = None → (|| e @ E {{ Φ }} ★ ▷ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
Proof.
- intros He; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
+ intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?).
revert Hvalid; rewrite Hr; clear Hr.
destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega.
@@ -185,7 +186,8 @@ Proof.
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
exists (r2 â‹… rR), r2'; split_and?; auto.
- by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- - apply wp_frame_r; [auto|exists r2, rR; split_and?; auto].
+ - rewrite -uPred_sep_eq.
+ apply wp_frame_r; [auto|uPred.unseal; exists r2, rR; split_and?; auto].
eapply uPred_weaken with n rR; eauto.
Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
--
GitLab