Commit d4adcaa0 authored by Ralf Jung's avatar Ralf Jung

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

parents 12447782 ca56a751
Pipeline #310 passed with stage
......@@ -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 iprod_included_spec (f g : iprod B) : f g x, f x g x.
Proof.
split.
- by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
- intros Hh; exists (g ÷ f)=> x; specialize (Hh x).
by rewrite /op /iprod_op /div /iprod_div cmra_op_div.
split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
intros [h ?]%finite_choice. by exists h.
Qed.
Definition iprod_cmra_mixin : CMRAMixin (iprod B).
......@@ -140,7 +137,6 @@ Section iprod_cmra.
- by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
- by intros n f1 f2 Hf ? x; rewrite -(Hf x).
- by intros n f f' Hf g