Commit 58096261 authored by Robbert Krebbers's avatar Robbert Krebbers

Step-indexed order on CMRAs

* 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.
parent f1f45de3
......@@ -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.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment