From c399acafab4c3990301e6c366fd42518af0d6e4c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Apr 2016 18:05:23 +0200
Subject: [PATCH] Some tweaks.

---
 heap_lang/lifting.v      | 6 ++----
 program_logic/language.v | 2 ++
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index e3122bfd9..1185095ab 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -36,10 +36,8 @@ Proof.
   iIntros  "[HP HΦ]". iFrame "HP". iNext.
   iIntros {v2 σ2 ef} "[% HP]".
   (* FIXME: I should not have to refer to "H0". *)
-  destruct H0 as (l & -> & ? & -> & ?).
-  rewrite -(of_to_val (Loc l) (LocV l)) // in H0.
-  apply of_val_inj in H0 as ->.
-  simpl. iSplitL; last done. iApply "HΦ" {l}. iSplit; done.
+  destruct H0 as (l & -> & [= <-]%of_to_val_flip & -> & ?); simpl.
+  iSplit; last done. iApply "HΦ"; by iSplit.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :
diff --git a/program_logic/language.v b/program_logic/language.v
index 45834b1f8..d361644f2 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -46,6 +46,8 @@ Section language.
        prim_step e1 σ1 e2 σ2 ef →
        step ρ1 ρ2.
 
+  Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
+  Proof. intros <-. by rewrite to_of_val. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
   Lemma atomic_of_val v : ¬atomic (of_val v).
-- 
GitLab