Commit 30cab675 authored by Ralf Jung's avatar Ralf Jung

use m as prefix for things of option type

parent 0618ab9a
......@@ -12,6 +12,7 @@ j
k
l
m : iGst = ghost state
m* : prefix for option
n
o
p
......
......@@ -843,9 +843,9 @@ Proof. by rewrite /AddModal !embed_bupd. Qed.
(* ElimInv *)
Global Instance elim_inv_acc_without_close {X : Type}
φ Pinv Pin
M1 M2 α β γ Q (Q' : X PROP) :
IntoAcc (X:=X) Pinv φ Pin M1 M2 α β γ
ElimAcc (X:=X) M1 M2 α β γ Q Q'
M1 M2 α β 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'.
Proof.
rewrite /ElimAcc /IntoAcc /ElimInv.
......@@ -857,10 +857,10 @@ Qed.
Global Instance elim_inv_acc_with_close {X : Type}
φ Pinv Pin
M1 M2 α β γ Q Q' :
IntoAcc Pinv φ Pin M1 M2 α β γ
M1 M2 α β mγ Q Q' :
IntoAcc Pinv φ Pin M1 M2 α β mγ
( R, ElimModal True false false (M1 R) R Q Q')
ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x - M2 (proofmode.base.from_option id emp (γ x))))%I
ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x - M2 (proofmode.base.from_option id emp (mγ x))))%I
Q (λ _, Q').
Proof.
rewrite /ElimAcc /IntoAcc /ElimInv.
......
......@@ -552,11 +552,11 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
Proof. by rewrite /AddModal !embed_fupd. Qed.
(* ElimAcc *)
Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
Global Instance elim_acc_vs `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
(* FIXME: Why %I? ElimAcc sets the right scopes! *)
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β γ
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
(|={E1,E}=> Q)
(λ x, |={E2}=> (β x (coq_tactics.maybe_wand (γ x) (|={E1,E}=> Q))))%I.
(λ x, |={E2}=> (β x (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q))))%I.
Proof.
rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
......
......@@ -519,8 +519,8 @@ Hint Mode IntoInv + ! - : typeclass_instances.
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 {PROP : bi} {X : Type} (M1 M2 : PROP PROP)
(α β : X PROP) (γ : X option PROP) : PROP :=
M1 ( x, α x (β x - M2 (default emp (γ x) id)))%I.
(α β : X PROP) (mγ : X option PROP) : PROP :=
M1 ( x, α x (β x - M2 (default emp (mγ x) id)))%I.
(* Typeclass for assertions around which accessors can be elliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ]
......@@ -529,9 +529,9 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
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)
(α β : X PROP) (γ : X option PROP)
(α β : X PROP) (mγ : X option PROP)
(Q : PROP) (Q' : X PROP) :=
elim_acc : (( x, α x - Q' x) - accessor M1 M2 α β γ - Q).
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 {_}.
Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
......@@ -547,8 +547,8 @@ Hint Mode ElimAcc + ! ! ! ! ! ! ! - : typeclass_instances.
some evars though, e.g. for the masks)
*)
Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
(M1 M2 : PROP PROP) (α β : X PROP) (γ : X option PROP) :=
into_acc : φ Pacc - Pin - accessor M1 M2 α β γ.
(M1 M2 : PROP PROP) (α β : X PROP) (mγ : X option PROP) :=
into_acc : φ Pacc - Pin - accessor M1 M2 α β mγ.
Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
......@@ -574,9 +574,9 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
TODO: Add support for a binder (like accessors have it).
*)
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X PROP) (Pclose : option (X PROP))
(Pinv Pin : PROP) (Pout : X PROP) (mPclose : option (X PROP))
(Q : PROP) (Q' : X PROP) :=
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) Pclose id) x - Q' x) Q.
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) mPclose id) x - Q' x) Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
......
......@@ -136,8 +136,8 @@ Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
in
match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
Definition maybe_wand {PROP : bi} (P : option PROP) (Q : PROP) : PROP :=
match P with
Definition maybe_wand {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
match mP with
| None => Q
| Some P => (P - Q)%I
end.
......@@ -444,9 +444,9 @@ Proof.
rewrite /= assoc (comm _ P0 P) IH //.
Qed.
Lemma maybe_wand_sound (P : option PROP) Q :
maybe_wand P Q (default emp P id - Q).
Proof. destruct P; simpl; first done. rewrite emp_wand //. Qed.
Lemma maybe_wand_sound (mP : option PROP) Q :
maybe_wand mP Q (default emp mP id - Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
Global Instance envs_Forall2_refl (R : relation PROP) :
Reflexive R Reflexive (envs_Forall2 R).
......
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