From b71c6f4444b64c87cd3bcf1f390b219f8384e1f8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 27 Apr 2018 10:53:07 +0200
Subject: [PATCH] have two instances for ElimInv and MakeEmbed, instead of one
horrible one
---
theories/proofmode/monpred.v | 25 ++++++++++++++-----------
1 file changed, 14 insertions(+), 11 deletions(-)
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 6820522f6..87a9466b3 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -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.
--
GitLab