From 346ca437bee0d101c88043609b67894ae67a9d75 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Sun, 11 Apr 2021 09:33:14 +0200
Subject: [PATCH] Add CoreId instances for auth and view
---
iris/algebra/auth.v | 2 ++
iris/algebra/view.v | 4 +++-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index bc52dd8e6..5a0aca789 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -132,6 +132,8 @@ Section auth.
Proof. apply view_frag_mono. Qed.
Lemma auth_frag_core a : core (â—¯ a) = â—¯ (core a).
Proof. apply view_frag_core. Qed.
+ Global Instance auth_auth_core_id a : CoreId (â—â–¡ a).
+ Proof. rewrite /auth_auth. apply _. Qed.
Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. rewrite /auth_frag. apply _. Qed.
Global Instance auth_frag_is_op a b1 b2 :
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 672aa04da..0d7106419 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -287,8 +287,10 @@ Section cmra.
Proof. intros [c ->]. rewrite view_frag_op. apply cmra_included_l. Qed.
Lemma view_frag_core b : core (â—¯V b) = â—¯V (core b).
Proof. done. Qed.
+ Global Instance view_auth_core_id a : CoreId (â—Vâ–¡ a).
+ Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
Global Instance view_frag_core_id b : CoreId b → CoreId (◯V b).
- Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
+ Proof. do 2 constructor; simpl; auto. apply: core_id_core. Qed.
Global Instance view_frag_is_op b b1 b2 :
IsOp b b1 b2 → IsOp' (◯V b) (◯V b1) (◯V b2).
Proof. done. Qed.
--
GitLab