From 7c5cfdbfbfcf36ddc60ff4591f6b37073baf3ec1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 23 Feb 2020 23:14:15 +0100
Subject: [PATCH] Use `TCEq` so that TC search can establish non-valueness in
 WP `step` lemmas.

---
 theories/program_logic/hoare.v      |  8 ++++----
 theories/program_logic/weakestpre.v | 10 +++++-----
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 9776e183e..a8f5850ae 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -120,7 +120,7 @@ Lemma ht_frame_r s E P Φ R e :
 Proof. iIntros "#Hwp !> [HP $]". by iApply "Hwp". Qed.
 
 Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
-  to_val e = None → E2 ⊆ E1 →
+  TCEq (to_val e) None → E2 ⊆ E1 →
   (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
   ⊢ {{ R1 ∗ P }} e @ s; E1 {{ λ v, R2 ∗ Φ v }}.
 Proof.
@@ -130,7 +130,7 @@ Proof.
 Qed.
 
 Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
-  to_val e = None → E2 ⊆ E1 →
+  TCEq (to_val e) None → E2 ⊆ E1 →
   (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ s; E2 {{ Φ }}
   ⊢ {{ P ∗ R1 }} e @ s; E1 {{ λ v, Φ v ∗ R2 }}.
 Proof.
@@ -140,7 +140,7 @@ Proof.
 Qed.
 
 Lemma ht_frame_step_l' s E P R e Φ :
-  to_val e = None →
+  TCEq (to_val e) None →
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; E {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (?) "#Hwp !> [HR HP]".
@@ -148,7 +148,7 @@ Proof.
 Qed.
 
 Lemma ht_frame_step_r' s E P Φ R e :
-  to_val e = None →
+  TCEq (to_val e) None →
   {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; E {{ v, Φ v ∗ R }}.
 Proof.
   iIntros (?) "#Hwp !> [HP HR]".
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 5bc2534b1..210cac507 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -140,7 +140,7 @@ Proof.
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
-  to_val e = None → E2 ⊆ E1 →
+  TCEq (to_val e) None → E2 ⊆ E1 →
   (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
@@ -221,24 +221,24 @@ Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, 
 Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma wp_frame_step_l s E1 E2 e Φ R :
-  to_val e = None → E2 ⊆ E1 →
+  TCEq (to_val e) None → E2 ⊆ E1 →
   (|={E1,E2}▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
   iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
 Qed.
 Lemma wp_frame_step_r s E1 E2 e Φ R :
-  to_val e = None → E2 ⊆ E1 →
+  TCEq (to_val e) None → E2 ⊆ E1 →
   WP e @ s; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
 Proof.
   rewrite [(WP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.
 Qed.
 Lemma wp_frame_step_l' s E e Φ R :
-  to_val e = None → ▷ R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
+  TCEq (to_val e) None → ▷ R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
 Proof. iIntros (?) "[??]". iApply (wp_frame_step_l s E E); try iFrame; eauto. Qed.
 Lemma wp_frame_step_r' s E e Φ R :
-  to_val e = None → WP e @ s; E {{ Φ }} ∗ ▷ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
+  TCEq (to_val e) None → WP e @ s; E {{ Φ }} ∗ ▷ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
 Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qed.
 
 Lemma wp_wand s E e Φ Ψ :
-- 
GitLab