Tactical support for null comparison.

theories/lang/lifting.v

@@ -240,19 +240,6 @@ Proof.
   iApply step_fupd_intro; done.
 Qed.
 
-(* TODO: wp_eq for locations, if needed.
-Lemma wp_bin_op_heap E σ op l1 l2 l' :
-  bin_op_eval σ op l1 l2 l' →
-  {{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
-  {{{ l'', RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌝ ∗ ownP σ }}}.
-Proof.
-  iIntros (? Φ) "HP HΦ". iApply ownP_lift_atomic_head_step; eauto.
-  iFrame "HP". iNext. iIntros (e2 σ2 efs Hs) "Ho".
-  inv_head_step; rewrite big_sepL_nil right_id.
-  iApply "HΦ". eauto.
-Qed.
-*)
-
 Lemma wp_bin_op_pure E op l1 l2 l' :
   (∀ σ, bin_op_eval σ op l1 l2 l') →
   {{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
@@ -290,6 +277,24 @@ Proof.
   - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
 Qed.
 
+Lemma wp_eq_loc_0_r E (l : loc) P Φ :
+  (P -∗ ▷ Φ (LitV false)) →
+  P -∗ WP BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0)) @ E {{ Φ }}.
+Proof.
+  iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
+  rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+Qed.
+
+Lemma wp_eq_loc_0_l E (l : loc) P Φ :
+  (P -∗ ▷ Φ (LitV false)) →
+  P -∗ WP BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l)) @ E {{ Φ }}.
+Proof.
+  iIntros (HΦ) "HP". iApply wp_bin_op_pure. by intros; do 2 constructor.
+  rewrite HΦ. iNext. iIntros (?? Heval). by inversion_clear Heval; inv_lit.
+Qed.
+
+(* TODO: wp_eq for locations, if needed. *)
+
 Lemma wp_offset E l z Φ :
   ▷ Φ (LitV $ LitLoc $ shift_loc l z) -∗
     WP BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z) @ E {{ Φ }}.

theories/lang/proofmode.v

@@ -92,7 +92,12 @@ Tactic Notation "wp_op" :=
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
-    | BinOp EqOp _ _ => wp_bind_core K; apply wp_eq_int; wp_finish
+    | BinOp EqOp (Lit (LitInt _)) (Lit (LitInt _)) =>
+      wp_bind_core K; apply wp_eq_int; wp_finish
+    | BinOp EqOp (Lit (LitLoc _)) (Lit (LitInt 0)) =>
+      wp_bind_core K; apply wp_eq_loc_0_r; wp_finish
+    | BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc _)) =>
+      wp_bind_core K; apply wp_eq_loc_0_l; wp_finish
     | BinOp OffsetOp _ _ =>
        wp_bind_core K; etrans; [|eapply wp_offset; try fast_done]; wp_finish
     | BinOp PlusOp _ _ =>