Commit 14a8f568 authored by Dan Frumin's avatar Dan Frumin
Browse files

Strengthen the `a_invoke_spec` rule

parent 1c256b12
...@@ -267,8 +267,7 @@ Section proofs. ...@@ -267,8 +267,7 @@ Section proofs.
IntoVal ef f IntoVal ef f
(R R1 R2) (R R1 R2)
awp ea R Ψ - awp ea R Ψ -
U ( a, Ψ a - R1 - (awp (ef a) R2 (λ v, R1 Φ v))) - ( a, Ψ a - U (R1 - (awp (ef a) R2 (λ v, R1 Φ v)))) -
(* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ ?? *)
awp (a_invoke ef ea) R Φ. awp (a_invoke ef ea) R Φ.
Proof. Proof.
iIntros (<-%of_to_val HR12) "Ha Hfa". iIntros (<-%of_to_val HR12) "Ha Hfa".
...@@ -277,19 +276,19 @@ Section proofs. ...@@ -277,19 +276,19 @@ Section proofs.
iIntros (a) "Ha". awp_let. iIntros (a) "Ha". awp_let.
iApply a_sequence_spec. iApply a_sequence_spec.
iApply (awp_wand with "Ha"). clear a. iApply (awp_wand with "Ha"). clear a.
iIntros (a) "HΨ". iModIntro. iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ").
iModIntro.
awp_let. awp_let.
iApply awp_atomic. iIntros "HR". iApply awp_atomic. iIntros "HR".
iDestruct (HR12 with "HR") as "[HR1 HR2]". iDestruct (HR12 with "HR") as "[HR1 HR2]".
iExists R2. iFrame. awp_let. iExists R2. iFrame. awp_let.
iSpecialize ("Hfa" with "HΨ").
iApply (awp_wand with "[Hfa HR1]"). iApply (awp_wand with "[Hfa HR1]").
{ by iApply "Hfa". } { by iApply "Hfa". }
iIntros (v) "[HR1 $] HR2". iIntros (v) "[HR1 $] HR2".
iApply HR12. iFrame. iApply HR12. iFrame.
Qed. Qed.
Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :
awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ. awp e1 R Φ - awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ.
Proof. Proof.
......
...@@ -25,6 +25,7 @@ Section contents. ...@@ -25,6 +25,7 @@ Section contents.
rewrite !bi.big_sepL_nil. eauto. rewrite !bi.big_sepL_nil. eauto.
Qed. Qed.
(** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Lemma U_sep_2 P Q : U P U Q U (P Q). Lemma U_sep_2 P Q : U P U Q U (P Q).
Proof. Proof.
iIntros "[HP HQ]". iIntros "[HP HQ]".
...@@ -36,6 +37,19 @@ Section contents. ...@@ -36,6 +37,19 @@ Section contents.
- by iApply "HQ2". - by iApply "HQ2".
Qed. Qed.
Lemma U_stength P Q : P U Q U (P Q).
Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.
Lemma U_applicative P Q : U (P - Q) U P - U Q.
Proof.
iDestruct 1 as (ls1) "[HPQ1 HPQ2]".
iDestruct 1 as (ls2) "[HP1 HP2]".
iExists (ls1++ls2). rewrite !bi.big_sepL_app. iFrame.
iIntros "[HPQ1 HP1]".
iApply ("HPQ2" with "HPQ1").
iApply ("HP2" with "HP1").
Qed.
Lemma U_unlock l v : l L v U (l U v). Lemma U_unlock l v : l L v U (l U v).
Proof. Proof.
iIntros "Hl". iExists [(l,v)]. iIntros "/= {$Hl} [$ _]". iIntros "Hl". iExists [(l,v)]. iIntros "/= {$Hl} [$ _]".
......
...@@ -66,13 +66,13 @@ Section test. ...@@ -66,13 +66,13 @@ Section test.
IntoVal ef f IntoVal ef f
awp ea R Ψ - awp ea R Ψ -
U ( a, Ψ a - (awp (ef a) R Φ)) - U ( a, Ψ a - (awp (ef a) R Φ)) -
(* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ ?? *) (* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ *)
awp (a_invoke ef ea) R Φ. awp (a_invoke ef ea) R Φ.
Proof. Proof.
iIntros (<-%of_to_val) "Ha Hfa". iIntros (<-%of_to_val) "Ha Hfa".
iApply (a_invoke_spec _ _ R True%I R with "Ha"). iApply (a_invoke_spec _ _ R True%I R with "Ha").
{ by rewrite bi.True_sep'. } { by rewrite bi.True_sep'. }
iModIntro. iIntros (a) "HΨ _". iIntros (a) "HΨ". iModIntro. iIntros (_).
iSpecialize ("Hfa" with "HΨ"). iSpecialize ("Hfa" with "HΨ").
iApply (awp_wand with "Hfa"). eauto. iApply (awp_wand with "Hfa"). eauto.
Qed. Qed.
......
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