Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

b24d969a · Ralf Jung · ec5e106d · 6950fa1d · b24d969a · b24d969a
Commit b24d969a authored Feb 12, 2016 by Ralf Jung
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,8 +67,9 @@ program_logic/tests.v
 program_logic/auth.v
 program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
-heap_lang/heap_lang_tactics.v
+heap_lang/tactics.v
 heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
 heap_lang/tests.v
+heap_lang/substitution.v
--- a/algebra/agree.v
+++ b/algebra/agree.v
@@ -59,9 +59,9 @@ Program Instance agree_op : Op (agree A) := λ x y,
 Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
 Instance agree_unit : Unit (agree A) := id.
 Instance agree_minus : Minus (agree A) := λ x y, x.
-Instance: Commutative (≡) (@op (agree A) _).
+Instance: Comm (≡) (@op (agree A) _).
 Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
-Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x.
+Definition agree_idemp (x : agree A) : x ⋅ x ≡ x.
 Proof. split; naive_solver. Qed.
 Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
 Proof.
@@ -79,18 +79,18 @@ Proof.
      eauto using agree_valid_le.
 Qed.
 Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
-Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
+Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
 Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
-Instance: Associative (≡) (@op (agree A) _).
+Instance: Assoc (≡) (@op (agree A) _).
 Proof.
  intros x y z; split; simpl; intuition;
    repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
-    by cofe_subst; rewrite !agree_idempotent.
+    by cofe_subst; rewrite !agree_idemp.
 Qed.
 Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y.
 Proof.
  split; [|by intros ?; exists y].
-  by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
+  by intros [z Hz]; rewrite Hz assoc agree_idemp.
 Qed.
 Definition agree_cmra_mixin : CMRAMixin (agree A).
 Proof.
@@ -99,7 +99,7 @@ Proof.
  * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
    rewrite (Hx n'); last auto.
    symmetry; apply dist_le with n; try apply Hx; auto.
-  * intros x; apply agree_idempotent.
+  * intros x; apply agree_idemp.
  * by intros x y n [(?&?&?) ?].
  * by intros x y n; rewrite agree_includedN.
 Qed.
@@ -108,13 +108,13 @@ Proof. intros Hxy; apply Hxy. Qed.
 Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
 Proof.
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
-  by move=> /agree_op_inv->; rewrite agree_idempotent.
+  by move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
 Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
 Proof.
  intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
-  * by rewrite agree_idempotent.
-  * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent.
+  * by rewrite agree_idemp.
+  * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
 Qed.
 Canonical Structure agreeRA : cmraT :=
  CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
@@ -125,7 +125,7 @@ Solve Obligations with done.
 Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
 Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
-Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
+Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
 Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
 Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.

--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -50,8 +50,8 @@ Proof.
    apply (conv_compl (chain_map own c) n).
 Qed.
 Canonical Structure authC := CofeT auth_cofe_mixin.
-Instance Auth_timeless (ea : excl A) (b : A) :
-  Timeless ea → Timeless b → Timeless (Auth ea b).
+Global Instance auth_timeless (x : auth A) :
+  Timeless (authoritative x) → Timeless (own x) → Timeless x.
 Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
 Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A).
 Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed.
@@ -106,10 +106,10 @@ Proof.
  * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
      split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
  * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
-  * by split; simpl; rewrite associative.
-  * by split; simpl; rewrite commutative.
+  * by split; simpl; rewrite assoc.
+  * by split; simpl; rewrite comm.
  * by split; simpl; rewrite ?cmra_unit_l.
-  * by split; simpl; rewrite ?cmra_unit_idempotent.
+  * by split; simpl; rewrite ?cmra_unit_idemp.
  * intros n ??; rewrite! auth_includedN; intros [??].
    by split; simpl; apply cmra_unit_preservingN.
  * assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
@@ -140,7 +140,7 @@ Proof.
  split; simpl.
  * by apply (@cmra_empty_valid A _).
  * by intros x; constructor; rewrite /= left_id.
-  * apply Auth_timeless; apply _.
+  * apply _.
 Qed.
 Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
 Proof. done. Qed.
@@ -153,8 +153,8 @@ Lemma auth_update a a' b b' :
 Proof.
  move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
  destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto.
-  { by rewrite Ha left_id associative. }
-  split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
+  { by rewrite Ha left_id assoc. }
+  split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done].
 Qed.

 Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
@@ -170,7 +170,7 @@ Lemma auth_update_op_l a a' b :
 Proof. by intros; apply (auth_local_update _). Qed.
 Lemma auth_update_op_r a a' b :
  ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
-Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
+Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed.

 (* This does not seem to follow from auth_local_update.
   The trouble is that given ✓ (L a ⋅ a'), Lv a

--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -43,10 +43,10 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
  (* valid *)
  mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x;
  (* monoid *)
-  mixin_cmra_associative : Associative (≡) (⋅);
-  mixin_cmra_commutative : Commutative (≡) (⋅);
+  mixin_cmra_assoc : Assoc (≡) (⋅);
+  mixin_cmra_comm : Comm (≡) (⋅);
  mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
-  mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x;
+  mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x;
  mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
  mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
  mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y
@@ -101,14 +101,14 @@ Section cmra_mixin.
  Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
  Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x.
  Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
-  Global Instance cmra_associative : Associative (≡) (@op A _).
-  Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed.
-  Global Instance cmra_commutative : Commutative (≡) (@op A _).
-  Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed.
+  Global Instance cmra_assoc : Assoc (≡) (@op A _).
+  Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed.
+  Global Instance cmra_comm : Comm (≡) (@op A _).
+  Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_l x : unit x ⋅ x ≡ x.
  Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed.
-  Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x.
-  Proof. apply (mixin_cmra_unit_idempotent _ (cmra_mixin A)). Qed.
+  Lemma cmra_unit_idemp x : unit (unit x) ≡ unit x.
+  Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed.
  Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y.
  Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed.
  Lemma cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
@@ -166,7 +166,7 @@ Proof. apply (ne_proper _). Qed.
 Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
 Proof.
  intros x1 x2 Hx y1 y2 Hy.
-  by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
+  by rewrite Hy (comm _ x1) Hx (comm _ y2).
 Qed.
 Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
 Proof. apply (ne_proper_2 _). Qed.
@@ -217,15 +217,15 @@ Proof. induction 2; eauto using cmra_validN_S. Qed.
 Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x.
 Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed.
 Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
-Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed.
+Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed.
 Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y.
 Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.

 (** ** Units *)
 Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
-Proof. by rewrite (commutative _ x) cmra_unit_l. Qed.
+Proof. by rewrite (comm _ x) cmra_unit_l. Qed.
 Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x.
-Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed.
+Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed.
 Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} unit x.
 Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed.
 Lemma cmra_unit_valid x : ✓ x → ✓ unit x.
@@ -243,7 +243,7 @@ Proof.
  split.
  * by intros x; exists (unit x); rewrite cmra_unit_r.
  * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2).
-    by rewrite (associative _) -Hy -Hz.
+    by rewrite assoc -Hy -Hz.
 Qed.
 Global Instance cmra_included_preorder: PreOrder (@included A _ _).
 Proof.
@@ -265,22 +265,22 @@ Proof. by exists y. Qed.
 Lemma cmra_included_l x y : x ≼ x ⋅ y.
 Proof. by exists y. Qed.
 Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_includedN_l. Qed.
+Proof. rewrite (comm op); apply cmra_includedN_l. Qed.
 Lemma cmra_included_r x y : y ≼ x ⋅ y.
-Proof. rewrite (commutative op); apply cmra_included_l. Qed.
+Proof. rewrite (comm op); apply cmra_included_l. Qed.

 Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
 Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
 Lemma cmra_included_unit x : unit x ≼ x.
 Proof. by exists x; rewrite cmra_unit_l. Qed.
 Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
 Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
-Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
+Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed.
 Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z.
-Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed.
 Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
-Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.
+Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed.

 Lemma cmra_included_dist_l x1 x2 x1' n :
  x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2.
@@ -321,7 +321,7 @@ Section identity.
  Lemma cmra_empty_least x : ∅ ≼ x.
  Proof. by exists x; rewrite left_id. Qed.
  Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅).
-  Proof. by intros x; rewrite (commutative op) left_id. Qed.
+  Proof. by intros x; rewrite (comm op) left_id. Qed.
  Lemma cmra_unit_empty : unit ∅ ≡ ∅.
  Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
 End identity.
