From d30d44672cd9241f9b881b6df6d66a7138e16654 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Wed, 24 Aug 2022 17:40:21 +0200
Subject: [PATCH] =?UTF-8?q?Ah,=20the=20recursive=20TryMerge=20=E2=8A=A0=20?=
=?UTF-8?q?instance=20was=20missing.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
diaframe/steps/introduce_hyp.v | 15 ---------------
diaframe/steps/solve_instances.v | 21 +++++++++++++++++++--
2 files changed, 19 insertions(+), 17 deletions(-)
diff --git a/diaframe/steps/introduce_hyp.v b/diaframe/steps/introduce_hyp.v
index 9c8f388d..f0bf49f3 100644
--- a/diaframe/steps/introduce_hyp.v
+++ b/diaframe/steps/introduce_hyp.v
@@ -295,21 +295,6 @@ Section coq_tactics.
rewrite HΔ //.
Qed.
- Global Instance mergable_persist_from_box P p P2 P3 :
- MergePersist P p P2 P3 →
- MergePersist (□ P)%I p P2 P3 | 5.
- Proof.
- rewrite /MergePersist => <-.
- iIntros "[#$ $]".
- Qed.
- Global Instance mergable_consume_from_box P p P2 P3 :
- MergeConsume P p P2 P3 →
- MergeConsume (□ P)%I p P2 P3 | 5.
- Proof.
- rewrite /MergeConsume => <-.
- iIntros "[#$ $]".
- Qed.
-
Lemma tac_introduce_hyp_not_mergable j Δ P1 a P1' R :
TCIf (TCAnd (IntoPersistent false P1 P1') (Affine P1))
(TCEq a true) (TCAnd (TCEq a false) (TCEq P1' P1)) →
diff --git a/diaframe/steps/solve_instances.v b/diaframe/steps/solve_instances.v
index 48f3ee40..f8c38ed8 100644
--- a/diaframe/steps/solve_instances.v
+++ b/diaframe/steps/solve_instances.v
@@ -213,17 +213,34 @@ End drop_modal_instances.
Section misc.
Context {PROP : bi}.
+ Implicit Types P Q : PROP.
(* TODO: where to put this? *)
- Global Instance exclusive_prop_try_merge (Q : PROP) :
+ Global Instance exclusive_prop_try_merge Q :
ExclusiveProp Q → TryMerge Q.
Proof. exact (λ _, I). Qed.
- Global Instance exclusive_prop_merge_false (Q : PROP) p :
+ Global Instance exclusive_prop_merge_false Q p :
ExclusiveProp Q →
MergeConsume Q p Q False%I.
Proof.
rewrite /ExclusiveProp /MergeConsume bi.intuitionistically_if_elim //.
Qed.
+
+ Global Instance mergable_persist_from_box P p P2 P3 :
+ MergePersist P p P2 P3 →
+ MergePersist (□ P)%I p P2 P3 | 5.
+ Proof.
+ rewrite /MergePersist => <-.
+ iIntros "[#$ $]".
+ Qed.
+ Global Instance mergable_consume_from_box P p P2 P3 :
+ MergeConsume P p P2 P3 →
+ MergeConsume (□ P)%I p P2 P3 | 5.
+ Proof.
+ rewrite /MergeConsume => <-.
+ iIntros "[#$ $]".
+ Qed.
+ Global Instance try_merge_from_box P : TryMerge P → TryMerge (□ P)%I := id.
End misc.
--
GitLab