From 68ee814eab1f731557d17d194887fe10f44e37bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Oct 2017 10:21:32 +0200
Subject: [PATCH] Weaken the associativity axiom of the Dra class.

Now, associativity needs only to be established in case the elements are
valid and their compositions are defined. This is very much like the notion
of separation algebras I had in my PhD thesis (Def 4.2.1). The Dra to Ra
construction still easily works out.
---
 theories/algebra/dra.v | 8 +++++---
 theories/algebra/sts.v | 2 +-
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index 73b4d0b99..814450518 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -12,7 +12,8 @@ Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
   mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
   mixin_dra_core_valid x : ✓ x → ✓ core x;
   (* monoid *)
-  mixin_dra_assoc : Assoc (≡) (⋅);
+  mixin_dra_assoc x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z;
   mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
   mixin_dra_disjoint_move_l x y z :
     ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
@@ -62,7 +63,8 @@ Section dra_mixin.
   Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
   Lemma dra_core_valid x : ✓ x → ✓ core x.
   Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
-  Global Instance dra_assoc : Assoc (≡) (@op A _).
+  Lemma dra_assoc x y z :
+    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z.
   Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
   Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
   Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
@@ -161,7 +163,7 @@ Proof.
   - intros ?? [??]; naive_solver.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
       [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |intros; by rewrite assoc].
+      |intuition eauto using dra_assoc, dra_disjoint_rl].
   - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
   - intros [x px ?]; split;
       naive_solver eauto using dra_core_l, dra_core_disjoint_l.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index 638ceca69..28410330e 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -244,7 +244,7 @@ Proof.
       match goal with H : closed _ _ |- _ => destruct H end; set_solver.
   - intros []; naive_solver eauto using closed_up, closed_up_set,
       elem_of_up, elem_of_up_set with sts.
-  - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
+  - intros [] [] [] _ _ _ _ _; constructor; rewrite ?assoc; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
   - destruct 4; inversion_clear 1; constructor; auto with sts.
   - destruct 1; constructor; auto with sts.
-- 
GitLab