@@ -336,7 +336,7 @@ Lemma local_update L `{!LocalUpdate Lv L} x y :
 Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed.

 Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
-Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
+Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed.

 (** ** Updates *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
@@ -366,10 +366,10 @@ Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q.
 Proof.
  intros Hx1 Hx2 Hy z n ?.
-  destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite associative.
+  destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite assoc.
  destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?);
-    first by rewrite associative (commutative _ x2) -associative.
-  exists (y1 ⋅ y2); split; last rewrite (commutative _ y1) -associative; auto.
+    first by rewrite assoc (comm _ x2) -assoc.
+  exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto.
 Qed.
 Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
@@ -448,10 +448,10 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
  ra_validN_ne :> Proper ((≡) ==> impl) valid;
  ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus;
  (* monoid *)
-  ra_associative :> Associative (≡) (⋅);
-  ra_commutative :> Commutative (≡) (⋅);
+  ra_assoc :> Assoc (≡) (⋅);
+  ra_comm :> Comm (≡) (⋅);
  ra_unit_l x : unit x ⋅ x ≡ x;
-  ra_unit_idempotent x : unit (unit x) ≡ unit x;
+  ra_unit_idemp x : unit (unit x) ≡ unit x;
  ra_unit_preserving x y : x ≼ y → unit x ≼ unit y;
  ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x;
  ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y
@@ -524,10 +524,10 @@ Section prod.
    * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
        split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
    * by intros n x [??]; split; apply cmra_validN_S.
-    * split; simpl; apply (associative _).
-    * split; simpl; apply (commutative _).
-    * split; simpl; apply cmra_unit_l.
-    * split; simpl; apply cmra_unit_idempotent.
+    * by split; rewrite /= assoc.
+    * by split; rewrite /= comm.
+    * by split; rewrite /= cmra_unit_l.
+    * by split; rewrite /= cmra_unit_idemp.
    * intros n x y; rewrite !prod_includedN.
      by intros [??]; split; apply cmra_unit_preservingN.
    * intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.

--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -22,21 +22,21 @@ Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op.
 Proof.
  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
  * by rewrite IH.
-  * by rewrite !(associative _) (commutative _ x).
+  * by rewrite !assoc (comm _ x).
  * by transitivity (big_op xs2).
 Qed.
 Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op.
 Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
 Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys.
 Proof.
-  induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
-  by rewrite IH (associative _).
+  induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
+  by rewrite IH assoc.
 Qed.
 Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
 Proof.
  induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
  * by apply cmra_preserving_l.
-  * by rewrite !associative (commutative _ y).
+  * by rewrite !assoc (comm _ y).
  * by transitivity (big_op ys); last apply cmra_included_r.
  * by transitivity (big_op ys).
 Qed.
@@ -58,7 +58,7 @@ Qed.
 Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x.
 Proof.
  rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty.
-  by rewrite big_opM_empty (right_id _ _).
+  by rewrite big_opM_empty right_id.
 Qed.
 Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _).
 Proof.

--- a/algebra/cmra_tactics.v
+++ b/algebra/cmra_tactics.v
@@ -25,7 +25,7 @@ Module ra_reflection. Section ra_reflection.
    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
  Proof.
    by induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
+      rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.
  Qed.
  Lemma flatten_correct Σ e1 e2 :
    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.

--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -106,9 +106,12 @@ Section cofe.
     unfold Proper, respectful; setoid_rewrite equiv_dist.
     by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
  Qed.
-  Lemma contractive_S {B : cofeT} {f : A → B} `{!Contractive f} n x y :
+  Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y :
    x ≡{n}≡ y → f x ≡{S n}≡ f y.
  Proof. eauto using contractive, dist_le with omega. Qed.
+  Lemma contractive_0 {B : cofeT} (f : A → B) `{!Contractive f} x y :
+    f x ≡{0}≡ f y.
+  Proof. eauto using contractive with omega. Qed.
  Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
    Proper (dist n ==> dist n) f | 100.
  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
@@ -136,8 +139,8 @@ Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
-  * apply contractive; auto with omega.
-  * apply contractive_S, IH; auto with omega.
+  * apply (contractive_0 f).
+  * apply (contractive_S f), IH; auto with omega.
 Qed.
 Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
  `{!Contractive f} : A := compl (fixpoint_chain f).
@@ -147,7 +150,7 @@ Section fixpoint.
  Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
  Proof.
    apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
-    induction n as [|n IH]; simpl; eauto using contractive, dist_le with omega.
+    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
  Qed.
  Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
    (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
@@ -337,7 +340,7 @@ Section later.
  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
  Global Instance Next_contractive : Contractive (@Next A).
  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
-  Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Next A).
+  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
  Proof. by intros x y. Qed.
 End later.


--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -23,19 +23,6 @@ Context (map_comp : ∀ {A1 A2 A3 B1 B2 B3 : cofeT}
  map (f ◎ g, g' ◎ f') x ≡ map (g,g') (map (f,f') x)).
 Context (map_contractive : ∀ {A1 A2 B1 B2}, Contractive (@map A1 A2 B1 B2)).

