Commit b71c6f44 authored by Ralf Jung's avatar Ralf Jung

have two instances for ElimInv and MakeEmbed, instead of one horrible one

parent 3627c45f
......@@ -486,18 +486,21 @@ Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 𝓟 𝓟' Q i :
AddModal 𝓟 𝓟' (|={E1,E2}=> Q i) AddModal 𝓟 𝓟' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
Global Instance elim_inv_embed φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out 𝓟close (Q i) (Q' i))
Global Instance elim_inv_embed_with_close φ 𝓟inv 𝓟in 𝓟out 𝓟close Pin Pout Pclose Q Q' :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out (Some 𝓟close) (Q i) (Q' i))
MakeEmbed 𝓟in Pin MakeEmbed 𝓟out Pout MakeEmbed 𝓟close Pclose
ElimInv φ ⎡𝓟inv Pin Pout (Some Pclose) Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <- <- <- ?. iStartProof PROP.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Qed.
Global Instance elim_inv_embed_without_close φ 𝓟inv 𝓟in 𝓟out Pin Pout Q Q' :
( i, ElimInv φ 𝓟inv 𝓟in 𝓟out None (Q i) (Q' i))
MakeEmbed 𝓟in Pin MakeEmbed 𝓟out Pout
match 𝓟close, Pclose with
| Some 𝓟close, Some Pclose => MakeEmbed 𝓟close Pclose
| None, None => True
| _, _ => False
end
ElimInv φ ⎡𝓟inv Pin Pout Pclose Q Q'.
ElimInv φ ⎡𝓟inv Pin Pout None Q Q'.
Proof.
rewrite /MakeEmbed /ElimInv=>H <- <- Hclose ?. iStartProof PROP.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?".
destruct 𝓟close; destruct Pclose; try rewrite -Hclose; iApply "HQ'"; done.
rewrite /MakeEmbed /ElimInv=>H <- <- ?. iStartProof PROP.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Qed.
End sbi.
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