From 580962611ba17a54b3d54eeb76acd202629d89d7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Fri, 20 Nov 2015 16:51:21 +0100
Subject: [PATCH] Step-indexed order on CMRAs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
* Remove the order from RAs, it is now defined in terms of the ⋅ operation.
* Define ownership using the step-indexed order.
* Remove the order also from DRAs and change STS accordingly. While doing
that, I changed STS to no longer use decidable token sets, which removes the
requirement of decidable equality on tokens.
---
theories/collections.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/collections.v b/theories/collections.v
index 619134db..a0bbafe6 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -297,6 +297,8 @@ Section collection.
Proof. esolve_elem_of. Qed.
Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
Proof. esolve_elem_of. Qed.
+ Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y.
+ Proof. esolve_elem_of. Qed.
Section leibniz.
Context `{!LeibnizEquiv C}.
@@ -315,6 +317,8 @@ Section collection.
Lemma difference_intersection_distr_l_L X Y Z :
(X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
+ Lemma disjoint_union_difference_L X Y : X ∩ Y = ∅ → (X ∪ Y) ∖ X = Y.
+ Proof. unfold_leibniz. apply disjoint_union_difference. Qed.
End leibniz.
Section dec.
--
GitLab