-Lemma map_ext {A1 A2 B1 B2 : cofeT}
-  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' :
-  (∀ x, f x ≡ f' x) → (∀ y, g y ≡ g' y) → x ≡ x' →
-  map (f,g) x ≡ map (f',g') x'.
-Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
-Lemma map_ne {A1 A2 B1 B2 : cofeT}
-  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) n x :
-  (∀ x, f x ≡{n}≡ f' x) → (∀ y, g y ≡{n}≡ g' y) →
-  map (f,g) x ≡{n}≡ map (f',g') x.
-Proof.
-  intros. by apply map_contractive=> i ?; apply dist_le with n; last lia.
-Qed.
-
 Fixpoint A (k : nat) : cofeT :=
  match k with 0 => unitC | S k => F (A k) (A k) end.
 Fixpoint f (k : nat) : A k -n> A (S k) :=
@@ -51,16 +38,13 @@ Arguments g : simpl never.
 Lemma gf {k} (x : A k) : g k (f k x) ≡ x.
 Proof.
  induction k as [|k IH]; simpl in *; [by destruct x|].
-  rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
+  rewrite -map_comp -{2}(map_id _ _ x). by apply (contractive_proper map).
 Qed.
 Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
 Proof.
  induction k as [|k IH]; simpl.
-  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
-    apply map_contractive=> i ?; omega.
-  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
-    apply map_contractive=> i ?; apply dist_le with k; [|omega].
-    split=> x' /=; apply IH.
+  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. apply (contractive_0 map).
+  * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. by apply (contractive_S map).
 Qed.

 Record tower := {
@@ -197,10 +181,10 @@ Next Obligation.
  assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
  induction k as [|k IH]; simpl.
  { rewrite -f_tower f_S -map_comp.
-    apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f. }
+    by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. }
  rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
  rewrite f_S -map_comp.
-  apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f.
+  by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : F T T := compl (unfold_chain X).
 Instance unfold_ne : Proper (dist n ==> dist n) unfold.
@@ -214,7 +198,7 @@ Program Definition fold (X : F T T) : T :=
 Next Obligation.
  intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
  rewrite g_S -map_comp.
-  apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
+  apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
 Instance fold_ne : Proper (dist n ==> dist n) fold.
 Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
@@ -229,7 +213,7 @@ Proof.
    { rewrite /unfold (conv_compl (unfold_chain X) n).
      rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
      rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
-      rewrite f_S -!map_comp; apply map_ne; fold A=> Y.
+      rewrite f_S -!map_comp; apply (contractive_ne map); split=> Y.
      + rewrite /embed' /= /embed_coerce.
        destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
        by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -246,7 +230,8 @@ Proof.
    apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
  * intros X; rewrite equiv_dist=> n /=.
    rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
-    rewrite g_S -!map_comp -{2}(map_id _ _ X); apply map_ne=> Y /=.
+    rewrite g_S -!map_comp -{2}(map_id _ _ X).
+    apply (contractive_ne map); split => Y /=.
    + apply dist_le with n; last omega.
      rewrite f_tower. apply dist_S. by rewrite embed_tower.
    + etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].

--- a/algebra/dra.v
+++ b/algebra/dra.v
@@ -46,14 +46,14 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
  dra_unit_valid x : ✓ x → ✓ unit x;
  dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x);
  (* monoid *)
-  dra_associative :> Associative (≡) (⋅);
+  dra_assoc :> Assoc (≡) (⋅);
  dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
  dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
  dra_symmetric :> Symmetric (@disjoint A _);
-  dra_commutative x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
+  dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
  dra_unit_disjoint_l x : ✓ x → unit x ⊥ x;
  dra_unit_l x : ✓ x → unit x ⋅ x ≡ x;
-  dra_unit_idempotent x : ✓ x → unit (unit x) ≡ unit x;
+  dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x;
  dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y;
  dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x;
  dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y
@@ -73,12 +73,12 @@ Qed.
 Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
 Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
 Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
-Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed.
+Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
 Lemma dra_disjoint_move_r x y z :
  ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
 Proof.
-  intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl.
-  apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
+  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
+  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
 Qed.
 Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
 Hint Unfold dra_included.
@@ -114,11 +114,11 @@ Proof.
    + exists z. by rewrite Hx ?Hy; tauto.
  * intros [x px ?] [y py ?] [z pz ?]; split; simpl;
      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |intros; apply (associative _)].
-  * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative.
+      |by intros; rewrite assoc].
+  * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
  * intros [x px ?]; split;
      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
-  * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent.
+  * intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
  * intros x y Hxy; exists (unit y ⩪ unit x).
    destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl