From 94922d09c7029ce8c21aa4b32472b240a82f0970 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Dec 2017 15:55:02 +0100
Subject: [PATCH] make strongly_atomic_atomic more convenient

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

diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 5cafc8f7b..1789ca570 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -195,9 +195,7 @@ Definition is_atomic (e : expr) :=
   end.
 Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
-  enough (is_atomic e → Atomic StronglyAtomic (to_expr e)).
-  { destruct s; auto using strongly_atomic_atomic. }
-  intros He. apply ectx_language_atomic.
+  intros He. apply strongly_atomic_atomic, ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 26f813c5f..707f9c671 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -109,9 +109,9 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-  Lemma strongly_atomic_atomic e :
-    Atomic StronglyAtomic e → Atomic WeaklyAtomic e.
-  Proof. unfold Atomic. eauto using val_irreducible. Qed.
+  Lemma strongly_atomic_atomic e a :
+    Atomic StronglyAtomic e → Atomic a e.
+  Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
-- 
GitLab