fixed vcg_wp_bin_op

theories/vcgen/vcgen.v

@@ -499,19 +499,18 @@ Section vcg_spec.
                vcg_wp_continuation E Φ w.
   Proof.
     iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
-    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin. (*
-    * iExists (dval_interp E dw); iSplit.
+    destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin.
+    * iDestruct "Hwp" as (dw Hopt) "Hcont"; simplify_eq.
+    *  iExists (dval_interp E dw); iSplit.
       { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. }
       iExists E, dw, (denv_merge mOut m).
       apply dbin_op_eval_dSome_wf in Hbin; try done.
       rewrite -denv_merge_interp //. eauto with iFrame.
-    * destruct dw as [dw1|] eqn:Hdw; last done.
-      iExists  (dval_interp E dw1); iSplit.
+    * iDestruct "Hwp" as (dw0 Hopt) "Hcont"; simplify_eq.
+      destruct dw as [dw1|] eqn:Hdw; last done.
+      iExists  (dval_interp E dw0); iSplit; last done.
       iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin.
-      iExists E, dw1, (denv_merge mOut m).
-      rewrite -denv_merge_interp.
-      apply dbin_op_eval_dUnknown_wf in Hbin; try done. eauto with iFrame.
-  Qed. *) Admitted.
+  Qed.
 
   Lemma vcg_wp_store_correct E m dv1 dv2 Φ :
     denv_wf E m →