Skip to content
Snippets Groups Projects
Commit af80690d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Define uPred_{equiv,dist,entails} as an inductive. 

This better seals off their definition. Although it did not give
much of a speedup, I think it is conceptually nicer.
parent bcfc00b8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 178 additions and 134 deletions
algebra/agree.v
+ 2
− 2
View file @ af80690d
......@@ -132,9 +132,9 @@ 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. split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne. Qed.
Proof. 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. by intros r n _ ?; apply: agree_op_inv. Qed.
Proof. split=> r n _ ?; by apply: agree_op_inv. Qed.
End agree.
Arguments agreeC : clear implicits.
......
algebra/dec_agree.v
+ 2
− 2
View file @ af80690d
......@@ -60,8 +60,8 @@ Proof.
Qed.
Lemma dec_agree_equivI {M} a b : (DecAgree a ≡ DecAgree b)%I ≡ (a = b : uPred M)%I.
Proof. split. by case. by destruct 1. Qed.
Proof. do 2 split. by case. by destruct 1. Qed.
Lemma dec_agree_validI {M} (x y : dec_agreeRA) : ✓ (x ⋅ y) ⊑ (x = y : uPred M).
Proof. intros r n _ ?. by apply: dec_agree_op_inv. Qed.
Proof. split=> r n _ ?. by apply: dec_agree_op_inv. Qed.
End dec_agree.
algebra/excl.v
+ 1
− 1
View file @ af80690d
......@@ -145,7 +145,7 @@ Lemma excl_equivI {M} (x y : excl A) :
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| _, _ => False
end : uPred M)%I.
Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
Proof. 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.
......
algebra/option.v
+ 1
− 1
View file @ af80690d
......@@ -138,7 +138,7 @@ 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. split. by destruct 1. by destruct x, y; try constructor. Qed.
Proof. 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.
......
algebra/upred.v
+ 133
− 98
View file @ af80690d
......@@ -21,10 +21,13 @@ Arguments uPred_holds {_} _%I _ _.
Section cofe.
Context {M : cmraT}.
Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ n x,
✓{n} x → P n x ↔ Q n x.
Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ n' x,
n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
Inductive uPred_equiv' (P Q : uPred M) : Prop :=
{ uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
{ uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
Instance uPred_dist : Dist (uPred M) := uPred_dist'.
Program Instance uPred_compl : Compl (uPred M) := λ c,
{| uPred_holds n x := c (S n) n x |}.
Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
......@@ -35,14 +38,16 @@ Section cofe.
Definition uPred_cofe_mixin : CofeMixin (uPred M).
Proof.
split.
- intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
intros HPQ n x ?; apply HPQ with n; auto.
- intros P Q; split.
+ by intros HPQ n; split=> i x ??; apply HPQ.
+ intros HPQ; split=> n x ?; apply HPQ with n; auto.
- intros n; split.
+ by intros P x i.
+ by intros P Q HPQ x i ??; symmetry; apply HPQ.
+ by intros P Q Q' HP HQ i x ??; trans (Q i x);[apply HP|apply HQ].
- intros n P Q HPQ i x ??; apply HPQ; auto.
- intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
+ by intros P; split=> x i.
+ by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
+ intros P Q Q' HP HQ; split=> i x ??.
by trans (Q i x);[apply HP|apply HQ].
- intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
- intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
Qed.
Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
End cofe.
......@@ -71,30 +76,32 @@ Qed.
Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
Proof.
by intros x1 x2 Hx n' y; split; apply Hx; auto using validN_preserving.
intros x1 x2 Hx; split=> n' y ??.
split; apply Hx; auto using validN_preserving.
Qed.
Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
Proof. by intros n x ?. Qed.
Proof. by split=> n x ?. Qed.
Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
`{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
Proof. by intros n x Hx. Qed.
Proof. by split=> n x Hx. Qed.
Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
`{!CMRAMonotone f, !CMRAMonotone g} :
(∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. move=> Hfg x P n Hx /=. by rewrite /uPred_holds /= Hfg. Qed.
`{!CMRAMonotone f} `{!CMRAMonotone g}:
(∀ x, f x ≡ g x) -> ∀ x, uPred_map f x ≡ uPred_map g x.
Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
`{!CMRAMonotone f, !CMRAMonotone g} n :
f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
Proof.
by intros Hfg P n' y ??;
by intros Hfg P; split=> n' y ??;
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
Qed.
(** logical entailement *)
Definition uPred_entails {M} (P Q : uPred M) := ∀ n x, ✓{n} x → P n x → Q n x.
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
{ uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
......@@ -218,9 +225,9 @@ Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%
Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
Arguments timelessP {_} _ {_} _ _ _ _.
Arguments timelessP {_} _ {_}.
Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
Arguments always_stable {_} _ {_} _ _ _ _.
Arguments always_stable {_} _ {_}.
Module uPred. Section uPred_logic.
Context {M : cmraT}.
......@@ -229,15 +236,20 @@ Implicit Types P Q : uPred M.
Implicit Types A : Type.
Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails.
Global Instance: PreOrder (@uPred_entails M).
Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
Proof.
split.
* 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).
Proof. intros P Q HPQ HQP; split; auto. Qed.
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.
Proof.
split; [|by intros [??]; apply (anti_symm (⊑))].
intros HPQ; split; intros x i; apply HPQ.
intros HPQ; split; split=> x i; apply HPQ.
Qed.
Lemma equiv_entails P Q : P ≡ Q → P ⊑ Q.
Proof. apply equiv_spec. Qed.
......@@ -253,31 +265,34 @@ Qed.
(** Non-expansiveness and setoid morphisms *)
Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
Proof. by intros φ1 φ2 Hφ [|n] ??; try apply Hφ. Qed.
Proof. intros φ1 φ2 Hφ. by 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; intros [??]; split; by apply HP || by apply HQ.
intros P P' HP Q Q' HQ; split=> x n' ??.
split; (intros [??]; split; [by apply HP|by apply HQ]).
Qed.
Global Instance and_proper :
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; intros [?|?];
first [by left; apply HP | by right; apply HQ].
intros P P' HP Q Q' HQ; split=> x n' ??.
split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
Qed.
Global Instance or_proper :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_or M) := ne_proper_2 _.
Global Instance impl_ne n :
Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
Proof.
intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
intros P P' HP Q Q' HQ; split=> x n' ??.
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 n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
exists x1, x2; split_and?; try (apply HP || apply HQ);
intros P P' HP Q Q' HQ; split=> n' x ??.
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.
Global Instance sep_proper :
......@@ -285,7 +300,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 n' x ??; split; intros HPQ n'' x' ???;
intros P P' HP Q Q' HQ; split=> n' x ??; split; intros HPQ x' n'' ???;
apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
Qed.
Global Instance wand_proper :
......@@ -293,41 +308,51 @@ 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 n' z; split; intros; simpl in *.
- by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
- by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
intros x x' Hx y y' Hy; split=> n' z; split; intros; simpl in *.
* by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
* by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
Qed.
Global Instance eq_proper (A : cofeT) :
Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
Global Instance forall_ne A :
Global Instance forall_ne A n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
Proof. by intros Ψ1 Ψ2 HΨ; 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Ψ n' x; split; intros HP a; apply HΨ. Qed.
Global Instance exist_ne A :
Proof. by intros Ψ1 Ψ2 HΨ; 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. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
Proof.
intros Ψ1 Ψ2 HΨ; 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. by intros P1 P2 HP n' x; split; intros [a ?]; exists a; apply HP. Qed.
Proof.
intros Ψ1 Ψ2 HΨ; 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 [|n'] x ??; simpl; [done|].
intros n P Q HPQ; 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 n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
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.
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. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
Proof.
intros a b Ha; 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. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
Proper (dist n ==> dist n) (@uPred_valid M A).
Proof.
intros a b Ha; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
Qed.
Global Instance valid_proper {A : cmraT} :
Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
......@@ -337,43 +362,45 @@ Global Instance iff_proper :
(** Introduction and elimination rules *)
Lemma const_intro φ P : φ → P ⊑ ■ φ.
Proof. by intros ???. Qed.
Proof. by intros ?; split. Qed.
Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
Proof. intros HQP HQR n x ??; apply HQR; first eapply (HQP n); eauto. Qed.
Proof. intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto. Qed.
Lemma False_elim P : False ⊑ P.
Proof. by intros n x ?. Qed.
Proof. by split=> n x ?. Qed.
Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
Proof. by intros n x ? [??]. Qed.
Proof. by split=> n x ? [??]. Qed.
Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
Proof. by intros n x ? [??]. Qed.
Proof. by split=> n x ? [??]. Qed.
Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
Proof. intros HQ HR n x ??; split; auto. Qed.
Proof. intros HQ HR; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
Proof. intros n x ??; left; auto. Qed.
Proof. split=> n x ??; left; auto. Qed.
Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
Proof. intros n x ??; right; auto. Qed.
Proof. split=> n x ??; right; auto. Qed.
Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
Proof. intros HP HQ n x ? [?|?]. by apply HP. by apply HQ. Qed.
Proof. intros HP HQ; 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; repeat intro; apply HQ; naive_solver eauto using uPred_weaken.
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' n x ??; apply HP with n x, HP'. Qed.
Proof. by 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Ψ n x ?? a; apply HPΨ. Qed.
Proof. by intros HPΨ; split=> n x ?? a; apply HPΨ. Qed.
Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
Proof. intros n x ? HP; apply HP. Qed.
Proof. split=> n x ? HP; apply HP. Qed.
Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
Proof. by intros n x ??; exists a. Qed.
Proof. by split=> n x ??; exists a. Qed.
Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
Proof. by intros HΦΨ n x ? [a ?]; apply HΦΨ with a. Qed.
Proof. by intros HΦΨ; split=> n x ? [a ?]; apply HΦΨ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
Proof. by intros n x ??; simpl. Qed.
Proof. 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 n x ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
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.
......@@ -382,7 +409,7 @@ Proof.
apply cmra_valid_validN, cmra_empty_valid.
Qed.
Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
Proof. by intros HPQ n x ?; split; intros; apply HPQ with n x. Qed.
Proof. by intros HPQ; split=> n x ?; split; intros; apply HPQ with n x. Qed.
(* Derived logical stuff *)
Lemma True_intro P : P ⊑ True.
......@@ -552,23 +579,23 @@ 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' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
intros HQ HQ'; 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 n x Hvalid; split.
intros P; 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 n x ?; split;
by intros P Q; 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 n x ?; split.
intros P Q R; 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.
......@@ -578,12 +605,12 @@ Proof.
Qed.
Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
Proof.
intros HPQR n x ?? n' x' ???; apply HPQR; auto.
intros 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 intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
Proof. by split; intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
(* Derived BI Stuff *)
Hint Resolve sep_mono.
......@@ -688,10 +715,10 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
Proof. done. Qed.
Lemma always_elim P : □ P ⊑ P.
Proof. intros n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
Proof. split=> n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
Proof.
intros HPQ n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
intros HPQ; split=> n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
by rewrite cmra_unit_idemp.
Qed.
Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
......@@ -704,11 +731,11 @@ Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a,
Proof. done. Qed.
Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
Proof.
intros n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
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.
intros n x ? [??]; exists (unit x), x; simpl in *.
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.
......@@ -720,6 +747,9 @@ Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
Hint Resolve always_mono.
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).
Proof. intros P Q; apply always_mono. Qed.
Lemma always_impl P Q : □ (P → Q) ⊑ (□ P → □ Q).
Proof.
apply impl_intro_l; rewrite -always_and.
......@@ -730,7 +760,7 @@ Proof.
apply (anti_symm (⊑)); auto using always_elim.
apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
rewrite -(eq_refl _ True) always_const; auto.
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.
......@@ -757,33 +787,35 @@ Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
(* Later *)
Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
Proof. intros HP [|n] x ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
Proof.
intros HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
Qed.
Lemma later_intro P : P ⊑ ▷ P.
Proof.
intros [|n] x ??; simpl in *; [done|].
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.
intros n x ? HP; induction n as [|n IH]; [by apply HP|].
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 intros [|n] x. Qed.
Proof. by split=> -[|n] x. Qed.
Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
Proof. by intros [|n] x; split. Qed.
Proof. by split=> -[|n] x; split. Qed.
Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
Proof. intros [|n] x; simpl; tauto. Qed.
Proof. split=> -[|n] x; simpl; tauto. Qed.
Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
Proof. by intros [|n] x. Qed.
Proof. by split=> -[|n] x. Qed.
Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
Proof. by intros [|[|n]] x. Qed.
Proof. by split=> -[|[|n]] x. Qed.
Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
(▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
Proof. intros [|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
Proof. split=> -[|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
Proof.
intros n x ?; split.
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_op n x x1 x2)
......@@ -796,6 +828,9 @@ Qed.
(* Later derived *)
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).
Proof. intros P Q; apply later_mono. Qed.
Lemma later_True : (▷ True : uPred M)%I ≡ True%I.
Proof. apply (anti_symm (⊑)); auto using later_True'. Qed.
Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q).
......@@ -825,7 +860,7 @@ Qed.
Lemma ownM_op (a1 a2 : M) :
uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
Proof.
intros n x ?; split.
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).
......@@ -834,28 +869,28 @@ Proof.
Qed.
Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
Proof.
intros n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
split=> n x; split; [by apply always_elim|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. intros n x ??. by exists x; simpl. Qed.
Proof. split=> n x ??. by exists x; simpl. Qed.
Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
Proof. intros n x ??; by exists x; rewrite left_id. Qed.
Proof. split=> n x ??; by exists x; rewrite left_id. Qed.
(* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
Proof. intros n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
Proof. 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 ? n x ? _; simpl; apply cmra_valid_validN. Qed.
Proof. by intros ?; split=> n x ? _; simpl; apply cmra_valid_validN. Qed.
Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
Proof. intros Ha n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
Proof. intros 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.
Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
Proof. intros n x _; apply cmra_validN_op_l. Qed.
Proof. split=> n x _; apply cmra_validN_op_l. Qed.
(* Own and valid derived *)
Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
......@@ -888,8 +923,8 @@ 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 (HP (S n) x); auto using cmra_validN_S.
- move=> HP [|n] x /=; auto; left.
by destruct (uPred_in_entails _ _ HP (S n) x); auto using cmra_validN_S.
- move=> HP; 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.
......@@ -944,7 +979,7 @@ Lemma timeless_eq {A : cofeT} (a b : A) :
Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
Proof.
intros ?. apply (anti_symm (⊑)).
- move=>n x ? ? /=. by apply (timeless_iff n a).
- split=> n x ? ? /=. by apply (timeless_iff n a).
- eapply const_elim; first done. move=>->. apply eq_refl.
Qed.
......
program_logic/lifting.v
+ 3
− 3
View file @ af80690d
......@@ -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 n r ? Hvs; constructor; auto.
intros ? He Hsafe Hstep; 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'].
......@@ -36,7 +36,7 @@ Proof.
constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 rf k Ef σ2)
as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
{ split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
{ split. by eapply Hstep. apply ownP_spec; auto. }
{ rewrite (comm _ r2) -assoc; eauto using wsat_le. }
by exists r1', r2'; split_and?; [| |by intros ? ->].
Qed.
......@@ -47,7 +47,7 @@ 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 n r ? Hwp; constructor; auto.
intros He Hsafe Hstep; 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.
......
program_logic/model.v
+ 3
− 2
View file @ af80690d
......@@ -24,8 +24,9 @@ Proof.
rewrite -uPred_map_compose. apply uPred_map_ext=>{P} r /=.
rewrite -res_map_compose. apply res_map_ext=>{r} r /=.
by rewrite -later_map_compose.
- intros A1 A2 B1 B2 n f f' Hf P n' [???].
apply upredC_map_ne, resC_map_ne, laterC_map_contractive=>i. by apply Hf.
- intros A1 A2 B1 B2 n f f' Hf P; split=> n' -[???].
apply upredC_map_ne, resC_map_ne, laterC_map_contractive.
by intros i ?; apply Hf.
Qed.
End iProp.
......
program_logic/pviewshifts.v
+ 20
− 14
View file @ af80690d
......@@ -42,7 +42,7 @@ Transparent uPred_holds.
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Proof.
intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
intros P Q HPQ; split=> n' r1 ??; simpl; split; intros HP rf k Ef σ ???;
destruct (HP rf k Ef σ) as (r2&?&?); auto;
exists r2; split_and?; auto; apply HPQ; eauto.
Qed.
......@@ -51,36 +51,38 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ⊑ |={E}=> P.
Proof.
intros n r ? HP rf k Ef σ ???; exists r; split; last done.
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).
Proof.
intros HPQ n r ? HP rf k Ef σ ???.
destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
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).
Proof.
rewrite uPred.timelessP_spec=> HP [|n] r ? HP' rf k Ef σ ???; first lia.
rewrite uPred.timelessP_spec=> HP.
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.
Lemma pvs_trans E1 E2 E3 P :
E2 ⊆ E1 ∪ E3 → (|={E1,E2}=> |={E2,E3}=> P) ⊑ (|={E1,E3}=> P).
Proof.
intros ? n r1 ? HP1 rf k Ef σ ???.
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).
Proof.
intros ? n r ? HP rf k Ef' σ ???.
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).
Proof.
intros n r ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
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.
......@@ -88,7 +90,7 @@ Proof.
Qed.
Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
Proof.
intros [|n] r ? Hinv rf [|k] Ef σ ???; try lia.
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. }
......@@ -97,7 +99,8 @@ Proof.
Qed.
Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ (|={∅,{[i]}}=> True).
Proof.
intros [|n] r ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
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.
- set_solver +HE.
......@@ -107,7 +110,8 @@ Qed.
Lemma pvs_ownG_updateP E m (P : iGst Λ Σ → Prop) :
m ~~>: P → ownG m ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
Proof.
intros Hup%option_updateP' [|n] r ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
intros Hup%option_updateP'.
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]|].
......@@ -116,7 +120,7 @@ Lemma pvs_ownG_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
E (P : iGst Λ Σ → Prop) :
∅ ~~>: P → True ⊑ (|={E}=> ∃ m', ■ P m' ∧ ownG m').
Proof.
intros Hup [|n] r ? _ rf [|k] Ef σ ???; try lia.
intros Hup; 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;
......@@ -125,7 +129,7 @@ Proof.
Qed.
Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ (|={E}=> ∃ i, ■ (i ∈ E) ∧ ownI i P).
Proof.
intros ? [|n] r ? HP rf [|k] Ef σ ???; try lia.
intros ?; 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)) ]} ∅ ∅).
......@@ -137,6 +141,9 @@ Opaque uPred_holds.
Import uPred.
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).
Proof. intros P Q; apply pvs_mono. Qed.
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).
......@@ -194,7 +201,6 @@ 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=> ->.
Qed.
End pvs.
(** * Frame Shift Assertions. *)
......
program_logic/resources.v
+ 1
− 1
View file @ af80690d
......@@ -162,7 +162,7 @@ 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. split. by destruct 1. by intros (?&?&?); constructor. Qed.
Proof. do 2 split. by destruct 1. by intros (?&?&?); constructor. Qed.
Lemma res_validI {M} r : (✓ r)%I ≡ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M)%I.
Proof. done. Qed.
End res.
......
program_logic/weakestpre.v
+ 12
− 10
View file @ af80690d
......@@ -71,7 +71,7 @@ Global Instance wp_ne E e n :
Proof.
cut (∀ Φ Ψ, (∀ v, Φ v ≡{n}≡ Ψ v) →
∀ n' r, n' ≤ n → ✓{n'} r → wp E e Φ n' r → wp E e Ψ n' r).
{ by intros help Φ Ψ HΦΨ; split; apply help. }
{ intros help Φ Ψ HΦΨ. by do 2 split; apply help. }
intros Φ Ψ HΦΨ n' r; revert e r.
induction n' as [n' IH] using lt_wf_ind=> e r.
destruct 3 as [n' r v HpvsQ|n' r e1 ? Hgo].
......@@ -90,7 +90,8 @@ Qed.
Lemma wp_mask_frame_mono E1 E2 e Φ Ψ :
E1 ⊆ E2 → (∀ v, Φ v ⊑ Ψ v) → || e @ E1 {{ Φ }} ⊑ || e @ E2 {{ Ψ }}.
Proof.
intros HE HΦ n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r.
intros HE HΦ; split=> n r.
revert e r; induction n as [n IH] using lt_wf_ind=> e r.
destruct 2 as [n' r v HpvsQ|n' r e1 ? Hgo].
{ constructor; eapply pvs_mask_frame_mono, HpvsQ; eauto. }
constructor; [done|]=> rf k Ef σ1 ???.
......@@ -114,20 +115,20 @@ Lemma wp_step_inv E Ef Φ e k n σ r rf :
Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed.
Lemma wp_value' E Φ v : Φ v ⊑ || of_val v @ E {{ Φ }}.
Proof. by constructor; apply pvs_intro. Qed.
Proof. split=> n r; constructor; by apply pvs_intro. Qed.
Lemma pvs_wp E e Φ : (|={E}=> || e @ E {{ Φ }}) ⊑ || e @ E {{ Φ }}.
Proof.
intros n r ? Hvs.
split=> n r ? Hvs.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; eapply pvs_trans', pvs_mono, Hvs; eauto.
intros ???; apply wp_value_inv. }
split=> ???; apply wp_value_inv. }
constructor; [done|]=> rf k Ef σ1 ???.
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 {{ Φ }}.
Proof.
intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ.
destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|].
{ constructor; apply pvs_trans', (wp_value_inv _ (pvs E E ∘ Φ)); auto. }
constructor; [done|]=> rf k Ef σ1 ???.
......@@ -140,7 +141,7 @@ Lemma wp_atomic E1 E2 e Φ :
E2 ⊆ E1 → atomic e →
(|={E1,E2}=> || e @ E2 {{ λ v, |={E2,E1}=> Φ v }}) ⊑ || e @ E1 {{ Φ }}.
Proof.
intros ? He n r ? Hvs; constructor; eauto using atomic_not_val.
intros ? He; split=> n r ? Hvs; constructor; eauto using atomic_not_val.
intros rf k Ef σ1 ???.
destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto.
destruct (wp_step_inv E2 Ef (pvs E2 E1 ∘ Φ) e k (S k) σ1 r' rf)
......@@ -157,7 +158,7 @@ Proof.
Qed.
Lemma wp_frame_r E e Φ R : (|| e @ E {{ Φ }} ★ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
Proof.
intros n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid.
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]=>?.
......@@ -175,7 +176,8 @@ Qed.
Lemma wp_frame_later_r E e Φ R :
to_val e = None → (|| e @ E {{ Φ }} ★ ▷ R) ⊑ || e @ E {{ λ v, Φ v ★ R }}.
Proof.
intros He n r' Hvalid (r&rR&Hr&Hwp&?); revert Hvalid; rewrite Hr; clear Hr.
intros He; 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.
destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
......@@ -189,7 +191,7 @@ Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
|| e @ E {{ λ v, || K (of_val v) @ E {{ Φ }} }} ⊑ || K e @ E {{ Φ }}.
Proof.
intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
split=> n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r ?.
destruct 1 as [|n r e ? Hgo]; [by apply pvs_wp|].
constructor; auto using fill_not_val=> rf k Ef σ1 ???.
destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment