Skip to content

GitLab

Commit b672285b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files
Options

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 9321e1ad 61adc968
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 397 additions and 409 deletions
algebra/agree.v
View file @ b672285b
......@@ -136,7 +136,7 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
(** Internalized properties *)
Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b) ⊣⊢ (a ≡ b : uPred M).
Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
Proof.
uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
Qed.
......
algebra/auth.v
View file @ b672285b
......@@ -164,14 +164,14 @@ Canonical Structure authUR :=
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
(✓ x) ⊣⊢ (match authoritative x with
| Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
| None => ✓ own x
| ExclBot' => False
end : uPred M).
✓ x ⊣⊢ (match authoritative x with
| Excl' a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
| None => ✓ own x
| ExclBot' => False
end : uPred M).
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
......
algebra/csum.v
View file @ b672285b
......@@ -241,22 +241,22 @@ Proof. by move=> H n[]? =>[|/H|]. Qed.
(** Internalized properties *)
Lemma csum_equivI {M} (x y : csum A B) :
(x ≡ y) ⊣⊢ (match x, y with
| Cinl a, Cinl a' => a ≡ a'
| Cinr b, Cinr b' => b ≡ b'
| CsumBot, CsumBot => True
| _, _ => False
end : uPred M).
x ≡ y ⊣⊢ (match x, y with
| Cinl a, Cinl a' => a ≡ a'
| Cinr b, Cinr b' => b ≡ b'
| CsumBot, CsumBot => True
| _, _ => False
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma csum_validI {M} (x : csum A B) :
(✓ x) ⊣⊢ (match x with
| Cinl a => ✓ a
| Cinr b => ✓ b
| CsumBot => False
end : uPred M).
✓ x ⊣⊢ (match x with
| Cinl a => ✓ a
| Cinr b => ✓ b
| CsumBot => False
end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
......
algebra/excl.v
View file @ b672285b
......@@ -102,11 +102,11 @@ Proof. split. apply _. by intros []. Qed.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
(x ≡ y) ⊣⊢ (match x, y with
| Excl a, Excl b => a ≡ b
| ExclBot, ExclBot => True
| _, _ => False
end : uPred M).
x ≡ y ⊣⊢ (match x, y with
| Excl a, Excl b => a ≡ b
| ExclBot, ExclBot => True
| _, _ => False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
......
algebra/frac.v
View file @ b672285b
......@@ -145,7 +145,7 @@ Qed.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
(x ≡ y) ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
x ≡ y ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma frac_validI {M} (x : frac A) :
✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M).
......
algebra/gmap.v
View file @ b672285b
......@@ -171,9 +171,9 @@ Canonical Structure gmapUR :=
UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
(** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma gmap_validI {M} m : (✓ m) ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
Proof. by uPred.unseal. Qed.
End cmra.
......
algebra/iprod.v
View file @ b672285b
......@@ -139,9 +139,9 @@ Section iprod_cmra.
UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma iprod_validI {M} g : (✓ g) ⊣⊢ (∀ i, ✓ g i : uPred M).
Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M).
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
......
algebra/list.v
View file @ b672285b
......@@ -227,9 +227,9 @@ Section cmra.
Qed.
(** Internalized properties *)
Lemma list_equivI {M} l1 l2 : (l1 ≡ l2) ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
Lemma list_validI {M} l : (✓ l) ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End cmra.
......
algebra/one_shot.v
View file @ b672285b
......@@ -196,22 +196,22 @@ Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
(** Internalized properties *)
Lemma one_shot_equivI {M} (x y : one_shot A) :
(x ≡ y) ⊣⊢ (match x, y with
| OneShotPending, OneShotPending => True
| Shot a, Shot b => a ≡ b
| OneShotBot, OneShotBot => True
| _, _ => False
end : uPred M).
x ≡ y ⊣⊢ (match x, y with
| OneShotPending, OneShotPending => True
| Shot a, Shot b => a ≡ b
| OneShotBot, OneShotBot => True
| _, _ => False
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma one_shot_validI {M} (x : one_shot A) :
(✓ x) ⊣⊢ (match x with
| Shot a => ✓ a
| OneShotBot => False
| _ => True
end : uPred M).
✓ x ⊣⊢ (match x with
| Shot a => ✓ a
| OneShotBot => False
| _ => True
end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
......
algebra/upred.v
View file @ b672285b
This diff is collapsed.
algebra/upred_big_op.v
View file @ b672285b
......@@ -83,9 +83,9 @@ Proof.
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ ([∧] Ps ∧ [∧] Qs).
Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs.
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ ([★] Ps ★ [★] Qs).
Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
......@@ -113,7 +113,7 @@ Section gmap.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
([★ map] k ↦ x ∈ m1, Φ k x) ⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x.
Proof.
intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
......@@ -152,12 +152,12 @@ Section gmap.
Lemma big_sepM_insert Φ m i x :
m !! i = None →
([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ m, Φ k y).
([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_delete Φ m i x :
m !! i = Some x →
([★ map] k↦y ∈ m, Φ k y) ⊣⊢ (Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y).
([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
Proof.
intros. rewrite -big_sepM_insert ?lookup_delete //.
by rewrite insert_delete insert_id.
......@@ -204,7 +204,7 @@ Section gmap.
Lemma big_sepM_sepM Φ Ψ m :
([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
⊣⊢ (([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x)).
⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
......@@ -212,7 +212,7 @@ Section gmap.
Qed.
Lemma big_sepM_later Φ m :
(▷ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
▷ ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
......@@ -228,7 +228,7 @@ Section gmap.
Qed.
Lemma big_sepM_always_if p Φ m :
(□?p [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
□?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
Proof. destruct p; simpl; auto using big_sepM_always. Qed.
Lemma big_sepM_forall Φ m :
......@@ -249,7 +249,7 @@ Section gmap.
Qed.
Lemma big_sepM_impl Φ Ψ m :
(□ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ [★ map] k↦x ∈ m, Φ k x)
□ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x)
⊢ [★ map] k↦x ∈ m, Ψ k x.
Proof.
rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
......@@ -267,7 +267,7 @@ Section gset.
Lemma big_sepS_mono Φ Ψ X Y :
Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) →
([★ set] x ∈ X, Φ x) ⊢ ([★ set] x ∈ Y, Ψ x).
([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x.
Proof.
intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
......@@ -315,7 +315,7 @@ Section gset.
Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
Lemma big_sepS_delete Φ X x :
x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y).
x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
......@@ -328,21 +328,21 @@ Section gset.
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ (([★ set] y ∈ X, Φ y) ★ [★ set] y ∈ X, Ψ y).
([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later Φ X : (▷ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
Lemma big_sepS_later Φ X : ▷ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
by rewrite later_sep IH.
Qed.
Lemma big_sepS_always Φ X : (□ [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const.
......@@ -350,7 +350,7 @@ Section gset.
Qed.
Lemma big_sepS_always_if q Φ X :
(□?q [★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
□?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
Proof. destruct q; simpl; auto using big_sepS_always. Qed.
Lemma big_sepS_forall Φ X :
......@@ -369,7 +369,7 @@ Section gset.
Qed.
Lemma big_sepS_impl Φ Ψ X :
(□ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ [★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
□ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
Proof.
rewrite always_and_sep_l always_forall.
setoid_rewrite always_impl; setoid_rewrite always_const.
......
algebra/upred_tactics.v
View file @ b672285b
......@@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
eval Σ e1' ⊢ eval Σ e2' → eval Σ e1 ⊢ eval Σ e2.
(eval Σ e1' ⊢ eval Σ e2') → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
......
heap_lang/lib/barrier/proof.v
View file @ b672285b
......@@ -77,8 +77,8 @@ Proof. solve_proper. Qed.
(** Helper lemmas *)
Lemma ress_split i i1 i2 Q R1 R2 P I :
i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
(saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★
(Q -★ R1 ★ R2) ★ ress P I)
saved_prop_own i Q ★ saved_prop_own i1 R1 ★ saved_prop_own i2 R2 ★
(Q -★ R1 ★ R2) ★ ress P I
⊢ ress P ({[i1;i2]} ∪ I ∖ {[i]}).
Proof.
iIntros {????} "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as {Ψ} "[HPΨ HΨ]".
......@@ -97,7 +97,7 @@ Qed.
(** Actual proofs *)
Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
heapN ⊥ N →
(heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ #l)
heap_ctx heapN ★ (∀ l, recv l P ★ send l P -★ Φ #l)
⊢ WP newbarrier #() {{ Φ }}.
Proof.
iIntros {HN} "[#? HΦ]".
......@@ -124,7 +124,7 @@ Proof.
Qed.
Lemma signal_spec l P (Φ : val → iProp) :
(send l P ★ P ★ Φ #()) ⊢ WP signal #l {{ Φ }}.
send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
Proof.
rewrite /signal /send /barrier_ctx.
iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as {γ} "[#(%&Hh&Hsts) Hγ]". wp_let.
......@@ -139,7 +139,7 @@ Proof.
Qed.
Lemma wait_spec l P (Φ : val → iProp) :
(recv l P ★ (P -★ Φ #())) ⊢ WP wait #l {{ Φ }}.
recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}.
Proof.
rename P into R; rewrite /recv /barrier_ctx.
iIntros "[Hr HΦ]"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
......@@ -200,7 +200,7 @@ Proof.
by iIntros "> ?".
Qed.
Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ (recv l P1 -★ recv l P2).
Lemma recv_weaken l P1 P2 : (P1 -★ P2) ⊢ recv l P1 -★ recv l P2.
Proof.
rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as {γ P Q i} "(#Hctx&Hγ&Hi&HP1)".
......@@ -208,7 +208,7 @@ Proof.
iIntros "> HQ". by iApply "HP"; iApply "HP1".
Qed.
Lemma recv_mono l P1 P2 : P1 ⊢ P2 → recv l P1 ⊢ recv l P2.
Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
Proof.
intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
Qed.
......
heap_lang/lib/barrier/specification.v
View file @ b672285b
......@@ -17,7 +17,7 @@ Lemma barrier_spec (heapN N : namespace) :
(∀ l P, {{ send l P ★ P }} signal #l {{ _, True }}) ∧
(∀ l P, {{ recv l P }} wait #l {{ _, P }}) ∧
(∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧
(∀ l P Q, (P -★ Q) ⊢ (recv l P -★ recv l Q)).
(∀ l P Q, (P -★ Q) ⊢ recv l P -★ recv l Q).
Proof.
intros HN.
exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)).
......
heap_lang/lib/lock.v
View file @ b672285b
......@@ -51,8 +51,7 @@ Qed.
Lemma newlock_spec N (R : iProp) Φ :
heapN ⊥ N →
(heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l))
⊢ WP newlock #() {{ Φ }}.
heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
Proof.
iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
......@@ -63,7 +62,7 @@ Proof.
Qed.
Lemma acquire_spec l R (Φ : val → iProp) :
(is_lock l R ★ (locked l R -★ R -★ Φ #())) ⊢ WP acquire #l {{ Φ }}.
is_lock l R ★ (locked l R -★ R -★ Φ #()) ⊢ WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as {N γ} "(%&#?&#?)".
iLöb as "IH". wp_rec. wp_focus (CAS _ _ _)%E.
......@@ -77,7 +76,7 @@ Proof.
Qed.
Lemma release_spec R l (Φ : val → iProp) :
(locked l R ★ R ★ Φ #()) ⊢ WP release #l {{ Φ }}.
locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
Proof.
iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as {N γ} "(% & #? & #? & Hγ)".
rewrite /release. wp_let. iInv N as {b} "[Hl _]".
......
heap_lang/lib/spawn.v
View file @ b672285b
......@@ -54,7 +54,7 @@ Proof. solve_proper. Qed.
Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
to_val e = Some f →
heapN ⊥ N →
(heap_ctx heapN ★ WP f #() {{ Ψ }} ★ ∀ l, join_handle l Ψ -★ Φ #l)
heap_ctx heapN ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
⊢ WP spawn e {{ Φ }}.
Proof.
iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
......@@ -72,7 +72,7 @@ Proof.
Qed.
Lemma join_spec (Ψ : val → iProp) l (Φ : val → iProp) :
(join_handle l Ψ ★ ∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
join_handle l Ψ ★ (∀ v, Ψ v -★ Φ v) ⊢ WP join #l {{ Φ }}.
Proof.
rewrite /join_handle; iIntros "[[% H] Hv]"; iDestruct "H" as {γ} "(#?&Hγ&#?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
......
heap_lang/proofmode.v
View file @ b672285b
......@@ -18,11 +18,11 @@ Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
to_val e = Some v →
Δ ⊢ heap_ctx N → nclose N ⊆ E →
(Δ ⊢ heap_ctx N) → nclose N ⊆ E →
StripLaterEnvs Δ Δ' →
(∀ l, ∃ Δ'',
envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
Δ'' ⊢ Φ (LitV (LitLoc l))) →
(Δ'' ⊢ Φ (LitV (LitLoc l)))) →
Δ ⊢ WP Alloc e @ E {{ Φ }}.
Proof.
intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
......@@ -33,10 +33,10 @@ Proof.
Qed.
Lemma tac_wp_load Δ Δ' N E i l q v Φ :
Δ ⊢ heap_ctx N → nclose N ⊆ E →
(Δ ⊢ heap_ctx N) → nclose N ⊆ E →
StripLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
Δ' ⊢ Φ v →
(Δ' ⊢ Φ v) →
Δ ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
......@@ -46,11 +46,11 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
to_val e = Some v' →
Δ ⊢ heap_ctx N → nclose N ⊆ E →
(Δ ⊢ heap_ctx N) → nclose N ⊆ E →
StripLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
(Δ'' ⊢ Φ (LitV LitUnit)) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
......@@ -59,10 +59,10 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
Δ ⊢ heap_ctx N → nclose N ⊆ E →
(Δ ⊢ heap_ctx N) → nclose N ⊆ E →
StripLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
Δ' ⊢ Φ (LitV (LitBool false)) →
(Δ' ⊢ Φ (LitV (LitBool false))) →
Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
......@@ -72,11 +72,11 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 → to_val e2 = Some v2 →
Δ ⊢ heap_ctx N → nclose N ⊆ E →
(Δ ⊢ heap_ctx N) → nclose N ⊆ E →
StripLaterEnvs Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
(Δ'' ⊢ Φ (LitV (LitBool true))) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros; subst.
rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
......
program_logic/adequacy.v
View file @ b672285b
......@@ -56,7 +56,7 @@ Proof.
by rewrite -Permutation_middle /= big_op_app.
Qed.
Lemma wp_adequacy_steps P Φ k n e1 t2 σ1 σ2 r1 :
P ⊢ WP e1 {{ Φ }} →
(P ⊢ WP e1 {{ Φ }}) →
nsteps step k ([e1],σ1) (t2,σ2) →
1 < n → wsat (k + n) ⊤ σ1 r1 →
P (k + n) r1 →
......@@ -70,7 +70,7 @@ Qed.
Lemma wp_adequacy_own Φ e1 t2 σ1 m σ2 :
✓ m →
(ownP σ1 ★ ownG m) ⊢ WP e1 {{ Φ }} →
(ownP σ1 ★ ownG m ⊢ WP e1 {{ Φ }}) →
rtc step ([e1],σ1) (t2,σ2) →
∃ rs2 Φs', wptp 2 t2 (Φ :: Φs') rs2 ∧ wsat 2 ⊤ σ2 (big_op rs2).
Proof.
......@@ -85,7 +85,7 @@ Qed.
Theorem wp_adequacy_result E φ e v t2 σ1 m σ2 :
✓ m →
(ownP σ1 ★ ownG m) ⊢ WP e @ E {{ v', ■ φ v' }} →
(ownP σ1 ★ ownG m ⊢ WP e @ E {{ v', ■ φ v' }}) →
rtc step ([e], σ1) (of_val v :: t2, σ2) →
φ v.
Proof.
......@@ -111,7 +111,7 @@ Qed.