diff --git a/modures/agree.v b/modures/agree.v
index 3020bf8c83d863cca8759ee0c829cb533c49b170..8aa273ee8e85bd6c6a0b4b2248c1d97693f34b93 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -12,27 +12,27 @@ Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
Section agree.
-Context `{Cofe A}.
+Context {A : cofeT}.
-Global Instance agree_validN : ValidN (agree A) := λ n x,
+Instance agree_validN : ValidN (agree A) := λ n x,
agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ={n'}= x n.
Lemma agree_valid_le (x : agree A) n n' :
agree_is_valid x n → n' ≤ n → agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
-Global Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
-Global Instance agree_equiv : Equiv (agree A) := λ x y,
+Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
+Instance agree_equiv : Equiv (agree A) := λ x y,
(∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
(∀ n, agree_is_valid x n → x n ={n}= y n).
-Global Instance agree_dist : Dist (agree A) := λ n x y,
+Instance agree_dist : Dist (agree A) := λ n x y,
(∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧
(∀ n', n' ≤ n → agree_is_valid x n' → x n' ={n'}= y n').
-Global Program Instance agree_compl : Compl (agree A) := λ c,
+Program Instance agree_compl : Compl (agree A) := λ c,
{| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
Next Obligation. intros; apply agree_valid_0. Qed.
Next Obligation.
intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
Qed.
-Instance agree_cofe : Cofe (agree A).
+Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
split.
* intros x y; split.
@@ -49,14 +49,15 @@ Proof.
by split; intros; apply agree_valid_0.
* by intros c n; split; intros; apply (chain_cauchy c).
Qed.
+Canonical Structure agreeC := CofeT agree_cofe_mixin.
-Global Program Instance agree_op : Op (agree A) := λ x y,
+Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ={n}= y |}.
Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
-Global Instance agree_unit : Unit (agree A) := id.
-Global Instance agree_minus : Minus (agree A) := λ x y, x.
+Instance agree_unit : Unit (agree A) := id.
+Instance agree_minus : Minus (agree A) := λ x y, x.
Instance: Commutative (≡) (@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.
@@ -70,7 +71,7 @@ Proof.
* etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
eauto using agree_valid_le.
Qed.
-Instance: Proper (dist n ==> dist n ==> dist n) op.
+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.
Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Instance: Associative (≡) (@op (agree A) _).
@@ -84,7 +85,7 @@ Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
Qed.
-Global Instance agree_cmra : CMRA (agree A).
+Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
* intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
@@ -103,12 +104,15 @@ Qed.
Lemma agree_op_inv (x y1 y2 : agree A) n :
✓{n} x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2.
Proof. by intros [??] Hxy; apply Hxy. Qed.
-Global Instance agree_extend : CMRAExtend (agree A).
+Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent.
* by rewrite Hx (agree_op_inv x y1 y2) // agree_idempotent.
Qed.
+Canonical Structure agreeRA : cmraT :=
+ CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
+
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
@@ -125,12 +129,20 @@ Proof.
Qed.
End agree.
+Arguments agreeC : clear implicits.
+Arguments agreeRA : clear implicits.
+
Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
{| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
Solve Obligations with auto using agree_valid_0, agree_valid_S.
+Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
+Proof. by destruct x. Qed.
+Lemma agree_map_compose {A B C} (f : A → B) (g : B → C)
+ (x : agree A) : agree_map (g ∘ f) x = agree_map g (agree_map f x).
+Proof. done. Qed.
Section agree_map.
- Context `{Cofe A, Cofe B} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+ Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Global Instance agree_map_proper :
@@ -147,13 +159,7 @@ Section agree_map.
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Qed.
End agree_map.
-Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
-Proof. by destruct x. Qed.
-Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
- agree_map (g ∘ f) x = agree_map g (agree_map f x).
-Proof. done. Qed.
-Canonical Structure agreeRA (A : cofeT) : cmraT := CMRAT (agree A).
Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A → agreeRA B).
Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
diff --git a/modures/auth.v b/modures/auth.v
index 44f63688500c3fe76a07f9f7c17e61ef7a01c984..4585be08b3e85e4b40acba74a0edda278056ddd6 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -10,22 +10,24 @@ Notation "â—¯ x" := (Auth ExclUnit x) (at level 20).
Notation "◠x" := (Auth (Excl x) ∅) (at level 20).
(* COFE *)
-Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
+Section cofe.
+Context {A : cofeT}.
+
+Instance auth_equiv : Equiv (auth A) := λ x y,
authoritative x ≡ authoritative y ∧ own x ≡ own y.
-Instance auth_dist `{Dist A} : Dist (auth A) := λ n x y,
+Instance auth_dist : Dist (auth A) := λ n x y,
authoritative x ={n}= authoritative y ∧ own x ={n}= own y.
-Instance Auth_ne `{Dist A} : Proper (dist n ==> dist n ==> dist n) (@Auth A).
+Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Proof. by split. Qed.
-Instance authoritative_ne `{Dist A} :
- Proper (dist n ==> dist n) (@authoritative A).
+Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
Proof. by destruct 1. Qed.
-Instance own_ne `{Dist A} : Proper (dist n ==> dist n) (@own A).
+Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
Proof. by destruct 1. Qed.
-Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
+Instance auth_compl : Compl (auth A) := λ c,
Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
-Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
+Definition auth_cofe_mixin : CofeMixin (auth A).
Proof.
split.
* intros x y; unfold dist, auth_dist, equiv, auth_equiv.
@@ -39,53 +41,59 @@ Proof.
* intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n).
Qed.
-Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) :
+Canonical Structure authC := CofeT auth_cofe_mixin.
+Instance Auth_timeless (x : excl A) (y : A) :
Timeless x → Timeless y → Timeless (Auth x y).
-Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed.
+Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
+End cofe.
+
+Arguments authC : clear implicits.
(* CMRA *)
-Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
-Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
+Section cmra.
+Context {A : cmraT}.
+
+Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
+Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
| Excl a => own x ≼ a ∧ ✓ a
| ExclUnit => ✓ (own x)
| ExclBot => False
end.
-Arguments auth_valid _ _ _ _ !_ /.
-Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x,
+Global Arguments auth_valid !_ /.
+Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x ≼{n} a ∧ ✓{n} a
| ExclUnit => ✓{n} (own x)
| ExclBot => n = 0
end.
-Arguments auth_validN _ _ _ _ _ !_ /.
-Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
+Global Arguments auth_validN _ !_ /.
+Instance auth_unit : Unit (auth A) := λ x,
Auth (unit (authoritative x)) (unit (own x)).
-Instance auth_op `{Op A} : Op (auth A) := λ x y,
+Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x â‹… authoritative y) (own x â‹… own y).
-Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
+Instance auth_minus : Minus (auth A) := λ x y,
Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
-Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
+Lemma auth_included (x y : auth A) :
x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
-Lemma auth_includedN `{Dist A, Op A} n (x y : auth A) :
+Lemma auth_includedN n (x y : auth A) :
x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
-Lemma authoritative_validN `{CMRA A} n (x : auth A) :
- ✓{n} x → ✓{n} (authoritative x).
+Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} (authoritative x).
Proof. by destruct x as [[]]. Qed.
-Lemma own_validN `{CMRA A} n (x : auth A) : ✓{n} x → ✓{n} (own x).
+Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} (own x).
Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
-Instance auth_cmra `{CMRA A} : CMRA (auth A).
+
+Definition auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
- * apply _.
* by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* intros n [x a] [y b] [Hx Ha]; simpl in *;
@@ -103,14 +111,14 @@ Proof.
* by split; simpl; rewrite ?(ra_unit_idempotent _).
* intros n ??; rewrite! auth_includedN; intros [??].
by split; simpl; apply cmra_unit_preserving.
- * assert (∀ n a b1 b2, b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
+ * assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
{ intros n a b1 b2 <-; apply cmra_included_l. }
intros n [[a1| |] b1] [[a2| |] b2];
naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
* by intros n ??; rewrite auth_includedN;
intros [??]; split; simpl; apply cmra_op_minus.
Qed.
-Instance auth_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (auth A).
+Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
Proof.
intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend_op n (authoritative x) (authoritative y1)
@@ -119,39 +127,49 @@ Proof.
as (z2&?&?&?); auto using own_validN.
by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
Qed.
-Instance auth_ra_empty `{CMRA A, Empty A, !RAIdentity A} : RAIdentity (auth A).
+Canonical Structure authRA : cmraT :=
+ CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
+Instance auth_ra_empty `{Empty A} : RAIdentity A → RAIdentity (auth A).
Proof.
- split; [apply (ra_empty_valid (A:=A))|].
+ split; simpl; [apply ra_empty_valid|].
by intros x; constructor; simpl; rewrite (left_id _ _).
Qed.
-Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
+Global Instance auth_frag_valid_timeless (x : A) :
ValidTimeless x → ValidTimeless (◯ x).
Proof. by intros ??; apply (valid_timeless x). Qed.
-Instance auth_valid_timeless `{CMRA A, Empty A, !RAIdentity A} (x : A) :
+Global Instance auth_valid_timeless `{Empty A, !RAIdentity A} (x : A) :
ValidTimeless x → ValidTimeless (◠x).
Proof.
by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
Qed.
-Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
+Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
+Lemma auth_includedN' n (x y : authC A) :
+ x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y.
+Proof.
+ split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
+ intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
+Qed.
+End cmra.
+
+Arguments authRA : clear implicits.
(* Functor *)
-Definition authRA (A : cmraT) : cmraT := CMRAT (auth A).
Instance auth_fmap : FMap auth := λ A B f x,
Auth (f <$> authoritative x) (f (own x)).
-Instance auth_fmap_cmra_ne `{Dist A, Dist B} n :
+Instance auth_fmap_cmra_ne {A B : cmraT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
Qed.
-Instance auth_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) :
+Instance auth_fmap_cmra_monotone {A B : cmraT} (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f →
CMRAMonotone (fmap f : auth A → auth B).
Proof.
split.
- * by intros n [x a] [y b]; rewrite !auth_includedN; simpl;
- intros [??]; split; apply includedN_preserving.
- * intros n [[a| |] b];
+ * by intros n [x a] [y b]; rewrite !auth_includedN /=;
+ intros [??]; split; simpl; apply: includedN_preserving.
+ * intros n [[a| |] b]; rewrite /= /cmra_validN;
naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authRA_map {A B : cmraT} (f : A -n> B) : authRA A -n> authRA B :=
diff --git a/modures/cmra.v b/modures/cmra.v
index d974534afd84b53fe927ce579ef87da602dc7141..c31f970922625c0cbdb5db833635062d88e488ee 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -10,37 +10,29 @@ Notation "x ≼{ n } y" := (includedN n x y)
Instance: Params (@includedN) 4.
Hint Extern 0 (?x ≼{_} ?x) => reflexivity.
-Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
+Record CMRAMixin A
+ `{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
(* setoids *)
- cmra_cofe :> Cofe A;
- cmra_op_ne n x :> Proper (dist n ==> dist n) (op x);
- cmra_unit_ne n :> Proper (dist n ==> dist n) unit;
- cmra_valid_ne n :> Proper (dist n ==> impl) (✓{n});
- cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus;
+ mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
+ mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
+ mixin_cmra_valid_ne n : Proper (dist n ==> impl) (✓{n});
+ mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
(* valid *)
- cmra_valid_0 x : ✓{0} x;
- cmra_valid_S n x : ✓{S n} x → ✓{n} x;
- cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
+ mixin_cmra_valid_0 x : ✓{0} x;
+ mixin_cmra_valid_S n x : ✓{S n} x → ✓{n} x;
+ mixin_cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x;
(* monoid *)
- cmra_associative : Associative (≡) (⋅);
- cmra_commutative : Commutative (≡) (⋅);
- cmra_unit_l x : unit x ⋅ x ≡ x;
- cmra_unit_idempotent x : unit (unit x) ≡ unit x;
- cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y;
- cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
- cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y
+ mixin_cmra_associative : Associative (≡) (⋅);
+ mixin_cmra_commutative : Commutative (≡) (⋅);
+ mixin_cmra_unit_l x : unit x ⋅ x ≡ x;
+ mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit x;
+ mixin_cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y;
+ mixin_cmra_valid_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
}.
-Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} :=
- cmra_extend_op n x y1 y2 :
- ✓{n} x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }.
-
-Class CMRAMonotone
- `{Dist A, Op A, ValidN A, Dist B, Op B, ValidN B} (f : A → B) := {
- includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
- validN_preserving n x : ✓{n} x → ✓{n} (f x)
-}.
-
-Hint Extern 0 (✓{0} _) => apply cmra_valid_0.
+Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := ∀ n x y1 y2,
+ ✓{n} x → x ={n}= y1 ⋅ y2 →
+ { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ={n}= y1 ∧ z.2 ={n}= y2 }.
(** Bundeled version *)
Structure cmraT := CMRAT {
@@ -53,32 +45,73 @@ Structure cmraT := CMRAT {
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_minus : Minus cmra_car;
- cmra_cmra : CMRA cmra_car;
- cmra_extend : CMRAExtend cmra_car
+ cmra_cofe_mixin : CofeMixin cmra_car;
+ cmra_mixin : CMRAMixin cmra_car;
+ cmra_extend_mixin : CMRAExtendMixin cmra_car
}.
-Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _}.
-Arguments cmra_car _ : simpl never.
-Arguments cmra_equiv _ _ _ : simpl never.
-Arguments cmra_dist _ _ _ _ : simpl never.
-Arguments cmra_compl _ _ : simpl never.
-Arguments cmra_unit _ _ : simpl never.
-Arguments cmra_op _ _ _ : simpl never.
-Arguments cmra_valid _ _ : simpl never.
-Arguments cmra_validN _ _ _ : simpl never.
-Arguments cmra_minus _ _ _ : simpl never.
-Arguments cmra_cmra _ : simpl never.
+Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _ _.
+Arguments cmra_car : simpl never.
+Arguments cmra_equiv : simpl never.
+Arguments cmra_dist : simpl never.
+Arguments cmra_compl : simpl never.
+Arguments cmra_unit : simpl never.
+Arguments cmra_op : simpl never.
+Arguments cmra_valid : simpl never.
+Arguments cmra_validN : simpl never.
+Arguments cmra_minus : simpl never.
+Arguments cmra_cofe_mixin : simpl never.
+Arguments cmra_mixin : simpl never.
+Arguments cmra_extend_mixin : simpl never.
Add Printing Constructor cmraT.
-Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
- cmra_valid cmra_validN cmra_minus cmra_cmra cmra_extend.
-Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A.
+Existing Instances cmra_unit cmra_op cmra_valid cmra_validN cmra_minus.
+Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
+(** Lifting properties from the mixin *)
+Section cmra_mixin.
+ Context {A : cmraT}.
+ Implicit Types x y : A.
+ Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
+ Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
+ Global Instance cmra_unit_ne n : Proper (dist n ==> dist n) (@unit A _).
+ Proof. apply (mixin_cmra_unit_ne _ (cmra_mixin A)). Qed.
+ Global Instance cmra_valid_ne n : Proper (dist n ==> impl) (@validN A _ n).
+ Proof. apply (mixin_cmra_valid_ne _ (cmra_mixin A)). Qed.
+ Global Instance cmra_minus_ne n :
+ Proper (dist n ==> dist n ==> dist n) (@minus A _).
+ Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
+ Lemma cmra_valid_0 x : ✓{0} x.
+ Proof. apply (mixin_cmra_valid_0 _ (cmra_mixin A)). Qed.
+ Lemma cmra_valid_S n x : ✓{S n} x → ✓{n} x.
+ Proof. apply (mixin_cmra_valid_S _ (cmra_mixin A)). Qed.
+ Lemma cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x.
+ Proof. apply (mixin_cmra_valid_validN _ (cmra_mixin A)). Qed.
+ Lemma cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y.
+ Proof. apply (mixin_cmra_unit_preserving _ (cmra_mixin A)). Qed.
+ Lemma cmra_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x.
+ Proof. apply (mixin_cmra_valid_op_l _ (cmra_mixin A)). Qed.
+ Lemma cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ={n}= y.
+ Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
+ Lemma cmra_extend_op n x y1 y2 :
+ ✓{n} x → x ={n}= y1 ⋅ y2 →
+ { z | x ≡ z.1 ⋅ z.2 ∧ z.1 ={n}= y1 ∧ z.2 ={n}= y2 }.
+ Proof. apply (cmra_extend_mixin A). Qed.
+End cmra_mixin.
+
+Hint Extern 0 (✓{0} _) => apply cmra_valid_0.
+
+(** Morphisms *)
+Class CMRAMonotone {A B : cmraT} (f : A → B) := {
+ includedN_preserving n x y : x ≼{n} y → f x ≼{n} f y;
+ validN_preserving n x : ✓{n} x → ✓{n} (f x)
+}.
+
(** Updates *)
-Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A → Prop) := ∀ z n,
+Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
Instance: Params (@cmra_updateP) 3.
Infix "â‡:" := cmra_updateP (at level 70).
-Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n,
+Definition cmra_update {A : cmraT} (x y : A) := ∀ z n,
✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Infix "â‡" := cmra_update (at level 70).
Instance: Params (@cmra_update) 3.
@@ -86,13 +119,13 @@ Instance: Params (@cmra_update) 3.
(** Timeless validity *)
(* Not sure whether this is useful, see the rule [uPred_valid_elim_timeless]
in logic.v *)
-Class ValidTimeless `{Valid A, ValidN A} (x : A) :=
+Class ValidTimeless {A : cmraT} (x : A) :=
valid_timeless : validN 1 x → valid x.
-Arguments valid_timeless {_ _ _} _ {_} _.
+Arguments valid_timeless {_} _ {_} _.
(** Properties **)
Section cmra.
-Context `{cmra : CMRA A}.
+Context {A : cmraT}.
Implicit Types x y z : A.
Lemma cmra_included_includedN x y : x ≼ y ↔ ∀ n, x ≼{n} y.
@@ -102,17 +135,17 @@ Proof.
symmetry; apply cmra_op_minus, Hxy.
Qed.
-Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n}) | 1.
+Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n} : A → _) | 1.
Proof. by split; apply cmra_valid_ne. Qed.
-Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n}) | 1.
+Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n} : A → _) | 1.
Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
Global Instance cmra_ra : RA A.
Proof.
- split; try by (destruct cmra;
+ split; try by (destruct (@cmra_mixin A);
eauto using ne_proper, ne_proper_2 with typeclass_instances).
* by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
* intros x y; rewrite !cmra_included_includedN.
- eauto using cmra_unit_preserving.
+ eauto using @cmra_unit_preserving.
* intros x y; rewrite !cmra_valid_validN; intros ? n.
by apply cmra_valid_op_l with y.
* intros x y [z Hz]; apply equiv_dist; intros n.
@@ -122,17 +155,16 @@ Lemma cmra_valid_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y.
Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
Lemma cmra_valid_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x.
Proof. induction 2; eauto using cmra_valid_S. Qed.
-Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (â‹…).
+Global Instance ra_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).
Qed.
Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x).
-Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
+Proof. rewrite -{1}(ra_unit_l x); apply cmra_valid_op_l. Qed.
(** * Timeless *)
-Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
- Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
+Lemma cmra_timeless_included_l x y : Timeless x → ✓{1} y → x ≼{1} y → x ≼ y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
@@ -140,7 +172,7 @@ Proof.
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{1} y → x ≼{n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
-Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
+Lemma cmra_op_timeless x1 x2 :
✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
Proof.
intros ??? z Hz.
@@ -151,13 +183,13 @@ Qed.
(** * Included *)
Global Instance cmra_included_ne n :
- Proper (dist n ==> dist n ==> iff) (includedN n) | 1.
+ Proper (dist n ==> dist n ==> iff) (includedN n : relation A) | 1.
Proof.
intros x x' Hx y y' Hy; unfold includedN.
by setoid_rewrite Hx; setoid_rewrite Hy.
Qed.
Global Instance cmra_included_proper :
- Proper ((≡) ==> (≡) ==> iff) (includedN n) | 1.
+ Proper ((≡) ==> (≡) ==> iff) (includedN n : relation A) | 1.
Proof.
intros n x x' Hx y y' Hy; unfold includedN.
by setoid_rewrite Hx; setoid_rewrite Hy.
@@ -171,7 +203,7 @@ Lemma cmra_included_l n x y : x ≼{n} x ⋅ y.
Proof. by exists y. Qed.
Lemma cmra_included_r n x y : y ≼{n} x ⋅ y.
Proof. rewrite (commutative op); apply cmra_included_l. Qed.
-Global Instance cmra_included_ord n : PreOrder (includedN n).
+Global Instance cmra_included_ord n : PreOrder (includedN n : relation A).
Proof.
split.
* by intros x; exists (unit x); rewrite ra_unit_r.
@@ -179,9 +211,9 @@ Proof.
by rewrite (associative _) -Hy -Hz.
Qed.
Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{n} x.
-Proof. intros Hyv [z Hy]; revert Hyv; rewrite Hy; apply cmra_valid_op_l. Qed.
+Proof. intros Hyv [z ?]; cofe_subst y; eauto using @cmra_valid_op_l. Qed.
Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{n} x.
-Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed.
+Proof. rewrite cmra_included_includedN; eauto using @cmra_valid_includedN. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n :
x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
Proof.
@@ -190,7 +222,7 @@ Proof.
Qed.
(** * Properties of [(â‡)] relation *)
-Global Instance cmra_update_preorder : PreOrder cmra_update.
+Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
Lemma cmra_update_updateP x y : x ⇠y ↔ x â‡: (y =).
Proof.
@@ -200,9 +232,14 @@ Proof.
Qed.
End cmra.
-Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A).
+Hint Resolve cmra_ra.
+Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
+(* Also via [cmra_cofe; cofe_equivalence] *)
+Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
+
+Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. by split. Qed.
-Instance cmra_monotone_ra_monotone `{CMRA A, CMRA B} (f : A → B) :
+Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A → B) :
CMRAMonotone f → RAMonotone f.
Proof.
split.
@@ -212,18 +249,13 @@ Proof.
by intros ? n; apply validN_preserving.
Qed.
-Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
-(* Also via [cmra_cofe; cofe_equivalence] *)
-Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
-
(** Discrete *)
Section discrete.
Context `{ra : RA A}.
Existing Instances discrete_dist discrete_compl.
- Let discrete_cofe' : Cofe A := discrete_cofe.
Instance discrete_validN : ValidN A := λ n x,
match n with 0 => True | S n => ✓ x end.
- Instance discrete_cmra : CMRA A.
+ Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
split; try by (destruct ra; auto).
* by intros [|n]; try apply ra_op_proper.
@@ -236,91 +268,93 @@ Section discrete.
* by intros [|n]; try apply ra_valid_op_l.
* by intros [|n] x y; try apply ra_op_minus.
Qed.
- Instance discrete_extend : CMRAExtend A.
+ Definition discrete_extend_mixin : CMRAExtendMixin A.
Proof.
- intros [|n] x y1 y2 ??; [|by exists (y1,y2)].
+ intros [|n] x y1 y2 ??; [|by exists (y1,y2); rewrite /dist /discrete_dist].
by exists (x,unit x); simpl; rewrite ra_unit_r.
Qed.
- Global Instance discrete_timeless (x : A) : ValidTimeless x.
+ Definition discreteRA : cmraT :=
+ CMRAT discrete_cofe_mixin discrete_cmra_mixin discrete_extend_mixin.
+ Global Instance discrete_timeless (x : A) : ValidTimeless (x : discreteRA).
Proof. by intros ?. Qed.
- Definition discreteRA : cmraT := CMRAT A.
Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} :
- (∀ z, ✓ (x â‹… z) → ∃ y, P y ∧ ✓ (y â‹… z)) → x â‡: P.
+ (∀ z, ✓ (x â‹… z) → ∃ y, P y ∧ ✓ (y â‹… z)) → (x : discreteRA) â‡: P.
Proof.
intros Hvalid z [|n]; [|apply Hvalid].
by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y.
Qed.
- Lemma discrete_update (x y : A) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇠y.
+ Lemma discrete_update (x y : A) :
+ (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → (x : discreteRA) ⇠y.
Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed.
End discrete.
Arguments discreteRA _ {_ _ _ _ _ _}.
(** Product *)
-Instance prod_op `{Op A, Op B} : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
-Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
-Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := λ x,
- (unit (x.1), unit (x.2)).
-Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x,
- ✓ (x.1) ∧ ✓ (x.2).
-Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x,
- ✓{n} (x.1) ∧ ✓{n} (x.2).
-Instance prod_minus `{Minus A, Minus B} : Minus (A * B) := λ x y,
- (x.1 ⩪ y.1, x.2 ⩪ y.2).
-Lemma prod_included `{Equiv A, Equiv B, Op A, Op B} (x y : A * B) :
- x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
-Proof.
- split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
- intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
-Qed.
-Lemma prod_includedN `{Dist A, Dist B, Op A, Op B} (x y : A * B) n :
- x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2.
-Proof.
- split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
- intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
-Qed.
-Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B).
-Proof.
- split; try apply _.
- * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
- * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite -?Hy1 -?Hy2.
- * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
- split; simpl in *; rewrite ?Hx1 ?Hx2 ?Hy1 ?Hy2.
- * split; apply cmra_valid_0.
- * by intros n x [??]; split; apply cmra_valid_S.
- * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
- intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid.
- * split; simpl; apply (associative _).
- * split; simpl; apply (commutative _).
- * split; simpl; apply ra_unit_l.
- * split; simpl; apply ra_unit_idempotent.
- * intros n x y; rewrite !prod_includedN.
- by intros [??]; split; apply cmra_unit_preserving.
- * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
- * intros x y n; rewrite prod_includedN; intros [??].
- by split; apply cmra_op_minus.
-Qed.
-Instance prod_ra_empty `{RAIdentity A, RAIdentity B} : RAIdentity (A * B).
-Proof.
- repeat split; simpl; repeat apply ra_empty_valid; repeat apply (left_id _ _).
-Qed.
-Instance prod_cmra_extend `{CMRAExtend A, CMRAExtend B} : CMRAExtend (A * B).
-Proof.
- intros n x y1 y2 [??] [??]; simpl in *.
- destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
- destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
- by exists ((z1.1,z2.1),(z1.2,z2.2)).
-Qed.
-Instance pair_timeless `{Valid A, ValidN A, Valid B, ValidN B} (x : A) (y : B) :
- ValidTimeless x → ValidTimeless y → ValidTimeless (x,y).
-Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
-Canonical Structure prodRA (A B : cmraT) : cmraT := CMRAT (A * B).
-Instance prod_map_cmra_monotone `{CMRA A, CMRA A', CMRA B, CMRA B'}
- (f : A → A') (g : B → B') `{!CMRAMonotone f, !CMRAMonotone g} :
- CMRAMonotone (prod_map f g).
+Section prod.
+ Context {A B : cmraT}.
+ Instance prod_op : Op (A * B) := λ x y, (x.1 ⋅ y.1, x.2 ⋅ y.2).
+ Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅).
+ Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
+ Instance prod_valid : Valid (A * B) := λ x, ✓ (x.1) ∧ ✓ (x.2).
+ Instance prod_validN : ValidN (A * B) := λ n x, ✓{n} (x.1) ∧ ✓{n} (x.2).
+ Instance prod_minus : Minus (A * B) := λ x y, (x.1 ⩪ y.1, x.2 ⩪ y.2).
+ Lemma prod_included (x y : A * B) : x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2.
+ Proof.
+ split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
+ intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
+ Qed.
+ Lemma prod_includedN (x y : A * B) n : x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2.
+ Proof.
+ split; [intros [z Hz]; split; [exists (z.1)|exists (z.2)]; apply Hz|].
+ intros [[z1 Hz1] [z2 Hz2]]; exists (z1,z2); split; auto.
+ Qed.
+ Definition prod_cmra_mixin : CMRAMixin (A * B).
+ Proof.
+ split; try apply _.
+ * by intros n x y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
+ * by intros n y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hy1 ?Hy2.
+ * by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
+ * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
+ split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
+ * split; apply cmra_valid_0.
+ * by intros n x [??]; split; apply cmra_valid_S.
+ * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
+ intros Hvalid; split; apply cmra_valid_validN; intros n; apply Hvalid.
+ * split; simpl; apply (associative _).
+ * split; simpl; apply (commutative _).
+ * split; simpl; apply ra_unit_l.
+ * split; simpl; apply ra_unit_idempotent.
+ * intros n x y; rewrite !prod_includedN.
+ by intros [??]; split; apply cmra_unit_preserving.
+ * intros n x y [??]; split; simpl in *; eapply cmra_valid_op_l; eauto.
+ * intros x y n; rewrite prod_includedN; intros [??].
+ by split; apply cmra_op_minus.
+ Qed.
+ Global Instance prod_ra_empty `{Empty A, Empty B} :
+ RAIdentity A → RAIdentity B → RAIdentity (A * B).
+ Proof.
+ repeat split; simpl; repeat (apply ra_empty_valid || apply (left_id _ _)).
+ Qed.
+ Definition prod_cmra_extend_mixin : CMRAExtendMixin (A * B).
+ Proof.
+ intros n x y1 y2 [??] [??]; simpl in *.
+ destruct (cmra_extend_op n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
+ destruct (cmra_extend_op n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
+ by exists ((z1.1,z2.1),(z1.2,z2.2)).
+ Qed.
+ Canonical Structure prodRA : cmraT :=
+ CMRAT prod_cofe_mixin prod_cmra_mixin prod_cmra_extend_mixin.
+ Instance pair_timeless (x : A) (y : B) :
+ ValidTimeless x → ValidTimeless y → ValidTimeless (x,y).
+ Proof. by intros ?? [??]; split; apply (valid_timeless _). Qed.
+End prod.
+Arguments prodRA : clear implicits.
+
+Instance prod_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
+ CMRAMonotone f → CMRAMonotone g → CMRAMonotone (prod_map f g).
Proof.
split.
- * intros n x1 x2; rewrite !prod_includedN; intros [??]; simpl.
+ * intros n x y; rewrite !prod_includedN; intros [??]; simpl.
by split; apply includedN_preserving.
* by intros n x [??]; split; simpl; apply validN_preserving.
Qed.
diff --git a/modures/cofe.v b/modures/cofe.v
index bca6b342113729ea2cc88ba4bf69f7b709fb7a83..b508eb45fb94b62ded4c4ee3f41365d81eb08073 100644
--- a/modures/cofe.v
+++ b/modures/cofe.v
@@ -29,14 +29,13 @@ Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A → A.
-Class Cofe A `{Equiv A, Compl A} := {
- equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
- dist_equivalence n :> Equivalence (dist n);
- dist_S n x y : x ={S n}= y → x ={n}= y;
- dist_0 x y : x ={0}= y;
- conv_compl (c : chain A) n : compl c ={n}= c n
+Record CofeMixin A `{Equiv A, Compl A} := {
+ mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
+ mixin_dist_equivalence n : Equivalence (dist n);
+ mixin_dist_S n x y : x ={S n}= y → x ={n}= y;
+ mixin_dist_0 x y : x ={0}= y;
+ mixin_conv_compl (c : chain A) n : compl c ={n}= c n
}.
-Hint Extern 0 (_ ={0}= _) => apply dist_0.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
contractive n : Proper (dist n ==> dist (S n)) f.
@@ -46,20 +45,39 @@ Structure cofeT := CofeT {
cofe_equiv : Equiv cofe_car;
cofe_dist : Dist cofe_car;
cofe_compl : Compl cofe_car;
- cofe_cofe : Cofe cofe_car
+ cofe_mixin : CofeMixin cofe_car
}.
-Arguments CofeT _ {_ _ _ _}.
+Arguments CofeT {_ _ _ _} _.
Add Printing Constructor cofeT.
-Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
-Arguments cofe_car _ : simpl never.
-Arguments cofe_equiv _ _ _ : simpl never.
-Arguments cofe_dist _ _ _ _ : simpl never.
-Arguments cofe_compl _ _ : simpl never.
-Arguments cofe_cofe _ : simpl never.
+Existing Instances cofe_equiv cofe_dist cofe_compl.
+Arguments cofe_car : simpl never.
+Arguments cofe_equiv : simpl never.
+Arguments cofe_dist : simpl never.
+Arguments cofe_compl : simpl never.
+Arguments cofe_mixin : simpl never.
+
+(** Lifting properties from the mixin *)
+Section cofe_mixin.
+ Context {A : cofeT}.
+ Implicit Types x y : A.
+ Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y.
+ Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
+ Global Instance dist_equivalence n : Equivalence (@dist A _ n).
+ Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
+ Lemma dist_S n x y : x ={S n}= y → x ={n}= y.
+ Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
+ Lemma dist_0 x y : x ={0}= y.
+ Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
+ Lemma conv_compl (c : chain A) n : compl c ={n}= c n.
+ Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
+End cofe_mixin.
+
+Hint Extern 0 (_ ={0}= _) => apply dist_0.
(** General properties *)
Section cofe.
- Context `{Cofe A}.
+ Context {A : cofeT}.
+ Implicit Types x y : A.
Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
Proof.
split.
@@ -67,24 +85,24 @@ Section cofe.
* by intros x y; rewrite !equiv_dist.
* by intros x y z; rewrite !equiv_dist; intros; transitivity y.
Qed.
- Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (dist n).
+ Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Proof.
intros x1 x2 ? y1 y2 ?; split; intros.
* by transitivity x1; [|transitivity y1].
* by transitivity x2; [|transitivity y2].
Qed.
- Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (dist n).
+ Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n).
Proof.
by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Qed.
Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
- Lemma dist_le x y n n' : x ={n}= y → n' ≤ n → x ={n'}= y.
+ Lemma dist_le (x y : A) n n' : x ={n}= y → n' ≤ n → x ={n'}= y.
Proof. induction 2; eauto using dist_S. Qed.
- Instance ne_proper `{Cofe B} (f : A → B)
+ Instance ne_proper {B : cofeT} (f : A → B)
`{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
- Instance ne_proper_2 `{Cofe B, Cofe C} (f : A → B → C)
+ Instance ne_proper_2 {B C : cofeT} (f : A → B → C)
`{!∀ n, Proper (dist n ==> dist n ==> dist n) f} :
Proper ((≡) ==> (≡) ==> (≡)) f | 100.
Proof.
@@ -95,10 +113,10 @@ Section cofe.
Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
- Global Instance contractive_ne `{Cofe B} (f : A → B) `{!Contractive f} n :
+ Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
- Global Instance contractive_proper `{Cofe B} (f : A → B) `{!Contractive f} :
+ Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
Proper ((≡) ==> (≡)) f | 100 := _.
End cofe.
@@ -106,24 +124,24 @@ End cofe.
Program Definition chain_map `{Dist A, Dist B} (f : A → B)
`{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
{| chain_car n := f (c n) |}.
-Next Obligation. by intros A ? B ? f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
-Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y → x ≡ y.
-Arguments timeless {_ _ _} _ {_} _ _.
+Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y → x ≡ y.
+Arguments timeless {_} _ {_} _ _.
(** Fixpoint *)
-Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A)
+Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Next Obligation.
- intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
+ intros A ? f ? n; induction n as [|n IH]; intros i ?; first done.
destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Qed.
-Program Definition fixpoint `{Cofe A, Inhabited A} (f : A → A)
+Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Section fixpoint.
- Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
+ Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
apply equiv_dist; intros n; unfold fixpoint.
@@ -153,46 +171,51 @@ Arguments CofeMor {_ _} _ {_}.
Add Printing Constructor cofeMor.
Existing Instance cofe_mor_ne.
-Instance cofe_mor_proper `(f : cofeMor A B) : Proper ((≡) ==> (≡)) f := _.
-Instance cofe_mor_equiv {A B : cofeT} : Equiv (cofeMor A B) := λ f g,
- ∀ x, f x ≡ g x.
-Instance cofe_mor_dist (A B : cofeT) : Dist (cofeMor A B) := λ n f g,
- ∀ x, f x ={n}= g x.
-Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
- {| chain_car n := c n x |}.
-Next Obligation. intros A B c x n i ?. by apply (chain_cauchy c). Qed.
-Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
- {| cofe_mor_car x := compl (fun_chain c x) |}.
-Next Obligation.
- intros A B c n x y Hxy.
- rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy.
- apply (chain_cauchy c); lia.
-Qed.
-Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
-Proof.
- split.
- * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|].
- intros HXY k; apply equiv_dist; intros n; apply HXY.
- * intros n; split.
- + by intros f x.
- + by intros f g ? x.
- + by intros f g h ?? x; transitivity (g x).
- * by intros n f g ? x; apply dist_S.
- * by intros f g x.
- * intros c n x; simpl.
- rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
-Qed.
-Instance cofe_mor_car_ne A B n :
- Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
-Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
-Instance cofe_mor_car_proper A B :
- Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _.
-Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
-Proof. done. Qed.
-Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
+Section cofe_mor.
+ Context {A B : cofeT}.
+ Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f.
+ Proof. apply ne_proper, cofe_mor_ne. Qed.
+ Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, ∀ x, f x ≡ g x.
+ Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ={n}= g x.
+ Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
+ {| chain_car n := c n x |}.
+ Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
+ Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
+ {| cofe_mor_car x := compl (fun_chain c x) |}.
+ Next Obligation.
+ intros c n x y Hx.
+ rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hx.
+ apply (chain_cauchy c); lia.
+ Qed.
+ Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
+ Proof.
+ split.
+ * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|].
+ intros HXY k; apply equiv_dist; intros n; apply HXY.
+ * intros n; split.
+ + by intros f x.
+ + by intros f g ? x.
+ + by intros f g h ?? x; transitivity (g x).
+ * by intros n f g ? x; apply dist_S.
+ * by intros f g x.
+ * intros c n x; simpl.
+ rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
+ Qed.
+ Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
+
+ Global Instance cofe_mor_car_ne n :
+ Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
+ Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
+ Global Instance cofe_mor_car_proper :
+ Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _.
+ Lemma cofe_mor_ext (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
+ Proof. done. Qed.
+End cofe_mor.
+
+Arguments cofe_mor : clear implicits.
Infix "-n>" := cofe_mor (at level 45, right associativity).
-Instance cofe_more_inhabited (A B : cofeT)
- `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
+Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
+ Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
(** Identity and composition *)
Definition cid {A} : A -n> A := CofeMor id.
@@ -205,46 +228,47 @@ Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
f1 ={n}= f2 → g1 ={n}= g2 → f1 ◎ g1 ={n}= f2 ◎ g2.
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
-(** Pre-composition as a functor *)
-Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n :
- Proper (dist n ==> dist n) (λ g : A -n> C, g ◎ f).
-Proof. by intros g1 g2 ?; apply ccompose_ne. Qed.
-Definition ccompose_l {A B C} (f : B -n> A) : (A -n> C) -n> (B -n> C) :=
- CofeMor (λ g : A -n> C, g ◎ f).
-Instance ccompose_l_ne {A B C} : Proper (dist n ==> dist n) (@ccompose_l A B C).
-Proof. by intros n f1 f2 Hf g x; apply ccompose_ne. Qed.
-
(** unit *)
-Instance unit_dist : Dist unit := λ _ _ _, True.
-Instance unit_compl : Compl unit := λ _, ().
-Instance unit_cofe : Cofe unit.
-Proof. by repeat split; try exists 0. Qed.
+Section unit.
+ Instance unit_dist : Dist unit := λ _ _ _, True.
+ Instance unit_compl : Compl unit := λ _, ().
+ Definition unit_cofe_mixin : CofeMixin unit.
+ Proof. by repeat split; try exists 0. Qed.
+ Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
+End unit.
(** Product *)
-Instance prod_dist `{Dist A, Dist B} : Dist (A * B) := λ n,
- prod_relation (dist n) (dist n).
-Instance pair_ne `{Dist A, Dist B} :
- Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
-Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _.
-Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _.
-Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c,
- (compl (chain_map fst c), compl (chain_map snd c)).
-Instance prod_cofe `{Cofe A, Cofe B} : Cofe (A * B).
-Proof.
- split.
- * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
- rewrite !equiv_dist; naive_solver.
- * apply _.
- * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
- * by split.
- * intros c n; split. apply (conv_compl (chain_map fst c) n).
- apply (conv_compl (chain_map snd c) n).
-Qed.
-Instance pair_timeless `{Dist A, Equiv A, Dist B, Equiv B} (x : A) (y : B) :
- Timeless x → Timeless y → Timeless (x,y).
-Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
-Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B).
-Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n :
+Section product.
+ Context {A B : cofeT}.
+
+ Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
+ Global Instance pair_ne :
+ Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
+ Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _.
+ Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _.
+ Instance prod_compl : Compl (A * B) := λ c,
+ (compl (chain_map fst c), compl (chain_map snd c)).
+ Definition prod_cofe_mixin : CofeMixin (A * B).
+ Proof.
+ split.
+ * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
+ rewrite !equiv_dist; naive_solver.
+ * apply _.
+ * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+ * by split.
+ * intros c n; split. apply (conv_compl (chain_map fst c) n).
+ apply (conv_compl (chain_map snd c) n).
+ Qed.
+ Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
+ Global Instance pair_timeless (x : A) (y : B) :
+ Timeless x → Timeless y → Timeless (x,y).
+ Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
+End product.
+
+Arguments prodC : clear implicits.
+Typeclasses Opaque prod_dist.
+
+Instance prod_map_ne {A A' B B' : cofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
dist n ==> dist n) (@prod_map A A' B B').
Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
@@ -254,15 +278,13 @@ Instance prodC_map_ne {A A' B B'} n :
Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B').
Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
-Typeclasses Opaque prod_dist.
-
(** Discrete cofe *)
Section discrete_cofe.
Context `{Equiv A, @Equivalence A (≡)}.
Instance discrete_dist : Dist A := λ n x y,
match n with 0 => True | S n => x ≡ y end.
Instance discrete_compl : Compl A := λ c, c 1.
- Instance discrete_cofe : Cofe A.
+ Definition discrete_cofe_mixin : CofeMixin A.
Proof.
split.
* intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
@@ -271,9 +293,9 @@ Section discrete_cofe.
* done.
* intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
Qed.
- Global Instance discrete_timeless (x : A) : Timeless x.
+ Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
+ Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
Proof. by intros y. Qed.
- Definition discreteC : cofeT := CofeT A.
End discrete_cofe.
Arguments discreteC _ {_ _}.
@@ -288,16 +310,15 @@ Arguments Later {_} _.
Arguments later_car {_} _.
Section later.
- Instance later_equiv `{Equiv A} : Equiv (later A) := λ x y,
- later_car x ≡ later_car y.
- Instance later_dist `{Dist A} : Dist (later A) := λ n x y,
+ Context {A : cofeT}.
+ Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
+ Instance later_dist : Dist (later A) := λ n x y,
match n with 0 => True | S n => later_car x ={n}= later_car y end.
- Program Definition later_chain `{Dist A} (c : chain (later A)) : chain A :=
+ Program Definition later_chain (c : chain (later A)) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
- Next Obligation. intros A ? c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
- Instance later_compl `{Compl A} : Compl (later A) := λ c,
- Later (compl (later_chain c)).
- Instance later_cofe `{Cofe A} : Cofe (later A).
+ Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
+ Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)).
+ Definition later_cofe_mixin : CofeMixin (later A).
Proof.
split.
* intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
@@ -310,23 +331,25 @@ Section later.
* done.
* intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
Qed.
- Canonical Structure laterC (A : cofeT) : cofeT := CofeT (later A).
-
- Global Instance Later_contractive `{Dist A} : Contractive (@Later A).
+ Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
+ Global Instance Later_contractive : Contractive (@Later A).
Proof. by intros n ??. Qed.
- Definition later_map {A B} (f : A → B) (x : later A) : later B :=
- Later (f (later_car x)).
- Global Instance later_map_ne `{Cofe A, Cofe B} (f : A → B) n :
- Proper (dist (pred n) ==> dist (pred n)) f →
- Proper (dist n ==> dist n) (later_map f) | 0.
- Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
- Lemma later_fmap_id {A} (x : later A) : later_map id x = x.
- Proof. by destruct x. Qed.
- Lemma later_fmap_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
- later_map (g ∘ f) x = later_map g (later_map f x).
- Proof. by destruct x. Qed.
- Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
- CofeMor (later_map f).
- Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
- Proof. intros n f g Hf n'; apply Hf. Qed.
End later.
+
+Arguments laterC : clear implicits.
+
+Definition later_map {A B} (f : A → B) (x : later A) : later B :=
+ Later (f (later_car x)).
+Instance later_map_ne {A B : cofeT} (f : A → B) n :
+ Proper (dist (pred n) ==> dist (pred n)) f →
+ Proper (dist n ==> dist n) (later_map f) | 0.
+Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
+Lemma later_map_id {A} (x : later A) : later_map id x = x.
+Proof. by destruct x. Qed.
+Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
+ later_map (g ∘ f) x = later_map g (later_map f x).
+Proof. by destruct x. Qed.
+Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
+ CofeMor (later_map f).
+Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
+Proof. intros n f g Hf n'; apply Hf. Qed.
diff --git a/modures/cofe_solver.v b/modures/cofe_solver.v
index d9dd6166ec057b6231dc391090a85ce8569734ba..984246d6b68b5b1b7e992b68042925b770a83f30 100644
--- a/modures/cofe_solver.v
+++ b/modures/cofe_solver.v
@@ -2,7 +2,7 @@ Require Export modures.cofe.
Section solver.
Context (F : cofeT → cofeT → cofeT).
-Context `{Finhab : Inhabited (F (CofeT unit) (CofeT unit))}.
+Context `{Finhab : Inhabited (F unitC unitC)}.
Context (map : ∀ {A1 A2 B1 B2 : cofeT},
((A2 -n> A1) * (B1 -n> B2)) → (F A1 B1 -n> F A2 B2)).
Arguments map {_ _ _ _} _.
@@ -20,11 +20,11 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
Fixpoint A (k : nat) : cofeT :=
- match k with 0 => CofeT unit | S k => F (A k) (A k) end.
+ match k with 0 => unitC | S k => F (A k) (A k) end.
Fixpoint f {k} : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
with g {k} : A (S k) -n> A k :=
- match k with 0 => CofeMor (λ _, () : CofeT ()) | S k => map (f,g) end.
+ match k with 0 => CofeMor (λ _, () : unitC) | S k => map (f,g) end.
Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
Lemma gf {k} (x : A k) : g (f x) ≡ x.
@@ -58,7 +58,7 @@ Next Obligation.
rewrite (conv_compl (tower_chain c k) n).
by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
Qed.
-Instance tower_cofe : Cofe tower.
+Definition tower_cofe_mixin : CofeMixin tower.
Proof.
split.
* intros X Y; split; [by intros HXY n k; apply equiv_dist|].
@@ -73,7 +73,7 @@ Proof.
* intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
apply (chain_cauchy c); lia.
Qed.
-Definition T : cofeT := CofeT tower.
+Definition T : cofeT := CofeT tower_cofe_mixin.
Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
match i with 0 => cid | S i => f â—Ž ff i end.
diff --git a/modures/excl.v b/modures/excl.v
index 1014ece16e034d961b3671a701390819ea802aa9..4e84b333b458b4455940386129cd60891b5d9bd4 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -12,8 +12,11 @@ Arguments ExclBot {_}.
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a => Some a | _ => None end.
+Section excl.
+Context {A : cofeT}.
+
(* Cofe *)
-Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
+Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y
| ExclUnit_equiv : ExclUnit ≡ ExclUnit
| ExclBot_equiv : ExclBot ≡ ExclBot.
@@ -24,21 +27,21 @@ Inductive excl_dist `{Dist A} : Dist (excl A) :=
| ExclUnit_dist n : ExclUnit ={n}= ExclUnit
| ExclBot_dist n : ExclBot ={n}= ExclBot.
Existing Instance excl_dist.
-Program Definition excl_chain `{Cofe A}
+Program Definition excl_chain
(c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
{| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
Next Obligation.
- intros A ???? c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
+ intros c x ? n i ?; simpl; destruct (c 1) eqn:?; simplify_equality'.
destruct (decide (i = 0)) as [->|].
{ by replace n with 0 by lia. }
feed inversion (chain_cauchy c 1 i); auto with lia congruence.
feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
Qed.
-Instance excl_compl `{Cofe A} : Compl (excl A) := λ c,
+Instance excl_compl : Compl (excl A) := λ c,
match Some_dec (maybe Excl (c 1)) with
| inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
end.
-Local Instance excl_cofe `{Cofe A} : Cofe (excl A).
+Definition excl_cofe_mixin : CofeMixin (excl A).
Proof.
split.
* intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -61,39 +64,40 @@ Proof.
feed inversion (chain_cauchy c 1 n); auto with lia; constructor.
destruct (c 1); simplify_equality'.
Qed.
-Instance Excl_timeless `{Equiv A, Dist A} (x:A) :Timeless x → Timeless (Excl x).
+Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
+
+Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
-Instance ExclUnit_timeless `{Equiv A, Dist A} : Timeless (@ExclUnit A).
+Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
Proof. by inversion_clear 1; constructor. Qed.
-Instance ExclBot_timeless `{Equiv A, Dist A} : Timeless (@ExclBot A).
+Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
-Instance excl_timeless `{Equiv A, Dist A} :
+Global Instance excl_timeless :
(∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
Proof. intros ? []; apply _. Qed.
(* CMRA *)
-Instance excl_valid {A} : Valid (excl A) := λ x,
+Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ | ExclUnit => True | ExclBot => False end.
-Instance excl_validN {A} : ValidN (excl A) := λ n x,
+Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ | ExclUnit => True | ExclBot => n = 0 end.
-Instance excl_empty {A} : Empty (excl A) := ExclUnit.
-Instance excl_unit {A} : Unit (excl A) := λ _, ∅.
-Instance excl_op {A} : Op (excl A) := λ x y,
+Global Instance excl_empty : Empty (excl A) := ExclUnit.
+Instance excl_unit : Unit (excl A) := λ _, ∅.
+Instance excl_op : Op (excl A) := λ x y,
match x, y with
| Excl x, ExclUnit | ExclUnit, Excl x => Excl x
| ExclUnit, ExclUnit => ExclUnit
| _, _=> ExclBot
end.
-Instance excl_minus {A} : Minus (excl A) := λ x y,
+Instance excl_minus : Minus (excl A) := λ x y,
match x, y with
| _, ExclUnit => x
| Excl _, Excl _ => ExclUnit
| _, _ => ExclBot
end.
-Instance excl_cmra `{Cofe A} : CMRA (excl A).
+Definition excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
- * apply _.
* by intros n []; destruct 1; constructor.
* constructor.
* by destruct 1 as [? []| | |]; intros ?.
@@ -110,9 +114,9 @@ Proof.
* by intros n [?| |] [?| |].
* by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
Qed.
-Instance excl_empty_ra `{Cofe A} : RAIdentity (excl A).
+Global Instance excl_empty_ra : RAIdentity (excl A).
Proof. split. done. by intros []. Qed.
-Instance excl_extend `{Cofe A} : CMRAExtend (excl A).
+Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
Proof.
intros [|n] x y1 y2 ? Hx; [by exists (x,∅); destruct x|].
by exists match y1, y2 with
@@ -121,23 +125,28 @@ Proof.
| ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
Qed.
-Instance excl_valid_timeless {A} (x : excl A) : ValidTimeless x.
+Canonical Structure exclRA : cmraT :=
+ CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Global Instance excl_valid_timeless (x : excl A) : ValidTimeless x.
Proof. by destruct x; intros ?. Qed.
(* Updates *)
-Lemma excl_update {A} (x : A) y : ✓ y → Excl x ⇠y.
+Lemma excl_update (x : A) y : ✓ y → Excl x ⇠y.
Proof. by destruct y; intros ? [?| |]. Qed.
+End excl.
+
+Arguments exclC : clear implicits.
+Arguments exclRA : clear implicits.
(* Functor *)
-Definition exclRA (A : cofeT) : cmraT := CMRAT (excl A).
Instance excl_fmap : FMap excl := λ A B f x,
match x with
| Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
end.
-Instance excl_fmap_cmra_ne `{Dist A, Dist B} n :
+Instance excl_fmap_cmra_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_fmap_cmra_monotone `{Cofe A, Cofe B} :
+Instance excl_fmap_cmra_monotone {A B : cofeT} :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (fmap f : excl A → excl B).
Proof.
split.
@@ -145,7 +154,7 @@ Proof.
by destruct x, z; constructor.
* by intros n [a| |].
Qed.
-Definition exclRA_map {A B : cofeT} (f : A -n> B) : exclRA A -n> exclRA B :=
+Definition exclRA_map {A B} (f : A -n> B) : exclRA A -n> exclRA B :=
CofeMor (fmap f : exclRA A → exclRA B).
Lemma exclRA_map_ne A B n : Proper (dist n ==> dist n) (@exclRA_map A B).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
diff --git a/modures/fin_maps.v b/modures/fin_maps.v
index 9c25aa3320fd3775a3e96b6d9398963d5f3f35c2..a5331a804684f3b0d5e695c21013d52c2b701f3c 100644
--- a/modures/fin_maps.v
+++ b/modures/fin_maps.v
@@ -1,18 +1,17 @@
-Require Export modures.cmra prelude.gmap.
-Require Import modures.option.
+Require Export modures.cmra prelude.gmap modures.option.
-Section map.
-Context `{Countable K}.
+Section cofe.
+Context `{Countable K} {A : cofeT}.
(* COFE *)
-Global Instance map_dist `{Dist A} : Dist (gmap K A) := λ n m1 m2,
+Instance map_dist : Dist (gmap K A) := λ n m1 m2,
∀ i, m1 !! i ={n}= m2 !! i.
-Program Definition map_chain `{Dist A} (c : chain (gmap K A))
+Program Definition map_chain (c : chain (gmap K A))
(k : K) : chain (option A) := {| chain_car n := c n !! k |}.
-Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
-Global Instance map_compl `{Cofe A} : Compl (gmap K A) := λ c,
+Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
+Instance map_compl : Compl (gmap K A) := λ c,
map_imap (λ i _, compl (map_chain c i)) (c 1).
-Global Instance map_cofe `{Cofe A} : Cofe (gmap K A).
+Definition map_cofe_mixin : CofeMixin (gmap K A).
Proof.
split.
* intros m1 m2; split.
@@ -29,30 +28,32 @@ Proof.
feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
by rewrite conv_compl; simpl; apply reflexive_eq.
Qed.
-Global Instance lookup_ne `{Dist A} n k :
+Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
+
+Global Instance lookup_ne n k :
Proper (dist n ==> dist n) (lookup k : gmap K A → option A).
Proof. by intros m1 m2. Qed.
-Global Instance insert_ne `{Dist A} (i : K) n :
+Global Instance insert_ne (i : K) n :
Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
Proof.
intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
[by constructor|by apply lookup_ne].
Qed.
-Global Instance singleton_ne `{Cofe A} (i : K) n :
+Global Instance singleton_ne (i : K) n :
Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
Proof. by intros ???; apply insert_ne. Qed.
-Global Instance delete_ne `{Dist A} (i : K) n :
+Global Instance delete_ne (i : K) n :
Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
Proof.
intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
[by constructor|by apply lookup_ne].
Qed.
-Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless (∅ : gmap K A).
+Global Instance map_empty_timeless : Timeless (∅ : gmap K A).
Proof.
intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
inversion_clear Hm; constructor.
Qed.
-Global Instance map_lookup_timeless `{Cofe A} (m : gmap K A) i :
+Global Instance map_lookup_timeless (m : gmap K A) i :
Timeless m → Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
@@ -60,51 +61,41 @@ Proof.
by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
-Global Instance map_ra_insert_timeless `{Cofe A} (m : gmap K A) i x :
+Global Instance map_ra_insert_timeless (m : gmap K A) i x :
Timeless x → Timeless m → Timeless (<[i:=x]>m).
Proof.
intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
{ by apply (timeless _); rewrite -Hm lookup_insert. }
by apply (timeless _); rewrite -Hm lookup_insert_ne.
Qed.
-Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
+Global Instance map_ra_singleton_timeless (i : K) (x : A) :
Timeless x → Timeless ({[ i ↦ x ]} : gmap K A) := _.
-Global Instance map_fmap_ne `{Dist A, Dist B} (f : A → B) n :
- Proper (dist n ==> dist n) f →
- Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
-Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Canonical Structure mapC (A : cofeT) : cofeT := CofeT (gmap K A).
-Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
- CofeMor (fmap f : mapC A → mapC B).
-Global Instance mapC_map_ne {A B} n :
- Proper (dist n ==> dist n) (@mapC_map A B).
-Proof.
- intros f g Hf m k; rewrite /= !lookup_fmap.
- destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
-Qed.
+End cofe.
+Arguments mapC _ {_ _} _.
(* CMRA *)
-Global Instance map_op `{Op A} : Op (gmap K A) := merge op.
-Global Instance map_unit `{Unit A} : Unit (gmap K A) := fmap unit.
-Global Instance map_valid `{Valid A} : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
-Global Instance map_validN `{ValidN A} : ValidN (gmap K A) := λ n m,
- ∀ i, ✓{n} (m!!i).
-Global Instance map_minus `{Minus A} : Minus (gmap K A) := merge minus.
-Lemma lookup_op `{Op A} m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
+Section cmra.
+Context `{Countable K} {A : cmraT}.
+
+Instance map_op : Op (gmap K A) := merge op.
+Instance map_unit : Unit (gmap K A) := fmap unit.
+Instance map_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
+Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m!!i).
+Instance map_minus : Minus (gmap K A) := merge minus.
+Lemma lookup_op m1 m2 i : (m1 â‹… m2) !! i = m1 !! i â‹… m2 !! i.
Proof. by apply lookup_merge. Qed.
-Lemma lookup_minus `{Minus A} m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
+Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
Proof. by apply lookup_merge. Qed.
-Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i).
+Lemma lookup_unit m i : unit m !! i = unit (m !! i).
Proof. by apply lookup_fmap. Qed.
-Lemma map_included_spec `{CMRA A} (m1 m2 : gmap K A) :
- m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
+Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
Proof.
split.
* by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
* intros Hm; exists (m2 ⩪ m1); intros i.
by rewrite lookup_op lookup_minus ra_op_minus.
Qed.
-Lemma map_includedN_spec `{CMRA A} (m1 m2 : gmap K A) n :
+Lemma map_includedN_spec (m1 m2 : gmap K A) n :
m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
Proof.
split.
@@ -112,10 +103,9 @@ Proof.
* intros Hm; exists (m2 ⩪ m1); intros i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
-Global Instance map_cmra `{CMRA A} : CMRA (gmap K A).
+Definition map_cmra_mixin : CMRAMixin (gmap K A).
Proof.
split.
- * apply _.
* by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
* by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
* by intros n m1 m2 Hm ? i; rewrite -(Hm i).
@@ -135,13 +125,13 @@ Proof.
* intros x y n; rewrite map_includedN_spec; intros ? i.
by rewrite lookup_op lookup_minus cmra_op_minus.
Qed.
-Global Instance map_ra_empty `{RA A} : RAIdentity (gmap K A).
+Global Instance map_ra_empty : RAIdentity (gmap K A).
Proof.
split.
* by intros ?; rewrite lookup_empty.
- * by intros m i; rewrite /= lookup_op lookup_empty; destruct (m !! i).
+ * by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
Qed.
-Global Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (gmap K A).
+Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
Proof.
intros n m m1 m2 Hm Hm12.
assert (∀ i, m !! i ={n}= m1 !! i ⋅ m2 !! i) as Hm12'
@@ -150,20 +140,21 @@ Proof.
set (f_proj i := proj1_sig (f i)).
exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
- * destruct (m !! i) as [x|] eqn:Hx; simpl; [|constructor].
+ * destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
rewrite -Hx; apply (proj2_sig (f i)).
- * destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
+ * destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
- by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
+ by symmetry; apply option_op_positive_dist_l with (m2 !! i).
* destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
- by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''.
+ by symmetry; apply option_op_positive_dist_r with (m1 !! i).
Qed.
-Global Instance map_empty_valid_timeless `{Valid A, ValidN A} :
- ValidTimeless (∅ : gmap K A).
+Canonical Structure mapRA : cmraT :=
+ CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
+
+Global Instance map_empty_valid_timeless : ValidTimeless (∅ : gmap K A).
Proof. by intros ??; rewrite lookup_empty. Qed.
-Global Instance map_ra_insert_valid_timeless `{Valid A, ValidN A}
- (m : gmap K A) i x:
+Global Instance map_ra_insert_valid_timeless (m : gmap K A) i x:
ValidTimeless x → ValidTimeless m → m !! i = None →
ValidTimeless (<[i:=x]>m).
Proof.
@@ -173,48 +164,40 @@ Proof.
intros j; destruct (decide (i = j)); simplify_map_equality;[by rewrite Hi|].
by specialize (Hm j); simplify_map_equality.
Qed.
-Global Instance map_ra_singleton_valid_timeless `{Valid A, ValidN A} (i : K) x :
- ValidTimeless x → ValidTimeless ({[ i ↦ x ]} : gmap K A).
+Global Instance map_ra_singleton_valid_timeless (i : K) x :
+ ValidTimeless x → ValidTimeless {[ i ↦ x ]}.
Proof.
intros ?; apply (map_ra_insert_valid_timeless _ _ _ _ _).
by rewrite lookup_empty.
Qed.
-Lemma map_insert_valid `{ValidN A} (m : gmap K A) n i x :
- ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
+End cmra.
+Arguments mapRA _ {_ _} _.
+
+Section properties.
+Context `{Countable K} {A: cmraT}.
+
+Lemma map_insert_valid (m :gmap K A) n i x : ✓{n} x → ✓{n} m → ✓{n} (<[i:=x]>m).
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
-Lemma map_insert_op `{Op A} (m1 m2 : gmap K A) i x :
+Lemma map_insert_op (m1 m2 : gmap K A) i x :
m2 !! i = None → <[i:=x]>(m1 ⋅ m2) = <[i:=x]>m1 ⋅ m2.
-Proof. by intros Hi; apply (insert_merge_l _); rewrite Hi. Qed.
-Lemma map_singleton_op `{Op A} (i : K) (x y : A) :
- ({[ i ↦ x ⋅ y ]} : gmap K A) = {[ i ↦ x ]} ⋅ {[ i ↦ y ]}.
-Proof. by apply symmetry, merge_singleton. Qed.
-
-Canonical Structure mapRA (A : cmraT) : cmraT := CMRAT (gmap K A).
-Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
- `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
-Proof.
- split.
- * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
- by rewrite !lookup_fmap; apply includedN_preserving.
- * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
-Qed.
-Definition mapRA_map {A B : cmraT} (f : A -n> B) : mapRA A -n> mapRA B :=
- CofeMor (fmap f : mapRA A → mapRA B).
-Global Instance mapRA_map_ne {A B} n :
- Proper (dist n ==> dist n) (@mapRA_map A B) := mapC_map_ne n.
-Global Instance mapRA_map_monotone {A B : cmraT} (f : A -n> B)
- `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
+Proof. by intros Hi; apply (insert_merge_l _ m1 m2); rewrite Hi. Qed.
+Lemma map_unit_singleton (i : K) (x : A) :
+ unit ({[ i ↦ x ]} : gmap K A) = {[ i ↦ unit x ]}.
+Proof. apply map_fmap_singleton. Qed.
+Lemma map_op_singleton (i : K) (x y : A) :
+ {[ i ↦ x ]} ⋅ {[ i ↦ y ]} = ({[ i ↦ x ⋅ y ]} : gmap K A).
+Proof. by apply (merge_singleton _ _ _ x y). Qed.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma map_dom_op `{Op A} (m1 m2 : gmap K A) :
+Lemma map_dom_op (m1 m2 : gmap K A) :
dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
Proof.
apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
unfold is_Some; setoid_rewrite lookup_op.
destruct (m1 !! i), (m2 !! i); naive_solver.
Qed.
-Lemma map_update_alloc `{CMRA A} (m : gmap K A) x :
+Lemma map_update_alloc (m : gmap K A) x :
✓ x → m â‡: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
Proof.
intros ? mf n Hm. set (i := fresh (dom (gset K) (m â‹… mf))).
@@ -225,6 +208,31 @@ Proof.
* rewrite -map_insert_op; last by apply not_elem_of_dom.
by apply map_insert_valid; [apply cmra_valid_validN|].
Qed.
-End map.
-Arguments mapC _ {_ _} _.
-Arguments mapRA _ {_ _} _.
+End properties.
+
+Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n :
+ Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
+Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
+Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
+ CofeMor (fmap f : mapC K A → mapC K B).
+Instance mapC_map_ne `{Countable K} {A B} n :
+ Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
+Proof.
+ intros f g Hf m k; rewrite /= !lookup_fmap.
+ destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
+Qed.
+
+Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
+ `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
+Proof.
+ split.
+ * intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
+ by rewrite !lookup_fmap; apply: includedN_preserving.
+ * by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
+Qed.
+Definition mapRA_map `{Countable K} {A B : cmraT} (f : A -n> B) :
+ mapRA K A -n> mapRA K B := CofeMor (fmap f : mapRA K A → mapRA K B).
+Instance mapRA_map_ne `{Countable K} {A B} n :
+ Proper (dist n ==> dist n) (@mapRA_map K _ _ A B) := mapC_map_ne n.
+Instance mapRA_map_monotone `{Countable K} {A B : cmraT} (f : A -n> B)
+ `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _.
diff --git a/modures/logic.v b/modures/logic.v
index c717b2b87505e6c09527e6c0e150011df064c7b1..791a9366fd5138eecca0ae68926020fbfdebb7e8 100644
--- a/modures/logic.v
+++ b/modures/logic.v
@@ -15,36 +15,41 @@ Hint Resolve uPred_0.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
-Instance uPred_equiv (M : cmraT) : Equiv (uPred M) := λ P Q, ∀ x n,
- ✓{n} x → P n x ↔ Q n x.
-Instance uPred_dist (M : cmraT) : Dist (uPred M) := λ n P Q, ∀ x n',
- n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
-Program Instance uPred_compl (M : cmraT) : Compl (uPred M) := λ c,
- {| uPred_holds n x := c n n x |}.
-Next Obligation. by intros M c x y n ??; simpl in *; apply uPred_ne with x. Qed.
-Next Obligation. by intros M c x; simpl. Qed.
-Next Obligation.
- intros M c x1 x2 n1 n2 ????; simpl in *.
- apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
-Qed.
-Instance uPred_cofe (M : cmraT) : Cofe (uPred M).
-Proof.
- split.
- * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
- intros HPQ x n ?; apply HPQ with n; auto.
- * intros n; split.
- + by intros P x i.
- + by intros P Q HPQ x i ??; symmetry; apply HPQ.
- + by intros P Q Q' HP HQ x i ??; transitivity (Q i x); [apply HP|apply HQ].
- * intros n P Q HPQ x i ??; apply HPQ; auto.
- * intros P Q x i; rewrite Nat.le_0_r; intros ->; split; intros; apply uPred_0.
- * by intros c n x i ??; apply (chain_cauchy c i n).
-Qed.
+Section cofe.
+ Context {M : cmraT}.
+ Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ x n,
+ ✓{n} x → P n x ↔ Q n x.
+ Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ x n',
+ n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
+ Program Instance uPred_compl : Compl (uPred M) := λ c,
+ {| uPred_holds n x := c n n x |}.
+ Next Obligation. by intros c x y n ??; simpl in *; apply uPred_ne with x. Qed.
+ Next Obligation. by intros c x; simpl. Qed.
+ Next Obligation.
+ intros c x1 x2 n1 n2 ????; simpl in *.
+ apply (chain_cauchy c n2 n1); eauto using uPred_weaken.
+ Qed.
+ Definition uPred_cofe_mixin : CofeMixin (uPred M).
+ Proof.
+ split.
+ * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
+ intros HPQ x n ?; apply HPQ with n; auto.
+ * intros n; split.
+ + by intros P x i.
+ + by intros P Q HPQ x i ??; symmetry; apply HPQ.
+ + by intros P Q Q' HP HQ x i ??; transitivity (Q i x); [apply HP|apply HQ].
+ * intros n P Q HPQ x i ??; apply HPQ; auto.
+ * intros P Q x i; rewrite Nat.le_0_r; intros ->; split; intros; apply uPred_0.
+ * by intros c n x i ??; apply (chain_cauchy c i n).
+ Qed.
+ Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
+End cofe.
+Arguments uPredC : clear implicits.
+
Instance uPred_holds_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
Instance uPred_holds_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_holds_ne, equiv_dist. Qed.
-Canonical Structure uPredC (M : cmraT) : cofeT := CofeT (uPred M).
(** functor *)
Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1)
@@ -125,7 +130,7 @@ Next Obligation. by intros M P Q x; exists x, x. Qed.
Next Obligation.
intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??.
assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
- { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using ra_included_l.
+ { destruct Hxy as [z Hy]; exists (x2 â‹… z); split; eauto using @ra_included_l.
apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. }
exists x1, x2'; split_ands; [done| |].
* cofe_subst y; apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l.
@@ -144,7 +149,7 @@ Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed.
Next Obligation.
intros M P Q x1 x2 n1 n2 HPQ ??? x3 n3 ???; simpl in *.
apply uPred_weaken with (x1 â‹… x3) n3;
- eauto using cmra_valid_included, ra_preserving_r.
+ eauto using cmra_valid_included, @ra_preserving_r.
Qed.
Program Definition uPred_later {M} (P : uPred M) : uPred M :=
@@ -160,7 +165,7 @@ Next Obligation. by intros M P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
Next Obligation. by intros; simpl. Qed.
Next Obligation.
intros M P x1 x2 n1 n2 ????; eapply uPred_weaken with (unit x1) n1;
- auto using ra_unit_preserving, cmra_unit_valid.
+ eauto using @ra_unit_preserving, cmra_unit_valid.
Qed.
Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
@@ -480,7 +485,7 @@ Qed.
Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
Proof.
intros P x n Hvalid; split.
- * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, ra_included_r.
+ * intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, @ra_included_r.
* by destruct n as [|n]; [|intros ?; exists (unit x), x; rewrite ra_unit_l].
Qed.
Global Instance sep_commutative : Commutative (≡) (@uPred_sep M).
@@ -555,11 +560,11 @@ Proof. by apply forall_intro; intros a; rewrite ->forall_elim. Qed.
(* Later *)
Lemma later_mono P Q : P ⊆ Q → (▷ P)%I ⊆ (▷ Q)%I.
-Proof. intros HP x [|n] ??; [done|apply HP; auto using cmra_valid_S]. Qed.
+Proof. intros HP x [|n] ??; [done|apply HP; eauto using cmra_valid_S]. Qed.
Lemma later_intro P : P ⊆ (▷ P)%I.
Proof.
intros x [|n] ??; simpl in *; [done|].
- apply uPred_weaken with x (S n); auto using cmra_valid_S.
+ apply uPred_weaken with x (S n); eauto using cmra_valid_S.
Qed.
Lemma lub P : (▷ P → P)%I ⊆ P.
Proof.
@@ -582,10 +587,10 @@ Proof.
intros x n ?; split.
* destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)].
destruct (cmra_extend_op n x x1 x2)
- as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
+ as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_valid_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
* destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
- exists x1, x2; eauto using (dist_S (A:=M)).
+ exists x1, x2; eauto using dist_S.
Qed.
(* Later derived *)
@@ -604,7 +609,8 @@ Lemma always_const (P : Prop) : (□ uPred_const P : uPred M)%I ≡ uPred_const
Proof. done. Qed.
Lemma always_elim P : (□ P)%I ⊆ P.
Proof.
- intros x n ??; apply uPred_weaken with (unit x) n;auto using ra_included_unit.
+ intros x n ??; apply uPred_weaken with (unit x) n;
+ eauto using @ra_included_unit.
Qed.
Lemma always_intro P Q : (□ P)%I ⊆ Q → (□ P)%I ⊆ (□ Q)%I.
Proof.
diff --git a/modures/option.v b/modures/option.v
index aec24387ae421e6826a2729e93c6bd58b3dd5303..2df111ca30ce3a8e2f2061c30c771963601ce534 100644
--- a/modures/option.v
+++ b/modures/option.v
@@ -1,25 +1,27 @@
Require Export modures.cmra.
(* COFE *)
-Inductive option_dist `{Dist A} : Dist (option A) :=
+Section cofe.
+Context {A : cofeT}.
+Inductive option_dist : Dist (option A) :=
| option_0_dist (x y : option A) : x ={0}= y
| Some_dist n x y : x ={n}= y → Some x ={n}= Some y
| None_dist n : None ={n}= None.
Existing Instance option_dist.
-Program Definition option_chain `{Cofe A}
+Program Definition option_chain
(c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
{| chain_car n := from_option x (c n) |}.
Next Obligation.
- intros A ???? c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
+ intros c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
{ by replace n with 0 by lia. }
feed inversion (chain_cauchy c 1 i); auto with lia congruence.
feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
Qed.
-Instance option_compl `{Cofe A} : Compl (option A) := λ c,
+Instance option_compl : Compl (option A) := λ c,
match Some_dec (c 1) with
| inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
end.
-Instance option_cofe `{Cofe A} : Cofe (option A).
+Definition option_cofe_mixin : CofeMixin (option A).
Proof.
split.
* intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
@@ -40,28 +42,36 @@ Proof.
by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
Qed.
-Instance Some_ne `{Dist A} : Proper (dist n ==> dist n) Some.
+Canonical Structure optionC := CofeT option_cofe_mixin.
+Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
Proof. by constructor. Qed.
-Instance None_timeless `{Dist A, Equiv A} : Timeless (@None A).
+Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
-Instance Some_timeless `{Dist A, Equiv A} x : Timeless x → Timeless (Some x).
+Global Instance Some_timeless x : Timeless x → Timeless (Some x).
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
-Instance option_fmap_ne `{Dist A, Dist B} (f : A → B) n:
+End cofe.
+
+Arguments optionC : clear implicits.
+
+Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
-Instance is_Some_ne `{Dist A} : Proper (dist (S n) ==> iff) (@is_Some A).
+Instance is_Some_ne `{A : cofeT} : Proper (dist (S n) ==> iff) (@is_Some A).
Proof. intros n; inversion_clear 1; split; eauto. Qed.
(* CMRA *)
-Instance option_valid `{Valid A} : Valid (option A) := λ mx,
+Section cmra.
+Context {A : cmraT}.
+
+Instance option_valid : Valid (option A) := λ mx,
match mx with Some x => ✓ x | None => True end.
-Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx,
+Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => ✓{n} x | None => True end.
-Instance option_unit `{Unit A} : Unit (option A) := fmap unit.
-Instance option_op `{Op A} : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
-Instance option_minus `{Minus A} : Minus (option A) :=
+Instance option_unit : Unit (option A) := fmap unit.
+Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
+Instance option_minus : Minus (option A) :=
difference_with (λ x y, Some (x ⩪ y)).
-Lemma option_included `{CMRA A} mx my :
+Lemma option_included mx my :
mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y.
Proof.
split.
@@ -72,7 +82,7 @@ Proof.
* intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
-Lemma option_includedN `{CMRA A} n mx my :
+Lemma option_includedN n (mx my : option A) :
mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
Proof.
split.
@@ -80,15 +90,14 @@ Proof.
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
- cofe_subst; auto using cmra_included_l.
+ cofe_subst; eauto using @cmra_included_l.
* intros [->|[->|(x&y&->&->&z&Hz)]];
try (by exists my; destruct my; constructor).
by exists (Some z); constructor.
Qed.
-Instance option_cmra `{CMRA A} : CMRA (option A).
+Definition option_cmra_mixin : CMRAMixin (option A).
Proof.
split.
- * apply _.
* by intros n [x|]; destruct 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
@@ -98,22 +107,22 @@ Proof.
* by destruct 1; inversion_clear 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* intros [x|]; unfold validN, option_validN; auto using cmra_valid_0.
- * intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S.
+ * intros n [x|]; unfold validN, option_validN; eauto using @cmra_valid_S.
* by intros [x|]; unfold valid, validN, option_validN, option_valid;
- auto using cmra_valid_validN.
+ eauto using cmra_valid_validN.
* intros [x|] [y|] [z|]; constructor; rewrite ?(associative _); auto.
* intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto.
- * by intros [x|]; constructor; rewrite cmra_unit_l.
- * by intros [x|]; constructor; rewrite cmra_unit_idempotent.
+ * by intros [x|]; constructor; rewrite ra_unit_l.
+ * by intros [x|]; constructor; rewrite ra_unit_idempotent.
* intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto.
- do 2 right; exists (unit x), (unit y); eauto using cmra_unit_preserving.
+ do 2 right; exists (unit x), (unit y); eauto using @cmra_unit_preserving.
* intros n [x|] [y|]; unfold validN, option_validN; simpl;
- eauto using cmra_valid_op_l.
+ eauto using @cmra_valid_op_l.
* intros n mx my; rewrite option_includedN.
intros [->|[->|(x&y&->&->&?)]]; [done|by destruct my|].
by constructor; apply cmra_op_minus.
Qed.
-Instance option_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (option A).
+Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
Proof.
intros n mx my1 my2; destruct (decide (n = 0)) as [->|].
{ by exists (mx, None); repeat constructor; destruct mx; constructor. }
@@ -126,17 +135,28 @@ Proof.
* by exists (None,Some x); inversion Hx'; repeat constructor.
* exists (None,None); repeat constructor.
Qed.
-Instance None_valid_timeless `{Valid A, ValidN A} : ValidTimeless (@None A).
+Canonical Structure optionRA :=
+ CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
+
+Lemma option_op_positive_dist_l n x y : x ⋅ y ={n}= None → x ={n}= None.
+Proof. by destruct x, y; inversion_clear 1. Qed.
+Lemma option_op_positive_dist_r n x y : x ⋅ y ={n}= None → y ={n}= None.
+Proof. by destruct x, y; inversion_clear 1. Qed.
+
+Global Instance None_valid_timeless : ValidTimeless (@None A).
Proof. done. Qed.
-Instance Some_valid_timeless `{Valid A, ValidN A} x :
+Global Instance Some_valid_timeless x :
ValidTimeless x → ValidTimeless (Some x).
Proof. by intros ? y; apply (valid_timeless x). Qed.
-Instance option_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B)
- `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B).
+End cmra.
+
+Arguments optionRA : clear implicits.
+
+Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
+ CMRAMonotone (fmap f : option A → option B).
Proof.
split.
* intros n mx my; rewrite !option_includedN.
intros [->|[->|(x&y&->&->&?)]]; simpl; eauto 10 using @includedN_preserving.
- * by intros n [x|] ?;
- unfold validN, option_validN; simpl; try apply validN_preserving.
-Qed.
\ No newline at end of file
+ * by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
+Qed.