From 27baa1d5920754396d5d00e01da33f83da3849e8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 13:57:26 +0200
Subject: [PATCH] Let wp_cas_suc generate equality goal if the values are not
 convertible.

This is more consistent with wp_cas_fail.
---
 heap_lang/proofmode.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index 2889b52b7..1f6b56802 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -70,15 +70,16 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
+Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   Δ ⊢ heap_ctx N → nclose N ⊆ E →
   StripLaterEnvs Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦ v1)%I →
+  envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
+  intros; subst.
+  rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -172,6 +173,7 @@ Tactic Notation "wp_cas_suc" :=
          |done || eauto with ndisj
          |apply _
          |iAssumptionCore || fail 2 "wp_cas_suc: cannot find" l "↦ ?"
+         |try reflexivity
          |env_cbv; reflexivity
          |wp_finish]
     end) || fail "wp_cas_suc: cannot find 'CAS' in" e
-- 
GitLab