Change the invoke specification

theories/c_translation/derived.v

@@ -65,6 +65,38 @@ Section derived.
     iApply a_store_ret. awp_load_ret t. iIntros "Ht".
     iExists v. iFrame. iSpecialize ("H" with "Ht"). done.
   Qed.
+
+  Lemma a_invoke_simpl (ef ea : expr) R Ψ Φ (f : val) :
+    IntoVal ef f →
+    awp ea R Ψ -∗
+    (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗
+    awp (a_invoke ef ea) R Φ.
+  Proof.
+    iIntros (<-%of_to_val) "Ha Hfa".
+    iApply (a_invoke_spec _ _ R with "Ha").
+    iIntros (a) "HΨ".
+    iSpecialize ("Hfa" with "HΨ"). iModIntro.
+    iIntros "HR".
+    iExists R. iFrame.
+    iApply (awp_wand with "Hfa"). eauto with iFrame.
+  Qed.
+
+  Lemma a_invoke_full (ef ea : expr) R Ψ Φ (f : val) :
+    IntoVal ef f →
+    awp ea R Ψ -∗
+    (∀ a, Ψ a -∗ U (R -∗ awp (ef a) True%I (λ v, R ∗ Φ v))) -∗
+    awp (a_invoke ef ea) R Φ.
+  Proof.
+    iIntros (<-%of_to_val) "Ha Hfa".
+    iApply (a_invoke_spec _ _ R with "Ha").
+    iIntros (a) "HΨ".
+    iSpecialize ("Hfa" with "HΨ"). iModIntro.
+    iIntros "HR".
+    iExists True%I. rewrite bi.True_sep'.
+    iSpecialize ("Hfa" with "HR").
+    iApply (awp_wand with "Hfa"). eauto with iFrame.
+  Qed.
+
 End derived.
 
 Ltac awp_load_ret l := iApply (a_load_ret l); iFrame; eauto.

theories/c_translation/translation.v

@@ -263,14 +263,13 @@ Section proofs.
     iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
   Qed.
 
-  Lemma a_invoke_spec (ef ea : expr) (R R1 R2 : iProp Σ) Ψ Φ (f : val) :
+  Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) :
     IntoVal ef f →
-    (R ⊣⊢ R1 ∗ R2) →
     awp ea R Ψ -∗
-    (∀ a, Ψ a -∗ U (R1 -∗ (awp (ef a) R2 (λ v, R1 ∗ Φ v)))) -∗
+    (∀ a, Ψ a -∗ U (R -∗ ∃ R', R' ∗ (awp (ef a) R' (λ v, R' -∗ R ∗ Φ v)))) -∗
     awp (a_invoke ef ea) R Φ.
   Proof.
-    iIntros (<-%of_to_val HR12) "Ha Hfa".
+    iIntros (<-%of_to_val) "Ha Hfa".
     rewrite /a_invoke. awp_lam.
     awp_apply (a_wp_awp R with "Ha").
     iIntros (a) "Ha". awp_let.
@@ -281,12 +280,8 @@ Section proofs.
     iModIntro.
     awp_let.
     iApply awp_atomic. iIntros "HR".
-    iDestruct (HR12 with "HR") as "[HR1 HR2]".
-    iExists R2. iFrame. awp_let.
-    iApply (awp_wand with "[Hfa HR1]").
-    { by iApply "Hfa". }
-    iIntros (v) "[HR1 $] HR2".
-    iApply HR12. iFrame.
+    iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
+    iExists R'. iFrame. by awp_let.
   Qed.
 
   Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ :

theories/tests/test1.v

@@ -62,30 +62,14 @@ Section test.
     iIntros "Hl2". awp_seq. iApply a_seq_spec. iModIntro. by iFrame.
   Qed.
 
-  Lemma a_invoke_spec_simpl (ef ea : expr) R Ψ Φ (f : val) :
-    IntoVal ef f →
-    awp ea R Ψ -∗
-    U (∀ a, Ψ a -∗ (awp (ef a) R Φ)) -∗
-    (* (∀ a, Ψ a -∗ U (awp (ef a) R Φ)) -∗ *)
-    awp (a_invoke ef ea) R Φ.
-  Proof.
-    iIntros (<-%of_to_val) "Ha Hfa".
-    iApply (a_invoke_spec _ _ R True%I R with "Ha").
-    { by rewrite bi.True_sep'. }
-    iIntros (a) "HΨ". iModIntro. iIntros (_).
-    iSpecialize ("Hfa" with "HΨ").
-    iApply (awp_wand with "Hfa"). eauto.
-  Qed.
-
   Lemma test_invoke (l : loc) R :
     l ↦L #1 -∗
     awp (a_invoke (λ: "x", a_load (a_ret "x")) (a_ret #l))%E R (fun v => ⌜v = #1⌝ ∗ l ↦U #1).
   Proof.
     iIntros "Hl".
-    iApply (a_invoke_spec_simpl _ _ _ (λ v, ⌜v = #l⌝)%I).
+    iApply (a_invoke_simpl _ _ _ (λ v, ⌜v = #l⌝)%I).
     { iApply awp_ret. by wp_value_head. }
-    iModIntro.
-    iIntros (? ->).
+    iIntros (? ->). iModIntro.
     awp_let. awp_load_ret l.
   Qed.