From 719c409c8c9c2b5c05f502d4b3fec3105fb544f2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Mar 2021 11:56:12 +0100
Subject: [PATCH] prove that Skip is atomic
---
theories/lang/tactics.v | 19 ++++++++++++++++++-
1 file changed, 18 insertions(+), 1 deletion(-)
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 894acff4..0887d4d7 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -157,7 +157,7 @@ Definition is_atomic (e: expr) : bool :=
Lemma is_atomic_correct e : is_atomic e → Atomic WeaklyAtomic (to_expr e).
Proof.
intros He. apply ectx_language_atomic.
- - intros σ e' σ' ef.
+ - intros σ ef e' σ'.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
@@ -202,6 +202,23 @@ Ltac solve_atomic :=
end.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
+Global Instance skip_atomic : Atomic WeaklyAtomic Skip.
+Proof.
+ apply strongly_atomic_atomic, ectx_language_atomic.
+ - inversion 1. naive_solver.
+ - apply ectxi_language_sub_redexes_are_values. intros [] * Hskip; try naive_solver.
+ + inversion Hskip. simpl. rewrite decide_left. eauto.
+ + inversion Hskip. rename select ([Lit _] = _) into Hargs.
+ assert (length [Lit LitPoison] = 1%nat) as Hlen by done. move:Hlen.
+ rewrite Hargs. rewrite app_length fmap_length /=.
+ rename select (list val) into vl. rename select (list expr) into el.
+ destruct vl; last first.
+ { simpl. intros. exfalso. lia. }
+ destruct el; last first.
+ { simpl. intros. exfalso. lia. }
+ simpl in *. intros _. inversion Hargs. eauto.
+Qed.
+
(** Substitution *)
Ltac simpl_subst :=
unfold subst_v; simpl;
--
GitLab