Commit 5ac2997a authored by Ralf Jung's avatar Ralf Jung

Merge remote-tracking branch 'origin/master' into ralf/greatest-fix

parents 968a2267 ea42f994
......@@ -49,10 +49,8 @@ Section proof.
( lo ln : loc,
lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R))%I.
Definition issued (γ : gname) (lk : val) (x : nat) (R : iProp Σ) : iProp Σ :=
( lo ln: loc,
lk = (#lo, #ln)%V inv N (lock_inv γ lo ln R)
own γ ( (, GSet {[ x ]})))%I.
Definition issued (γ : gname) (x : nat) : iProp Σ :=
own γ ( (, GSet {[ x ]}))%I.
Definition locked (γ : gname) : iProp Σ := ( o, own γ ( (Excl' o, )))%I.
......@@ -86,9 +84,9 @@ Section proof.
Qed.
Lemma wait_loop_spec γ lk x R :
{{{ issued γ lk x R }}} wait_loop #x lk {{{ RET #(); locked γ R }}}.
{{{ is_lock γ lk R issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ R }}}.
Proof.
iIntros (Φ) "Hl HΦ". iDestruct "Hl" as (lo ln) "(% & #? & Ht)".
iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln) "(% & #?)".
iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
iInv N as (o n) "(Hlo & Hln & Ha)" "Hclose".
wp_load. destruct (decide (x = o)) as [->|Hneq].
......@@ -129,7 +127,7 @@ Section proof.
rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
iModIntro. wp_if.
iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
+ rewrite /issued; eauto 10.
+ iFrame. rewrite /is_lock; eauto 10.
+ by iNext.
- wp_cas_fail.
iMod ("Hclose" with "[Hlo' Hln' Hauth Haown]") as "_".
......
......@@ -492,12 +492,15 @@ Qed.
(** * Implication and wand *)
Lemma tac_impl_intro Δ Δ' i P Q :
env_spatial_is_nil Δ = true
(if env_spatial_is_nil Δ then Unit else PersistentP P)
envs_app false (Esnoc Enil i P) Δ = Some Δ'
(Δ' Q) Δ P Q.
Proof.
intros ?? HQ. rewrite (persistentP Δ) envs_app_sound //; simpl.
by rewrite right_id always_wand_impl always_elim HQ.
intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (persistentP Δ) envs_app_sound //; simpl.
by rewrite right_id always_wand_impl always_elim.
- apply impl_intro_l. rewrite envs_app_sound //; simpl.
by rewrite always_and_sep_l right_id wand_elim_r.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
IntoPersistentP P P'
......
......@@ -7,7 +7,7 @@ Arguments Envs _ _%proof_scope _%proof_scope.
Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "" := Enil (format "", only printing) : proof_scope.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
......
......@@ -299,8 +299,10 @@ Local Tactic Notation "iIntro" constr(H) :=
first
[ (* (?Q → _) *)
eapply tac_impl_intro with _ H; (* (i:=H) *)
[reflexivity || fail 1 "iIntro: introducing" H
"into non-empty spatial context"
[env_cbv; apply _ ||
let P := lazymatch goal with |- PersistentP ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context"
|env_reflexivity || fail "iIntro:" H "not fresh"
|]
| (* (_ -∗ _) *)
......
......@@ -77,6 +77,9 @@ Proof.
done.
Qed.
Lemma test_iIntros_persistent P Q `{!PersistentP Q} : (P Q P Q)%I.
Proof. iIntros "H1 H2". by iFrame. Qed.
Lemma test_fast_iIntros P Q :
( x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x))%I.
......
Markdown is supported
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