add a_if_spec

theories/c_translation/translation.v

@@ -92,7 +92,7 @@ Section proofs.
     awp v1 R (λ _, U (awp v2 R Φ)) -∗ awp (a_sequence v1 v2) R Φ.
   Proof.
     iIntros "HΦ". do 2 awp_lam. iApply awp_bind.
-    iApply (awp_wand _ (λ _,  U (awp v2 R Φ))%I _ _ with "[HΦ]"); first done.
+    iApply (awp_wand  with "[HΦ]"); first done.
     iIntros (v) "H". awp_lam. iApply awp_bind. iApply a_seq_spec.
     iUnlock. by awp_pure _.
     Qed.
@@ -213,8 +213,8 @@ Section proofs.
   Lemma a_if_true_spec R (e1 e2 : val) Φ :
      awp e1 R Φ -∗ awp (a_if (a_ret #true) e1 e2) R Φ.
   Proof.
-    unfold a_if. iIntros "HΦ".
-    awp_lam. awp_lam. awp_lam. awp_lam.
+    iIntros "HΦ".
+    do 4 awp_lam.
     iApply awp_bind.
     iApply awp_value.
     awp_lam. by awp_if_true.
@@ -223,10 +223,21 @@ Section proofs.
   Lemma a_if_false_spec R (e1 e2 : val) Φ :
      awp e2 R Φ -∗ awp (a_if (a_ret #false) e1 e2) R Φ.
   Proof.
-    unfold a_if. iIntros "HΦ".
-    awp_lam. awp_lam. awp_lam. awp_lam.
+    iIntros "HΦ".
+    do 4 awp_lam.
     iApply awp_bind.
     iApply awp_value.
     awp_lam. by awp_if_false.
   Qed.
+
+  Lemma a_if_spec R (e e1 e2 : val) Φ:
+    awp e R (λ cnd, (⌜cnd = #true⌝ ∧ awp e1 R Φ) ∨ (⌜cnd = #false⌝ ∧ awp e2 R Φ)) -∗
+    awp (a_if e e1 e2) R Φ.
+  Proof.
+    iIntros "HΦ". do 3 awp_lam.
+    iApply awp_bind. iApply (awp_wand with "HΦ").
+    iIntros (v) "[[% H] | [% H]]"; subst; by repeat awp_pure _.
+    Qed.
+
+
 End proofs.