From 441ae9dde232275b78bc3147da05f6fb1985a89c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 5 Mar 2018 17:36:13 +0100
Subject: [PATCH] prove admitted lemma atomic_correct

---
 theories/tactics.v | 40 +++++++++++++++++++---------------------
 1 file changed, 19 insertions(+), 21 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 3f267492..017818b0 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -219,29 +219,27 @@ Definition atomic0 (e : expr0) :=
   end.
 Definition atomic (e : expr) := atomic0 (e.1).
 
-Lemma atomic_correct e π :
+Lemma atomic_correct e π s :
   atomic0 e  →
-  Atomic WeaklyAtomic ((to_expr' e, π) : language.expr ra_lang).
+  Atomic s ((to_expr' e, π) : language.expr ra_lang).
 Proof.
-  (* intros He. *)
-  (* - inversion H; clear H. *)
-  (*   apply ectxi_language_sub_redexes_are_values in H0. *)
-  (*   simplify_eq. cbn. rewrite /ra_lang.to_val /=. *)
-  (*   inversion H0. *)
-  (* - intros σ [e' ρ'] σ' ef. cbn. unfold ra_lang.to_val. move => STEP. *)
-  (*   apply language.val_irreducible. *)
-  (*   apply/fmap_is_Some. *)
-  (*   destruct e; simpl; try done; repeat (case_match; try done); *)
-  (*   inversion STEP; (inversion BaseStep || inversion ExprStep); rewrite ?to_of_val; eauto. subst. *)
-  (*   unfold base.subst'; repeat (case_match || contradiction || simplify_eq/=); eauto. *)
-  (* - apply ectxi_language_sub_redexes_are_values => /= Ki e' Hfill. *)
-  (*   apply/fmap_is_Some. revert He. inversion Hfill as [Hfill']; subst; clear Hfill. simpl in *. *)
-  (*   destruct e; simpl; try done; repeat (case_match; try done); *)
-  (*   rewrite ?bool_decide_spec; *)
-  (*   destruct Ki; inversion Hfill'; subst; clear Hfill'; *)
-  (*   try naive_solver eauto using to_val0_is_Some. *)
-  (*   unfold base.to_val. case_match; first by eauto. by move/bool_decide_spec: (n) => //=. *)
-Admitted.
+  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/=;
+      match goal with
+        H : base.head_step _ _ |- _ => inversion H; simplify_eq/=
+      | H : step _ _ _ _ _ |- _  => inversion H; simplify_eq/=
+      end;
+      rewrite ?to_of_val; eauto.
+      unfold base.subst'; repeat (simplify_eq/=; case_match=>//); eauto.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki [e' π'] /= [= Hfill ?].
+    cut (is_Some (base.to_val e')).
+    { intros [v Hv]. eexists. unfold ra_lang.to_val. simpl. rewrite Hv //. }
+    clear dependent π π'.
+    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
+      naive_solver eauto using to_val0_is_Some.
+Qed.
 End W.
 
 Ltac solve_closed :=
-- 
GitLab