From 393f02ede275fed39c5980d6a6bd5c98af9c9564 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Jun 2018 11:37:29 +0200
Subject: [PATCH] get rid of to_val_is_Some'

---
 theories/heap_lang/tactics.v      | 11 ++++-------
 theories/program_logic/language.v |  3 +++
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index cdb8f85a6..1efe90f58 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -138,16 +138,13 @@ Fixpoint to_val (e : expr) : option val :=
   | _ => None
   end.
 Lemma to_val_Some e v :
-  to_val e = Some v → of_val v = W.to_expr e.
+  to_val e = Some v → heap_lang.of_val v = W.to_expr e.
 Proof.
   revert v. induction e; intros; simplify_option_eq; try f_equal; auto using of_to_val.
 Qed.
 Lemma to_val_is_Some e :
-  is_Some (to_val e) → ∃ v, of_val v = to_expr e.
+  is_Some (to_val e) → ∃ v, heap_lang.of_val v = to_expr e.
 Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
-Lemma to_val_is_Some' e :
-  is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)).
-Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
 
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
@@ -202,8 +199,8 @@ Proof.
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
   - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
-    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
-      naive_solver eauto using to_val_is_Some'.
+    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//); try
+      naive_solver eauto using as_val_is_Some, to_val_is_Some.
 Qed.
 End W.
 
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 6ceddcaa3..b067bb1eb 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -170,4 +170,7 @@ Section language.
     apply TCForall_Forall, Forall_fmap, Forall_true=> v.
     rewrite /AsVal /=; eauto.
   Qed.
+  Lemma as_val_is_Some e :
+    (∃ v, of_val v = e) → is_Some (to_val e).
+  Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
 End language.
-- 
GitLab