diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v index 73b4d0b99f6ad0501fa45fac4a69e580df99ab0e..814450518e9f4448c48ac4fc91059ca9d073b333 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 638ceca69c54f5d5ef1e3e47aa48321e90a5b8c4..28410330e4f85c70b778fdc02f0f038367e3c9f7 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.