From 538a5d7f0d09edaa943a50b9a2bfe9d6383bc147 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 4 May 2023 17:46:42 +0200
Subject: [PATCH] Fix `tp_xchg` and resolve an admit.
---
theories/logic/proofmode/spec_tactics.v | 14 +++++++-------
theories/logic/rules.v | 6 +++---
2 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 5bba0af..7f6cca1 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -225,14 +225,14 @@ Qed.
Tactic Notation "tp_xchg" constr(j) :=
iStartProof;
- eapply (tac_tp_store j);
- [tc_solve || fail "tp_store: cannot eliminate modality in the goal"
- |solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
- |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
+ eapply (tac_tp_xchg j);
+ [tc_solve || fail "tp_xchg: cannot eliminate modality in the goal"
+ |solve_ndisj || fail "tp_xchg: cannot prove 'nclose specN ⊆ ?'"
+ |iAssumptionCore || fail "tp_xchg: cannot find '" j " ' RHS"
|tp_bind_helper
- |tc_solve || fail "tp_store: cannot convert the argument to a value"
- |iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
- |simpl; reflexivity || fail "tp_store: this should not happen"
+ |tc_solve || fail "tp_xchg: cannot convert the argument to a value"
+ |iAssumptionCore || fail "tp_xchg: cannot find '? ↦ₛ ?'"
+ |simpl; reflexivity || fail "tp_xchg: this should not happen"
|pm_reduce (* new goal *)].
(* *)
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 2d32037..374ecd8 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -195,9 +195,9 @@ Section rules.
rewrite /IntoVal. iIntros (?<-) "Hl Hlog".
iApply refines_step_r.
iIntros (k) "Hk".
- admit.
- Admitted.
-
+ tp_xchg k. iExists v. iModIntro. iFrame.
+ by iApply "Hlog".
+ Qed.
Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
nclose specN ⊆ E →
--
GitLab