Commit 42da9a0b authored by Ralf Jung's avatar Ralf Jung

rename AccElim -> ElimAcc

parent dc47e022
......@@ -405,22 +405,22 @@ 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 acc_elim_wp {X} E1 E2 α β γ e s Φ :
Global Instance elim_acc_wp {X} E1 E2 α β γ e s Φ :
Atomic (stuckness_to_atomicity s) e
AccElim (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
ElimAcc (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
(λ x, WP e @ s; E2 {{ v, |={E2}=> β x coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Proof.
intros ?. rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
Global Instance acc_elim_wp_nonatomic {X} E α β γ e s Φ :
AccElim (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
ElimAcc (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
(λ x, WP e @ s; E {{ v, |={E}=> β x coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Proof.
rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply wp_fupd.
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
......
......@@ -551,14 +551,14 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
AddModal P P' (|={E1,E2}=> Q)%I AddModal P P' |={E1,E2}=> Q.
Proof. by rewrite /AddModal !embed_fupd. Qed.
(* AccElim *)
Global Instance acc_elim_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
(* FIXME: Why %I? AccElim sets the right scopes! *)
AccElim (X:=X) E1 E2 α β γ
(* ElimAcc *)
Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
(* FIXME: Why %I? ElimAcc sets the right scopes! *)
ElimAcc (X:=X) E1 E2 α β γ
(|={E1,E}=> Q)
(λ x, |={E2}=> (β x (coq_tactics.maybe_wand (γ x) (|={E1,E}=> Q))))%I.
Proof.
rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
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".
......@@ -573,10 +573,10 @@ Global Instance elim_inv_acc_without_close `{BiFUpd PROP} {X : Type}
φ Pinv Pin
E1 E2 α β γ Q (Q' : X PROP) :
IntoAcc (X:=X) Pinv φ Pin E1 E2 α β γ
AccElim (X:=X) E1 E2 α β γ Q Q'
ElimAcc (X:=X) E1 E2 α β γ Q Q'
ElimInv φ Pinv Pin α None Q Q'.
Proof.
rewrite /AccElim /IntoAcc /ElimInv.
rewrite /ElimAcc /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iApply (Helim with "[Hcont]").
- iIntros (x) "Hα". iApply "Hcont". iSplitL; done.
......@@ -591,7 +591,7 @@ Global Instance elim_inv_acc_with_close `{BiFUpd PROP} {X : Type}
ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x ={E2,E1}= default emp (γ x) id))%I
Q (λ _, Q').
Proof.
rewrite /AccElim /IntoAcc /ElimInv.
rewrite /ElimAcc /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iMod (Hacc with "Hinv Hin") as (x) "[Hα Hclose]"; first done.
iApply "Hcont". simpl. iSplitL "Hα"; done.
......
......@@ -516,7 +516,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
(** Accessors.
This definition only exists for the purpose of the proof mode; a truly
usable and general form would use telescopes and also allow binders for the
closing view shift. [γ] is an [option] to make it easy for AccElim
closing view shift. [γ] is an [option] to make it easy for ElimAcc
instances to recognize the [emp] case and make it look nicer. *)
Definition accessor `{BiFUpd PROP} {X : Type} (E1 E2 : coPset)
(α β : X PROP) (γ : X option PROP) : PROP :=
......@@ -529,12 +529,12 @@ Definition accessor `{BiFUpd PROP} {X : Type} (E1 E2 : coPset)
Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
into [Q'] with a new assumption [α x]. *)
Class AccElim `{BiFUpd PROP} {X : Type} E1 E2 (α β : X PROP) (γ : X option PROP)
Class ElimAcc `{BiFUpd PROP} {X : Type} E1 E2 (α β : X PROP) (γ : X option PROP)
(Q : PROP) (Q' : X PROP) :=
acc_elim : (( x, α x - Q' x) - accessor E1 E2 α β γ - Q).
Arguments AccElim {_} {_} {_} _ _ _%I _%I _%I _%I : simpl never.
Arguments acc_elim {_} {_} {_} _ _ _%I _%I _%I _%I {_}.
Hint Mode AccElim + + ! - - ! ! ! ! - : typeclass_instances.
elim_acc : (( x, α x - Q' x) - accessor E1 E2 α β γ - Q).
Arguments ElimAcc {_} {_} {_} _ _ _%I _%I _%I _%I : simpl never.
Arguments elim_acc {_} {_} {_} _ _ _%I _%I _%I _%I {_}.
Hint Mode ElimAcc + + ! - - ! ! ! ! - : typeclass_instances.
(* Turn [P] into an accessor.
Inputs:
......@@ -566,7 +566,7 @@ Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
- [Q'] is the transformed goal that must be proved after opening the invariant.
Most users will never want to instantiate this; there is a general instance
based on [AccElim] and [IntoAcc]. However, logics like Iris 2 that support
based on [ElimAcc] and [IntoAcc]. However, logics like Iris 2 that support
invariants but not mask-changing fancy updates can use this class directly to
still benefit from [iInv].
......
Markdown is supported
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