Commit 146d90b0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Thread `Atomic` side-condition through `ElimModal`, `ElimAcc` and `ElimInv`.

This makes sure that when trying to open an invariant or to eliminate a mask-changing
update around a non-atomic WP that it doesn't fail with "cannot eliminate modality",
but instead gives an side-condition `Atomic ...` informing the user what's going on.

Unlike the class `ElimModal` and `ElimInv`, the class `ElimAcc` was not yet equipped
with a Coq side-condition. This commit adds such a side-condition.
parent fbe20e31
......@@ -319,17 +319,16 @@ Section lemmas.
(* This lets you open invariants etc. when the goal is an atomic accessor. *)
Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X PROP) γ' α β Pas Φ :
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α' β' γ'
(atomic_acc E1 Ei α Pas β Φ)
(λ x', atomic_acc E2 Ei α (β' x' (γ' x' -? Pas))%I β
(λ.. x y, β' x' (γ' x' -? Φ x y))
)%I.
Proof.
rewrite /ElimAcc.
(* FIXME: Is there any way to prevent maybe_wand from unfolding?
It gets unfolded by env_cbv in the proofmode, ideally we'd like that
to happen only if one argument is a constructor. *)
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x') "[Hα' Hclose]".
iMod ("Hinner" with "Hα'") as (x) "[Hα Hclose']".
iMod (fupd_intro_mask') as "Hclose''"; last iModIntro; first done.
iExists x. iFrame. iSplitWith "Hclose'".
......
......@@ -292,11 +292,11 @@ Section proofmode_classes.
Qed.
Global Instance elim_modal_fupd_twp_atomic p s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal True p false (|={E1,E2}=> P) P
(WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
ElimModal (Atomic (stuckness_to_atomicity s) e) p false
(|={E1,E2}=> P) P
(WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I | 100.
Proof.
intros. by rewrite /ElimModal intuitionistically_if_elim
intros ?. by rewrite intuitionistically_if_elim
fupd_frame_r wand_elim_r twp_atomic.
Qed.
......
......@@ -288,11 +288,11 @@ Section proofmode_classes.
Qed.
Global Instance elim_modal_fupd_wp_atomic p s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal True p false (|={E1,E2}=> P) P
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
ElimModal (Atomic (stuckness_to_atomicity s) e) p false
(|={E1,E2}=> P) P
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof.
intros. by rewrite /ElimModal intuitionistically_if_elim
intros ?. by rewrite intuitionistically_if_elim
fupd_frame_r wand_elim_r wp_atomic.
Qed.
......@@ -300,25 +300,23 @@ Section proofmode_classes.
AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
Atomic (stuckness_to_atomicity s) e
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
Global Instance elim_acc_wp_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.
(λ x, WP e @ s; E2 {{ v, |={E2}=> β x (γ x -? Φ v) }})%I | 100.
Proof.
intros ?. rewrite /ElimAcc.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply (wp_wand with "(Hinner Hα)").
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
ElimAcc (X:=X) (fupd E E) (fupd E E)
ElimAcc (X:=X) True (fupd E E) (fupd E E)
α β γ (WP e @ s; E {{ Φ }})
(λ x, WP e @ s; E {{ v, |={E}=> β x (γ x -? Φ v) }})%I.
Proof.
rewrite /ElimAcc.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply wp_fupd.
iApply (wp_wand with "(Hinner Hα)").
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
......
......@@ -968,14 +968,14 @@ Proof. rewrite /AddModal bi_tforall_forall. apply add_modal_forall. Qed.
(** ElimInv *)
Global Instance elim_inv_acc_without_close {X : Type}
φ Pinv Pin (M1 M2 : PROP PROP) α β mγ Q (Q' : X PROP) :
IntoAcc (X:=X) Pinv φ Pin M1 M2 α β mγ
ElimAcc (X:=X) M1 M2 α β mγ Q Q'
ElimInv φ Pinv Pin α None Q Q'.
φ1 φ2 Pinv Pin (M1 M2 : PROP PROP) α β mγ Q (Q' : X PROP) :
IntoAcc (X:=X) Pinv φ1 Pin M1 M2 α β mγ
ElimAcc (X:=X) φ2 M1 M2 α β mγ Q Q'
ElimInv (φ1 φ2) Pinv Pin α None Q Q'.
Proof.
rewrite /ElimAcc /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iApply (Helim with "[Hcont]").
iIntros (Hacc Helim [??]) "(Hinv & Hin & Hcont)".
iApply (Helim with "[Hcont]"); first done.
- iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
- iApply (Hacc with "Hinv Hin"). done.
Qed.
......
......@@ -170,12 +170,11 @@ Global Instance add_modal_fupd `{!BiFUpd PROP} E1 E2 P Q :
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
Global Instance elim_acc_fupd `{!BiFUpd PROP} {X} E1 E2 E α β mγ Q :
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
ElimAcc (X:=X) True (fupd E1 E2) (fupd E2 E1) α β mγ
(|={E1,E}=> Q)
(λ x, |={E2}=> β x (mγ x -? |={E1,E}=> Q))%I.
Proof.
rewrite /ElimAcc.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iIntros (?) "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
Qed.
......
......@@ -523,17 +523,18 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
(* Typeclass for assertions around which accessors can be eliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ]
Outputs: [Q']
Outputs: [Q'], [φ]
Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
into [Q'] with a new assumption [α x]. *)
Class ElimAcc {PROP : bi} {X : Type} (M1 M2 : PROP PROP)
into [Q'] with a new assumption [α x], where [φ] is a side-condition at the
Cow level that needs to hold. *)
Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP PROP)
(α β : X PROP) (mγ : X option PROP)
(Q : PROP) (Q' : X PROP) :=
elim_acc : (( x, α x - Q' x) - accessor M1 M2 α β mγ - Q).
Arguments ElimAcc {_} {_} _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_acc {_} {_} _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
elim_acc : φ (( x, α x - Q' x) - accessor M1 M2 α β mγ - Q).
Arguments ElimAcc {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_acc {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
(* Turn [P] into an accessor.
Inputs:
......
......@@ -24,10 +24,10 @@ performance and horrible error messages, so we wrap it in a [once]. *)
Ltac iSolveTC :=
solve [once (typeclasses eauto)].
(** Tactic used for solving side-conditions arising from TC resolution in iMod
and iInv. *)
(** Tactic used for solving side-conditions arising from TC resolution in [iMod]
and [iInv]. *)
Ltac iSolveSideCondition :=
split_and?; try solve [ fast_done | solve_ndisj ].
split_and?; try solve [ fast_done | solve_ndisj | iSolveTC ].
(** Used for printing [string]s and [ident]s. *)
Ltac pretty_ident H :=
......
......@@ -569,26 +569,26 @@ Global Instance elim_modal_at_fupd_hyp `{BiFUpd PROP} φ p p' E1 E2 P 𝓟 𝓟'
ElimModal φ p p' ((|={E1,E2}=> P) i) 𝓟' 𝓠 𝓠'.
Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
Global Instance elim_acc_at_None `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' P P'x i :
Global Instance elim_acc_at_None `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' P P'x i :
( x, MakeEmbed (α x) (α' x)) ( x, MakeEmbed (β x) (β' x))
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ _, None) P P'x
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ _, None) (P i) (λ x, P'x x i).
Proof.
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA) "Hinner Hacc".
iApply (HEA with "[Hinner]").
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ HEA ?) "Hinner Hacc".
iApply (HEA with "[Hinner]"); first done.
- iIntros (x). iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
- iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
rewrite -Hα -Hβ. iFrame. iIntros (? _) "Hβ". by iApply "Hclose".
Qed.
Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
Global Instance elim_acc_at_Some `{BiFUpd PROP} {X} φ E1 E2 E3 E4 α α' β β' γ γ' P P'x i :
( x, MakeEmbed (α x) (α' x))
( x, MakeEmbed (β x) (β' x))
( x, MakeEmbed (γ x) (γ' x))
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x
ElimAcc (X:=X) (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α' β' (λ x, Some (γ' x)) P P'x
ElimAcc (X:=X) φ (fupd E1 E2) (fupd E3 E4) α β (λ x, Some (γ x)) (P i) (λ x, P'x x i).
Proof.
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA) "Hinner Hacc".
iApply (HEA with "[Hinner]").
rewrite /ElimAcc /MakeEmbed. iIntros (Hα Hβ Hγ HEA ?) "Hinner Hacc".
iApply (HEA with "[Hinner]"); first done.
- iIntros (x). iSpecialize ("Hinner" $! x). rewrite -Hα. by iIntros (? <-).
- iMod "Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]". iModIntro. iExists x.
rewrite -Hα -Hβ -Hγ. iFrame. iIntros (? _) "Hβ /=". by iApply "Hclose".
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment