Commit 68ee814e by Robbert Krebbers

### 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.```
parent 83c9c1c1
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!