From 43f44e74105d733afc3fa6b826db7664623fa45a Mon Sep 17 00:00:00 2001
From: Janggun Lee <leesisi123@naver.com>
Date: Mon, 23 Sep 2024 23:59:59 +0900
Subject: [PATCH] Add missing typeclasses for twp.
---
CHANGELOG.md | 5 +++++
iris/program_logic/total_weakestpre.v | 31 +++++++++++++++++++++++++++
2 files changed, 36 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 286da8513..ea1c2dced 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -38,6 +38,11 @@ lemma.
wrappers of instances `big_sep*_mono'` for `flip (⊢)` instead of `(⊢)`. (by
Yusuke Matsushita)
+**Changes in `program_logic`:**
+
+* Add some missing proofmode instances for total weakest preconditions. (by
+ Janggun Lee)
+
**Changes in `heap_lang`:**
* Make `wp_cmpxchg_fail` work when the points-to is in the persistent context.
diff --git a/iris/program_logic/total_weakestpre.v b/iris/program_logic/total_weakestpre.v
index 1cbb361bc..6e7c972b3 100644
--- a/iris/program_logic/total_weakestpre.v
+++ b/iris/program_logic/total_weakestpre.v
@@ -343,6 +343,17 @@ Section proofmode_classes.
by rewrite /ElimModal intuitionistically_if_elim
fupd_frame_r wand_elim_r fupd_twp.
Qed.
+ (** Error message instance for non-mask-changing view shifts.
+ Also uses a slightly different error: we cannot apply [fupd_mask_subseteq]
+ if [e] is not atomic, so we tell the user to first add a leading [fupd]
+ and then change the mask of that. *)
+ Global Instance elim_modal_fupd_twp_wrong_mask p s E1 E2 e P Φ :
+ ElimModal
+ (pm_error "Goal and eliminated modality must have the same mask.
+Use [iApply fupd_twp; iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
+ p false
+ (|={E2}=> P) False (WP e @ s; E1 [{ Φ }]) False | 100.
+ Proof. intros []. Qed.
Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
ElimModal (Atomic (stuckness_to_atomicity s) e) p false
@@ -352,8 +363,28 @@ Section proofmode_classes.
intros ?. by rewrite intuitionistically_if_elim
fupd_frame_r wand_elim_r twp_atomic.
Qed.
+ (** Error message instance for mask-changing view shifts. *)
+ Global Instance elim_modal_fupd_twp_atomic_wrong_mask p s E1 E2 E2' e P Φ :
+ ElimModal
+ (pm_error "Goal and eliminated modality must have the same mask.
+ Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
+ p false
+ (|={E2,E2'}=> P) False
+ (WP e @ s; E1 [{ Φ }]) False | 200.
+ Proof. intros []. Qed.
Global Instance add_modal_fupd_twp s E e P Φ :
AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+
+ Global Instance elim_acc_twp_atomic {X} E1 E2 α β γ e s Φ :
+ ElimAcc (X:=X) (Atomic (stuckness_to_atomicity s) e)
+ (fupd E1 E2) (fupd E2 E1)
+ α β γ (WP e @ s; E1 [{ Φ }])
+ (λ x, WP e @ s; E2 [{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }])%I | 100.
+ Proof.
+ iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+ iApply (twp_wand with "(Hinner Hα)").
+ iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
+ Qed.
End proofmode_classes.
--
GitLab