From 7952bca415009d8690217d21967980bbd0fb2452 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Apr 2016 19:09:20 +0200
Subject: [PATCH] Make atomic a boolean predicate.

---
 heap_lang/lang.v              | 17 +++++++++--------
 heap_lang/lifting.v           |  8 ++++----
 prelude/decidable.v           |  1 +
 program_logic/ectx_language.v |  2 +-
 program_logic/language.v      |  2 +-
 tests/one_shot.v              | 13 +++++--------
 6 files changed, 21 insertions(+), 22 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 758c0dca7..19c368375 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -342,15 +342,16 @@ Inductive head_step : expr [] → state → expr [] → state → option (expr [
      head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
 
 (** Atomic expressions *)
-Definition atomic (e: expr []) : Prop :=
+Definition atomic (e: expr []) : bool :=
   match e with
-  | Alloc e => is_Some (to_val e)
-  | Load e => is_Some (to_val e)
-  | Store e1 e2 => is_Some (to_val e1) ∧ is_Some (to_val e2)
-  | CAS e0 e1 e2 => is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2)
+  | Alloc e => bool_decide (is_Some (to_val e))
+  | Load e => bool_decide (is_Some (to_val e))
+  | Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
+  | CAS e0 e1 e2 =>
+    bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
   (* Make "skip" atomic *)
-  | App (Rec _ _ (Lit _)) (Lit _) => True
-  | _ => False
+  | App (Rec _ _ (Lit _)) (Lit _) => true
+  | _ => false
   end.
 
 (** Substitution *)
@@ -449,7 +450,7 @@ Lemma val_stuck e1 σ1 e2 σ2 ef :
 Proof. destruct 1; naive_solver. Qed.
 
 Lemma atomic_not_val e : atomic e → to_val e = None.
-Proof. destruct e; naive_solver. Qed.
+Proof. by destruct e. Qed.
 
 Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
 Proof.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index bb6516166..cb2701e18 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -34,8 +34,8 @@ Proof.
   rewrite always_and_sep_l -assoc -always_and_sep_l.
   apply const_elim_l=>-[l [-> [Hl [-> ?]]]].
   rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
-  rewrite -(of_to_val (Loc l) (LocV l)) // in Hl. apply of_val_inj in Hl.
-  by subst.
+  rewrite -(of_to_val (Loc l) (LocV l)) // in Hl.
+  by apply of_val_inj in Hl as ->.
 Qed.
 
 Lemma wp_load_pst E σ l v Φ :
@@ -62,7 +62,7 @@ Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ None)
     ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; split_and?; by eauto.
+    simpl; by eauto 10.
 Qed.
 
 Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
@@ -72,7 +72,7 @@ Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
     (<[l:=v2]>σ) None) ?right_id //; last (by intros; inv_head_step; eauto);
-    simpl; split_and?; by eauto.
+    simpl; by eauto 10.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
diff --git a/prelude/decidable.v b/prelude/decidable.v
index 4dfd94a37..819749a94 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -113,6 +113,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
+Hint Resolve bool_decide_pack.
 Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
 Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
diff --git a/program_logic/ectx_language.v b/program_logic/ectx_language.v
index 2cae45d14..bbb34d489 100644
--- a/program_logic/ectx_language.v
+++ b/program_logic/ectx_language.v
@@ -9,7 +9,7 @@ Class EctxLanguage (expr val ectx state : Type) := {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  atomic : expr → Prop;
+  atomic : expr → bool;
   head_step : expr → state → expr → state → option expr → Prop;
 
   to_of_val v : to_val (of_val v) = Some v;
diff --git a/program_logic/language.v b/program_logic/language.v
index 365841026..45834b1f8 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -6,7 +6,7 @@ Structure language := Language {
   state : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  atomic : expr → Prop;
+  atomic : expr → bool;
   prim_step : expr → state → expr → state → option expr → Prop;
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v → of_val v = e;
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 44325dccd..e87d468fa 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -57,12 +57,11 @@ Proof.
   rewrite !assoc 2!forall_elim; eapply wand_apply_r'; first done.
   rewrite (always_sep_dup (_ ★ _)); apply sep_mono.
   - apply forall_intro=>n. apply: always_intro. wp_let.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
-      rewrite /= ?to_of_val; eauto 10 with I.
+    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
     rewrite (True_intro (inv _ _)) right_id.
     apply wand_intro_r; rewrite sep_or_l; apply or_elim.
     + rewrite -wp_pvs.
-      wp eapply wp_cas_suc; rewrite /= ?to_of_val; eauto with I ndisj.
+      wp eapply wp_cas_suc; eauto with I ndisj.
       rewrite (True_intro (heap_ctx _)) left_id.
       ecancel [l ↦ _]%I; apply wand_intro_l.
       rewrite (own_update); (* FIXME: canonical structures are not working *)
@@ -72,14 +71,13 @@ Proof.
       solve_sep_entails.
     + rewrite sep_exist_l; apply exist_elim=>m.
       eapply wp_cas_fail with (v':=InjRV #m) (q:=1%Qp);
-        rewrite /= ?to_of_val; eauto with I ndisj; strip_later.
+        eauto with I ndisj; strip_later.
       ecancel [l ↦ _]%I; apply wand_intro_l, sep_intro_True_r; eauto with I.
       rewrite /one_shot_inv -or_intro_r -(exist_intro m).
       solve_sep_entails.
   - apply: always_intro. wp_seq.
     wp_focus (Load (%l))%I.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
-      rewrite /= ?to_of_val; eauto 10 with I.
+    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
     apply wand_intro_r.
     trans (heap_ctx heapN ★ inv N (one_shot_inv γ l) ★ ∃ v, l ↦ v ★
       ((v = InjLV #0 ★ own γ OneShotPending) ∨
@@ -115,8 +113,7 @@ Proof.
     rewrite [(w=_ ★ _)%I]comm !assoc; apply const_elim_sep_r=>->.
     (* FIXME: why do we need to fold? *)
     wp_case; fold of_val. wp_let. wp_focus (Load (%l))%I.
-    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l));
-      rewrite /= ?to_of_val; eauto 10 with I.
+    eapply (wp_inv_timeless _ _ _ (one_shot_inv γ l)); eauto 10 with I.
     rewrite (True_intro (inv _ _)) right_id.
     apply wand_intro_r; rewrite sep_or_l; apply or_elim.
     + rewrite (True_intro (heap_ctx _)) (True_intro (l ↦ _)) !left_id.
-- 
GitLab