Commit c05f2a06 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove CMRA division.

The only drawback is that we have to restrict iprod to finite types,
but that is fine.
parent e15c090e
......@@ -61,7 +61,6 @@ Program Instance agree_op : Op (agree A) := λ x y,
agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_core : Core (agree A) := id.
Instance agree_div : Div (agree A) := λ x y, x.
Instance: Comm () (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
......@@ -108,13 +107,11 @@ Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
- by intros n x1 x2 Hx y1 y2 Hy.
- 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_idemp.
- by intros n x y [(?&?&?) ?].
- by intros x y; rewrite agree_included.
- intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
......
......@@ -73,7 +73,7 @@ Implicit Types x y : auth A.
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
| Excl a => ( n, own x {n} a) a
| ExclUnit => own x
| ExclBot => False
end.
......@@ -89,8 +89,6 @@ Instance auth_core : Core (auth A) := λ x,
Auth (core (authoritative x)) (core (own x)).
Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x authoritative y) (own x own y).
Instance auth_div : Div (auth A) := λ x y,
Auth (authoritative x ÷ authoritative y) (own x ÷ own y).
Lemma auth_included (x y : auth A) :
x y authoritative x authoritative y own x own y.
......@@ -110,8 +108,6 @@ Proof.
- by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
- intros n [x a] [y b] [Hx Ha]; simpl in *;
destruct Hx; intros ?; cofe_subst; auto.
- by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
- intros [[] ?]; rewrite /= ?cmra_included_includedN ?cmra_valid_validN;
naive_solver eauto using O.
- intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
......@@ -125,8 +121,6 @@ Proof.
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[a1| |] b1] [[a2| |] b2];
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- by intros ??; rewrite auth_included;
intros [??]; split; simpl; apply cmra_op_div.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (authoritative x) (authoritative y1)
(authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
......@@ -138,9 +132,9 @@ Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A CMRADiscrete authR.
Proof.
split; first apply _.
intros [[] ?]; by rewrite /= /cmra_valid /cmra_validN /=
-?cmra_discrete_included_iff -?cmra_discrete_valid_iff.
Qed.
intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=
-?cmra_discrete_included_iff -?cmra_discrete_valid_iff; auto.
Admitted.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
......
......@@ -14,10 +14,6 @@ Notation "(≼)" := included (only parsing) : C_scope.
Hint Extern 0 (_ _) => reflexivity.
Instance: Params (@included) 3.
Class Div (A : Type) := div : A A A.
Instance: Params (@div) 2.
Infix "÷" := div : C_scope.
Class ValidN (A : Type) := validN : nat A Prop.
Instance: Params (@validN) 3.
Notation "✓{ n } x" := (validN n x)
......@@ -33,13 +29,11 @@ Notation "x ≼{ n } y" := (includedN n x y)
Instance: Params (@includedN) 4.
Hint Extern 0 (_ {_} _) => reflexivity.
Record CMRAMixin A
`{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A, Div A} := {
Record CMRAMixin A `{Dist A, Equiv A, Core A, Op A, Valid A, ValidN A} := {
(* setoids *)
mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
mixin_cmra_core_ne n : Proper (dist n ==> dist n) core;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
mixin_cmra_div_ne n : Proper (dist n ==> dist n ==> dist n) div;
(* valid *)
mixin_cmra_valid_validN x : x n, {n} x;
mixin_cmra_validN_S n x : {S n} x {n} x;
......@@ -50,7 +44,6 @@ Record CMRAMixin A
mixin_cmra_core_idemp x : core (core x) core x;
mixin_cmra_core_preserving x y : x y core x core y;
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x;
mixin_cmra_op_div x y : x y x y ÷ x y;
mixin_cmra_extend n x y1 y2 :
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }
......@@ -66,11 +59,10 @@ Structure cmraT := CMRAT {
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_div : Div cmra_car;
cmra_cofe_mixin : CofeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car
}.
Arguments CMRAT {_ _ _ _ _ _ _ _ _} _ _.
Arguments CMRAT {_ _ _ _ _ _ _ _} _ _.
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never.
......@@ -79,11 +71,10 @@ Arguments cmra_core : simpl never.
Arguments cmra_op : simpl never.
Arguments cmra_valid : simpl never.
Arguments cmra_validN : simpl never.
Arguments cmra_div : simpl never.
Arguments cmra_cofe_mixin : simpl never.
Arguments cmra_mixin : simpl never.
Add Printing Constructor cmraT.
Existing Instances cmra_core cmra_op cmra_valid cmra_validN cmra_div.
Existing Instances cmra_core cmra_op cmra_valid cmra_validN.
Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT (cmra_cofe_mixin A).
Canonical Structure cmra_cofeC.
......@@ -97,9 +88,6 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_core_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_validN_ne n : Proper (dist n ==> impl) (@validN A _ n).
Proof. apply (mixin_cmra_validN_ne _ (cmra_mixin A)). Qed.
Global Instance cmra_div_ne n :
Proper (dist n ==> dist n ==> dist n) (@div A _).
Proof. apply (mixin_cmra_div_ne _ (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_validN_S n x : {S n} x {n} x.
......@@ -116,8 +104,6 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_core_preserving _ (cmra_mixin A)). Qed.
Lemma cmra_validN_op_l n x y : {n} (x y) {n} x.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_op_div x y : x y x y ÷ x y.
Proof. apply (mixin_cmra_op_div _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 :
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }.
......@@ -188,8 +174,6 @@ Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
Proof. by split; apply cmra_validN_ne. Qed.
Global Instance cmra_validN_proper : Proper (() ==> iff) (@validN A _ n) | 1.
Proof. by intros n x1 x2 Hx; apply cmra_validN_ne', equiv_dist. Qed.
Global Instance cmra_div_proper : Proper (() ==> () ==> ()) (@div A _).
Proof. apply (ne_proper_2 _). Qed.
Global Instance cmra_valid_proper : Proper (() ==> iff) (@valid A _).
Proof.
......@@ -246,17 +230,9 @@ Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_core_valid x : x core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_valid_op_l. Qed.
(** ** Div *)
Lemma cmra_op_div' n x y : x {n} y x y ÷ x {n} y.
Proof. intros [z ->]. by rewrite cmra_op_div; last exists z. Qed.
(** ** Order *)
Lemma cmra_included_includedN x y : x y n, x {n} y.
Proof.
split; [by intros [z Hz] n; exists z; rewrite Hz|].
intros Hxy; exists (y ÷ x); apply equiv_dist=> n.
by rewrite cmra_op_div'.
Qed.
Lemma cmra_included_includedN n x y : x y x {n} y.
Proof. intros [z ->]. by exists z. Qed.
Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n).
Proof.
split.
......@@ -266,13 +242,15 @@ Proof.
Qed.
Global Instance cmra_included_preorder: PreOrder (@included A _ _).
Proof.
split; red; intros until 0; rewrite !cmra_included_includedN; first done.
intros; etrans; eauto.
split.
- by intros x; exists (core x); rewrite cmra_core_r.
- intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2).
by rewrite assoc -Hy -Hz.
Qed.
Lemma cmra_validN_includedN n x y : {n} y x {n} y {n} x.
Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included n x y : {n} y x y {n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
Proof. intros Hyv [z ?]; setoid_subst; eauto using cmra_validN_op_l. Qed.
Lemma cmra_includedN_S n x y : x {S n} y x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
......@@ -337,7 +315,7 @@ Proof.
Qed.
Lemma cmra_discrete_included_iff `{Discrete A} n x y : x y x {n} y.
Proof.
split; first by rewrite cmra_included_includedN.
split; first by apply cmra_included_includedN.
intros [z ->%(timeless_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_updateP `{CMRADiscrete A} (x : A) (P : A Prop) :
......@@ -486,25 +464,23 @@ End cmra_transport.
(** * Instances *)
(** ** Discrete CMRA *)
Class RA A `{Equiv A, Core A, Op A, Valid A, Div A} := {
Class RA A `{Equiv A, Core A, Op A, Valid A} := {
(* setoids *)
ra_op_ne (x : A) : Proper (() ==> ()) (op x);
ra_core_ne :> Proper (() ==> ()) core;
ra_validN_ne :> Proper (() ==> impl) valid;
ra_div_ne :> Proper (() ==> () ==> ()) div;
(* monoid *)
ra_assoc :> Assoc () ();
ra_comm :> Comm () ();
ra_core_l x : core x x x;
ra_core_idemp x : core (core x) core x;
ra_core_preserving x y : x y core x core y;
ra_valid_op_l x y : (x y) x;
ra_op_div x y : x y x y ÷ x y
ra_valid_op_l x y : (x y) x
}.
Section discrete.
Context {A : cofeT} `{Discrete A}.
Context `{Core A, Op A, Valid A, Div A} (ra : RA A).
Context `{Core A, Op A, Valid A} (ra : RA A).
Instance discrete_validN : ValidN A := λ n x, x.
Definition discrete_cmra_mixin : CMRAMixin A.
......@@ -525,7 +501,6 @@ Section unit.
Instance unit_valid : Valid () := λ x, True.
Instance unit_core : Core () := λ x, x.
Instance unit_op : Op () := λ x y, ().
Instance unit_div : Div () := λ x y, ().
Global Instance unit_empty : Empty () := ().
Definition unit_ra : RA ().
Proof. by split. Qed.
......@@ -544,7 +519,6 @@ Section prod.
Instance prod_core : Core (A * B) := λ x, (core (x.1), core (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_div : Div (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|].
......@@ -561,8 +535,6 @@ Section prod.
- 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.
- intros x; split.
+ intros [??] n; split; by apply cmra_valid_validN.
+ intros Hxy; split; apply cmra_valid_validN=> n; apply Hxy.
......@@ -574,8 +546,6 @@ Section prod.
- intros x y; rewrite !prod_included.
by intros [??]; split; apply cmra_core_preserving.
- intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- intros x y; rewrite prod_included; intros [??].
by split; apply cmra_op_div.
- intros n x y1 y2 [??] [??]; simpl in *.
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
......
......@@ -27,7 +27,6 @@ Instance dec_agree_op : Op (dec_agree A) := λ x y,
| _, _ => DecAgreeBot
end.
Instance dec_agree_core : Core (dec_agree A) := id.
Instance dec_agree_div : Div (dec_agree A) := λ x y, x.
Definition dec_agree_ra : RA (dec_agree A).
Proof.
......@@ -35,15 +34,12 @@ Proof.
- apply _.
- apply _.
- apply _.
- apply _.
- intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- intros [?|]; by repeat (simplify_eq/= || case_match).
- by intros [?|] [?|] ?.
- by intros [?|] [?|] ?.
- intros [?|] [?|] [[?|]]; fold_leibniz;
intros; by repeat (simplify_eq/= || case_match).
Qed.
Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
......
......@@ -6,6 +6,7 @@ Record validity {A} (P : A → Prop) : Type := Validity {
validity_is_valid : Prop;
validity_prf : validity_is_valid P validity_car
}.
Add Printing Constructor validity.
Arguments Validity {_ _} _ _ _.
Arguments validity_car {_ _} _.
Arguments validity_is_valid {_ _} _.
......@@ -13,23 +14,16 @@ Arguments validity_is_valid {_ _} _.
Definition to_validity {A} {P : A Prop} (x : A) : validity P :=
Validity x (P x) id.
Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
z, y x z z x z.
Instance: Params (@dra_included) 4.
Local Infix "≼" := dra_included.
Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A} := {
(* setoids *)
dra_equivalence :> Equivalence (() : relation A);
dra_op_proper :> Proper (() ==> () ==> ()) ();
dra_core_proper :> Proper (() ==> ()) core;
dra_valid_proper :> Proper (() ==> impl) valid;
dra_disjoint_proper :> x, Proper (() ==> impl) (disjoint x);
dra_div_proper :> Proper (() ==> () ==> ()) div;
(* validity *)
dra_op_valid x y : x y x y (x y);
dra_core_valid x : x core x;
dra_div_valid x y : x y x y (y ÷ x);
(* monoid *)
dra_assoc :> Assoc () ();
dra_disjoint_ll x y z : x y z x y x y z x z;
......@@ -39,9 +33,8 @@ Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := {
dra_core_disjoint_l x : x core x x;
dra_core_l x : x core x x x;
dra_core_idemp x : x core (core x) core x;
dra_core_preserving x y : x y x y core x core y;
dra_disjoint_div x y : x y x y x y ÷ x;
dra_op_div x y : x y x y x y ÷ x y
dra_core_preserving x y :
z, x y x y core (x y) core x z z core x z
}.
Section dra.
......@@ -83,7 +76,6 @@ Proof.
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.
Lemma validity_valid_car_valid (z : T) : z validity_car z.
Proof. apply validity_prf. Qed.
......@@ -95,10 +87,6 @@ Program Instance validity_op : Op T := λ x y,
Validity (validity_car x validity_car y)
( x y validity_car x validity_car y) _.
Solve Obligations with naive_solver auto using dra_op_valid.
Program Instance validity_div : Div T := λ x y,
Validity (validity_car x ÷ validity_car y)
( x y validity_car y validity_car x) _.
Solve Obligations with naive_solver auto using dra_div_valid.
Definition validity_ra : RA (discreteC T).
Proof.
......@@ -108,11 +96,6 @@ Proof.
first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
- by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
- intros ?? [??]; naive_solver.
- intros x1 x2 [? Hx] y1 y2 [? Hy];
split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
split; intros (?&?&z&?&?); split_and!; try tauto.
+ exists z. by rewrite -Hy // -Hx.
+ 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
|by intros; rewrite assoc].
......@@ -120,15 +103,13 @@ Proof.
- intros [x px ?]; split;
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros x y Hxy; exists (core y ÷ core x).
destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
assert (py core x core y)
by intuition eauto 10 using dra_core_preserving.
constructor; [|symmetry]; simpl in *;
intuition eauto using dra_op_div, dra_disjoint_div, dra_core_valid.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
destruct (dra_core_preserving x z) as (z'&Hz').
unshelve eexists (Validity z' (px py pz) _); [|split; simpl].
{ intros (?&?&?); apply Hz'; tauto. }
+ tauto.
+ intros. rewrite Hy //. tauto.
- by intros [x px ?] [y py ?] (?&?&?).
- intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
intuition eauto 10 using dra_disjoint_div, dra_op_div.
Qed.
Definition validityR : cmraT := discreteR validity_ra.
Instance validity_cmra_discrete :
......@@ -146,21 +127,20 @@ Lemma to_validity_op (x y : A) :
to_validity (x y) to_validity x to_validity y.
Proof. split; naive_solver auto using dra_op_valid. Qed.
(*
Lemma to_validity_included x y:
( y to_validity x to_validity y)%C ( x x y).
Proof.
split.
- move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
destruct Hvl' as [? [? ?]].
split; first done.
exists (validity_car z). split_and!; last done.
+ apply EQ. assumption.
+ by apply validity_valid_car_valid.
destruct Hvl' as [? [? ?]]; split; first done.
exists (validity_car z); eauto.
- intros (Hvl & z & EQ & ? & ?).
assert ( y) by (rewrite EQ; apply dra_op_valid; done).
assert ( y) by (rewrite EQ; by apply dra_op_valid).
split; first done. exists (to_validity z). split; first split.
+ intros _. simpl. split_and!; done.
+ intros _. simpl. by split_and!.
+ intros _. setoid_subst. by apply dra_op_valid.
+ intros _. rewrite /= EQ //.
Qed.
*)
End dra.
......@@ -98,19 +98,13 @@ Instance excl_op : Op (excl A) := λ x y,
| ExclUnit, ExclUnit => ExclUnit
| _, _=> ExclBot
end.
Instance excl_div : Div (excl A) := λ x y,
match x, y with
| _, ExclUnit => x
| Excl _, Excl _ => ExclUnit
| _, _ => ExclBot
end.
Definition excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split.
- by intros n []; destruct 1; constructor.
- constructor.
- by destruct 1; intros ?.
- by destruct 1; inversion_clear 1; constructor.
- intros x; split. done. by move=> /(_ 0).
- intros n [?| |]; simpl; auto with lia.
- by intros [?| |] [?| |] [?| |]; constructor.
......@@ -119,7 +113,6 @@ Proof.
- constructor.
- by intros [?| |] [?| |]; exists .
- by intros n [?| |] [?| |].
- by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
......
......@@ -96,29 +96,26 @@ Instance map_op : Op (gmap K A) := merge op.
Instance map_core : Core (gmap K A) := fmap core.
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_div : Div (gmap K A) := merge div.
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_div m1 m2 i : (m1 ÷ m2) !! i = m1 !! i ÷ m2 !! i.
Proof. by apply lookup_merge. Qed.
Lemma lookup_core m i : core m !! i = core (m !! i).
Proof. by apply lookup_fmap. Qed.
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_div cmra_op_div.
Qed.
Lemma map_includedN_spec (m1 m2 : gmap K A) n :
m1 {n} m2 i, m1 !! i {n} 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_div cmra_op_div'.
split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
{ exists m2. by rewrite left_id. }
destruct (IH (delete i m2)) as [m2' Hm2'].
{ intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
- intros _. rewrite Hi. apply: cmra_unit_least.
- rewrite lookup_insert_ne // lookup_delete_ne //. }
destruct (Hm i) as [my Hi']; simplify_map_eq.
exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
- by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
- move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
lookup_insert_ne // lookup_partial_alter_ne.
Qed.
Definition map_cmra_mixin : CMRAMixin (gmap K A).
......@@ -127,7 +124,6 @@ Proof.
- by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
- by intros n m1 m2 Hm i; rewrite !lookup_core (Hm i).
- by intros n m1 m2 Hm ? i; rewrite -(Hm i).
- by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_div (Hm1 i) (Hm2 i).
- intros m; split.
+ by intros ? n i; apply cmra_valid_validN.
+ intros Hm i; apply cmra_valid_validN=> n; apply Hm.
......@@ -140,8 +136,6 @@ Proof.
by rewrite !lookup_core; apply cmra_core_preserving.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros x y; rewrite map_included_spec=> ? i.
by rewrite lookup_op lookup_div cmra_op_div.
- intros n m m1 m2 Hm Hm12.
assert ( i, m !! i {n} m1 !! i m2 !! i) as Hm12'
by (by intros i; rewrite -lookup_op).
......@@ -222,17 +216,17 @@ Lemma map_op_singleton (i : K) (x y : A) :
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Lemma singleton_includedN n m i x :
{[ i := x ]} {n} m y, m !! i {n} Some y x y.
(* not m !! i = Some y x {n} y to deal with n = 0 *)
{[ i := x ]} {n} m y, m !! i {n} Some y x {n} y.
Proof.
split.
- move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
destruct (m' !! i) as [y|];
[exists (x y)|exists x]; eauto using cmra_included_l.
- intros (y&Hi&?); rewrite map_includedN_spec=>j.
destruct (decide (i = j)); simplify_map_eq.
+ rewrite Hi. by apply (includedN_preserving _), cmra_included_includedN.
+ apply: cmra_unit_leastN.
- move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
case (m' !! i)=> [y|]=> Hm.
+ exists (x y); eauto using cmra_includedN_l.
+ by exists x.
- intros (y&Hi&[z ?]).
exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
+ rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
+ by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
Qed.
Lemma map_dom_op m1 m2 : dom (gset K) (m1 m2) dom _ m1 dom _ m2.
Proof.
......
......@@ -3,7 +3,6 @@ From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments div _ _ !_ !_ /.
Inductive frac (A : Type) :=
| Frac : Qp A frac A
......@@ -129,13 +128,6 @@ Instance frac_op : Op (frac A) := λ x y,
| Frac q a, FracUnit | FracUnit, Frac q a => Frac q a
| FracUnit, FracUnit => FracUnit
end.
Instance frac_div : Div (frac A) := λ x y,
match x, y with
| _, FracUnit => x
| Frac q1 a, Frac q2 b =>
match q1 - q2 with Some q => Frac q (a ÷ b) | None => FracUnit end%Qp
| FracUnit, _ => FracUnit
end.
Lemma Frac_op q1 q2 a b : Frac q1 a Frac q2 b = Frac (q1 + q2) (a b).
Proof. done. Qed.
......@@ -146,7 +138,6 @@ Proof.
- intros n []; destruct 1; constructor; by cofe_subst.
- constructor.
- do 2 destruct 1; split; by cofe_subst.
- do 2 destruct 1; simplify_eq/=; try case_match; constructor; by cofe_subst.
- intros [q a|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- intros n [q a|]; destruct 1; split; auto using cmra_validN_S.
- intros [q1 a1|] [q2 a2|] [q3 a3|]; constructor; by rewrite ?assoc.
......@@ -157,10 +148,6 @@ Proof.
- intros n [q1 a1|] [q2 a2|]; destruct 1; split; eauto using cmra_validN_op_l.
trans (q1 + q2)%Qp; simpl; last done.
rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak.
- intros [q1 a1|] [q2 a2|] [[q3 a3|] Hx];
inversion_clear Hx; simplify_eq/=; auto.
+ rewrite Qp_op_minus. by constructor; [|apply cmra_op_div; exists a3].
+ rewrite Qp_minus_diag. by constructor.
- intros n [q a|] y1 y2 Hx Hx'; last first.
{ by exists (, ); destruct y1, y2; inversion_clear Hx'. }
destruct Hx, y1 as [q1 b1|], y2 as [q2 b2|].
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
From iris.prelude Require Import finite.
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......@@ -113,25 +114,21 @@ End iprod_cofe.
Arguments iprodC {_} _.
Section iprod_cmra.
Context {A} {B : A cmraT}.
Context `{Finite A} {B : A cmraT}.
Implicit Types f g : iprod B.
Instance iprod_op : Op (iprod B) := λ f g x, f x g x.
Instance iprod_core : Core (iprod B) := λ f x, core (f x).
Instance iprod_valid : Valid (iprod B) := λ f, x, f x.
Instance iprod_validN : ValidN (iprod B) := λ n f, x, {n} f x.
Instance iprod_div : Div (iprod B) := λ f g x, f x ÷ g x.
Definition iprod_lookup_op f g x : (f g) x = f x g x := eq_refl.
Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
Definition iprod_lookup_div f g x : (f ÷ g) x = f x ÷ g x := eq_refl.
Lemma