diff --git a/iris/agree.v b/iris/agree.v index 38aaf15f05ef102eab8d61a3fa0e6181a0cfdf3a..2525dff1f19c7bc7644ff4625a9a25a23aa55ea7 100644 --- a/iris/agree.v +++ b/iris/agree.v @@ -57,7 +57,6 @@ 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. -Global Instance agree_included : Included (agree A) := λ x y, y ≡ x ⋅ y. 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. @@ -80,6 +79,11 @@ Proof. repeat match goal with H : agree_is_valid _ _ |- _ => clear H end; by cofe_subst; rewrite !agree_idempotent. Qed. +Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ={n}= x ⋅ y. +Proof. + split; [|by intros ?; exists y]. + by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent. +Qed. Global Instance agree_cmra : CMRA (agree A). Proof. split; try (apply _ || done). @@ -87,23 +91,20 @@ Proof. rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le. by apply dist_le with n; try apply Hxy. * by intros n x1 x2 Hx y1 y2 Hy. - * by intros x y1 y2 Hy ?; do 2 red; rewrite <-Hy. * intros x; split; [apply agree_valid_0|]. by intros n'; rewrite Nat.le_0_r; intros ->. * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?]. rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto. * intros x; apply agree_idempotent. - * intros x y; change (x ⋅ y ≡ x ⋅ (x ⋅ y)). - by rewrite (associative _), agree_idempotent. * by intros x y n [(?&?&?) ?]. - * by intros x y; do 2 red; rewrite (associative _), agree_idempotent. + * by intros x y n; rewrite agree_includedN. Qed. Lemma agree_op_inv (x y1 y2 : agree A) n : validN n x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2. Proof. by intros [??] Hxy; apply Hxy. Qed. Global Instance agree_extend : CMRAExtend (agree A). Proof. - intros x y1 y2 n ? Hx; exists (x,x); simpl; split. + 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 by done. Qed. @@ -131,15 +132,13 @@ Section agree_map. Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map. Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed. Global Instance agree_map_proper: Proper ((≡)==>(≡)) agree_map := ne_proper _. - Global Instance agree_map_preserving : CMRAPreserving agree_map. + Global Instance agree_map_monotone : CMRAMonotone agree_map. Proof. split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]]. - intros x y; unfold included, agree_included; intros Hy; rewrite Hy. - split; [split|done]. - * by intros (?&?&Hxy); repeat (intro || split); - try apply Hxy; try apply Hf; eauto using @agree_valid_le. - * by intros (?&(?&?&Hxy)&_); repeat split; - try apply Hxy; eauto using agree_valid_le. + intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy. + split; [split; simpl; try tauto|done]. + by intros (?&?&Hxy); repeat split; intros; + try apply Hxy; try apply Hf; eauto using @agree_valid_le. Qed. End agree_map. Lemma agree_map_id `{Cofe A} (x : agree A) : agree_map id x = x. diff --git a/iris/auth.v b/iris/auth.v index d204f361f63ba4a2e905fa031e2a531c4a93d201..23cfd6d983a09c4d2223de536963bfb4d380268a 100644 --- a/iris/auth.v +++ b/iris/auth.v @@ -1,27 +1,30 @@ Require Export iris.excl. Local Arguments disjoint _ _ !_ !_ /. -Local Arguments included _ _ !_ !_ /. -Record auth (A : Type) : Type := Auth { authorative : excl A ; own : A }. +Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. Arguments Auth {_} _ _. -Arguments authorative {_} _. +Arguments authoritative {_} _. Arguments own {_} _. Notation "∘ x" := (Auth ExclUnit x) (at level 20). Notation "∙ x" := (Auth (Excl x) ∅) (at level 20). Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅. -Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x, - valid (authorative x) ∧ excl_above (own x) (authorative x). +Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x, + valid (authoritative x) ∧ excl_above (own x) (authoritative x). Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y, - authorative x ≡ authorative y ∧ own x ≡ own y. + authoritative x ≡ authoritative y ∧ own x ≡ own y. Instance auth_unit `{Unit A} : Unit (auth A) := λ x, - Auth (unit (authorative x)) (unit (own x)). + Auth (unit (authoritative x)) (unit (own x)). Instance auth_op `{Op A} : Op (auth A) := λ x y, - Auth (authorative x ⋅ authorative y) (own x ⋅ own y). + Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y). Instance auth_minus `{Minus A} : Minus (auth A) := λ x y, - Auth (authorative x ⩪ authorative y) (own x ⩪ own y). -Instance auth_included `{Equiv A, Included A} : Included (auth A) := λ x y, - authorative x ≼ authorative y ∧ own x ≼ own y. + Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y). +Lemma auth_included `{Equiv A, Op A} (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. Instance auth_ra `{RA A} : RA (auth A). Proof. @@ -35,19 +38,19 @@ Proof. * by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'. * by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'. - * by intros x y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'. * by split; simpl; rewrite (associative _). * by split; simpl; rewrite (commutative _). * by split; simpl; rewrite ?(ra_unit_l _). * by split; simpl; rewrite ?(ra_unit_idempotent _). - * split; simpl; auto using ra_unit_weaken. - * intros ?? [??]; split; [by apply ra_valid_op_l with (authorative y)|]. + * intros ??; rewrite! auth_included; intros [??]. + by split; simpl; apply ra_unit_preserving. + * intros ?? [??]; split; [by apply ra_valid_op_l with (authoritative y)|]. by apply excl_above_weaken with (own x ⋅ own y) - (authorative x ⋅ authorative y); try apply ra_included_l. - * split; simpl; apply ra_included_l. - * by intros ?? [??]; split; simpl; apply ra_op_minus. + (authoritative x ⋅ authoritative y); try apply ra_included_l. + * by intros ??; rewrite auth_included; + intros [??]; split; simpl; apply ra_op_minus. Qed. Instance auth_ra_empty `{RA A, Empty A, !RAEmpty A} : RAEmpty (auth A). Proof. split. done. by intros x; constructor; simpl; rewrite (left_id _ _). Qed. Lemma auth_frag_op `{RA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b. -Proof. done. Qed. +Proof. done. Qed. \ No newline at end of file diff --git a/iris/cmra.v b/iris/cmra.v index e4c5589ae4eea4f2797c6c0f7f3d61348d1460fd..7b3a9d8b8ee2a4458c2d448430754022de352711 100644 --- a/iris/cmra.v +++ b/iris/cmra.v @@ -3,15 +3,18 @@ Require Export iris.ra iris.cofe. Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. -Class CMRA A `{Equiv A, Compl A, - Unit A, Op A, Valid A, ValidN A, Included A, Minus A} : Prop := { +Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z. +Notation "x ≼{ n } y" := (includedN n x y) + (at level 70, format "x ≼{ n } y") : C_scope. +Instance: Params (@includedN) 4. + +Class CMRA A `{Equiv A, Compl 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) (validN n); cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus; - cmra_included_proper x : Proper ((≡) ==> impl) (included x); (* valid *) cmra_valid_0 x : validN 0 x; cmra_valid_S n x : validN (S n) x → validN n x; @@ -21,18 +24,17 @@ Class CMRA A `{Equiv A, Compl A, cmra_commutative : Commutative (≡) (⋅); cmra_unit_l x : unit x ⋅ x ≡ x; cmra_unit_idempotent x : unit (unit x) ≡ unit x; - cmra_unit_weaken x y : unit x ≼ unit (x ⋅ y); + cmra_unit_preserving n x y : x ≼{n} y → unit x ≼{n} unit y; cmra_valid_op_l n x y : validN n (x ⋅ y) → validN n x; - cmra_included_l x y : x ≼ x ⋅ y; - cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y + 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 x y1 y2 n : + cmra_extend_op n x y1 y2 : validN n x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }. -Class CMRAPreserving - `{Included A, ValidN A, Included B, ValidN B} (f : A → B) := { - included_preserving x y : x ≼ y → f x ≼ f y; +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 : validN n x → validN n (f x) }. @@ -46,12 +48,11 @@ Structure cmraT := CMRAT { cmra_op : Op cmra_car; cmra_valid : Valid cmra_car; cmra_validN : ValidN cmra_car; - cmra_included : Included cmra_car; cmra_minus : Minus cmra_car; cmra_cmra : CMRA cmra_car; cmra_extend : CMRAExtend cmra_car }. -Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _ _}. +Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _}. Arguments cmra_car _ : simpl never. Arguments cmra_equiv _ _ _ : simpl never. Arguments cmra_dist _ _ _ _ : simpl never. @@ -60,12 +61,11 @@ Arguments cmra_unit _ _ : simpl never. Arguments cmra_op _ _ _ : simpl never. Arguments cmra_valid _ _ : simpl never. Arguments cmra_validN _ _ _ : simpl never. -Arguments cmra_included _ _ _ : simpl never. Arguments cmra_minus _ _ _ : simpl never. Arguments cmra_cmra _ : simpl never. Add Printing Constructor cmraT. Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op - cmra_valid cmra_validN cmra_included cmra_minus cmra_cmra cmra_extend. + cmra_valid cmra_validN cmra_minus cmra_cmra cmra_extend. Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A. Canonical Structure cmra_cofeC. @@ -73,6 +73,13 @@ Section cmra. Context `{cmra : CMRA A}. Implicit Types x y z : A. +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; intros n. + symmetry; apply cmra_op_minus, Hxy. +Qed. + Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n). Proof. by split; apply cmra_valid_ne. Qed. Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n). @@ -82,16 +89,15 @@ Proof. split; try by (destruct cmra; 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. * 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. + by apply cmra_op_minus; exists z; rewrite Hz. Qed. Lemma cmra_valid_op_r x y n : validN n (x ⋅ y) → validN n y. Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed. -Lemma cmra_valid_included x y n : validN n y → x ≼ y → validN n x. -Proof. - rewrite ra_included_spec; intros Hvalid [z Hy]; rewrite Hy in Hvalid. - eauto using cmra_valid_op_l. -Qed. Lemma cmra_valid_le x n n' : validN n x → n' ≤ n → validN n' x. Proof. induction 2; eauto using cmra_valid_S. Qed. Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (⋅). @@ -101,24 +107,66 @@ Proof. Qed. Lemma cmra_unit_valid x n : validN n x → validN n (unit x). Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed. -Lemma cmra_included_dist_l x1 x2 x1' n : - x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2. -Proof. - rewrite ra_included_spec; intros [z Hx2] Hx1; exists (x1' ⋅ z); split. - apply ra_included_l. by rewrite Hx1, Hx2. -Qed. Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 : validN 1 (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). Proof. intros ??? z Hz. - destruct (cmra_extend_op z x1 x2 1) as ([y1 y2]&Hz'&?&?); auto; simpl in *. + destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. { by rewrite <-?Hz. } by rewrite Hz', (timeless x1 y1), (timeless x2 y2). Qed. + +(** * Included *) +Global Instance cmra_included_ne n : + Proper (dist n ==> dist n ==> iff) (includedN n). +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). +Proof. + intros n x x' Hx y y' Hy; unfold includedN. + by setoid_rewrite Hx; setoid_rewrite Hy. +Qed. +Lemma cmra_included_0 x y : x ≼{0} y. +Proof. by exists (unit x). Qed. +Lemma cmra_included_S x y n : x ≼{S n} y → x ≼{n} y. +Proof. by intros [z Hz]; exists z; apply dist_S. Qed. + +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). +Proof. + split. + * by intros x; exists (unit x); rewrite ra_unit_r. + * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). + by rewrite (associative _), <-Hy, <-Hz. +Qed. +Lemma cmra_valid_includedN x y n : validN n y → x ≼{n} y → validN n x. +Proof. intros Hyv [z Hy]; rewrite Hy in Hyv; eauto using cmra_valid_op_l. Qed. +Lemma cmra_valid_included x y n : validN n y → x ≼ y → validN n x. +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. + intros [z Hx2] Hx1; exists (x1' ⋅ z); split; auto using ra_included_l. + by rewrite Hx1, Hx2. +Qed. End cmra. -Instance cmra_preserving_id `{CMRA A} : CMRAPreserving (@id A). +Instance cmra_monotone_id `{CMRA A} : CMRAMonotone (@id A). Proof. by split. Qed. +Instance cmra_monotone_ra_monotone `{CMRA A, CMRA B} (f : A → B) : + CMRAMonotone f → RAMonotone f. +Proof. + split. + * intros x y; rewrite !cmra_included_includedN. + by intros ? n; apply includedN_preserving. + * intros x; rewrite !cmra_valid_validN. + by intros ? n; apply validN_preserving. +Qed. (* Also via [cmra_cofe; cofe_equivalence] *) Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances. @@ -139,15 +187,18 @@ Section discrete. * by intros [|n]; try apply ra_minus_proper. * by intros [|n]. * intros x; split; intros Hvalid. by intros [|n]. apply (Hvalid 1). + * by intros [|n]; try apply ra_unit_preserving. * 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. Proof. - intros x y1 y2 [|n] ??; [|by exists (y1,y2)]. + intros [|n] x y1 y2 ??; [|by exists (y1,y2)]. by exists (x,unit x); simpl; rewrite ra_unit_r. Qed. - Definition discreteC : cmraT := CMRAT A. + Definition discreteRA : cmraT := CMRAT A. 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). @@ -158,11 +209,20 @@ Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x, valid (x.1) ∧ valid (x.2). Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x, validN n (x.1) ∧ validN n (x.2). -Instance prod_included `{Included A, Included B} : Included (A * B) := - prod_relation (≼) (≼). 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 _. @@ -171,7 +231,6 @@ Proof. * 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. - * by intros x y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?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|]. @@ -180,10 +239,11 @@ Proof. * split; simpl; apply (commutative _). * split; simpl; apply ra_unit_l. * split; simpl; apply ra_unit_idempotent. - * split; apply ra_unit_weaken. + * 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. - * split; apply cmra_included_l. - * by intros x y [??]; split; apply cmra_op_minus. + * intros x y n; rewrite prod_includedN; intros [??]. + by split; apply cmra_op_minus. Qed. Instance prod_ra_empty `{RAEmpty A, RAEmpty B} : RAEmpty (A * B). Proof. @@ -191,18 +251,19 @@ Proof. Qed. Instance prod_cmra_extend `{CMRAExtend A, CMRAExtend B} : CMRAExtend (A * B). Proof. - intros x y1 y2 n [??] [??]; simpl in *. - destruct (cmra_extend_op (x.1) (y1.1) (y2.1) n) as (z1&?&?&?); auto. - destruct (cmra_extend_op (x.2) (y1.2) (y2.2) n) as (z2&?&?&?); auto. + 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 (A B : cmraT) : cmraT := CMRAT (A * B). -Instance prod_map_cmra_preserving `{CMRA A, CMRA A', CMRA B, CMRA B'} - (f : A → A') (g : B → B') `{!CMRAPreserving f, !CMRAPreserving g} : - CMRAPreserving (prod_map f g). +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). Proof. split. - * by intros x1 x2 [??]; split; simpl; apply included_preserving. + * intros n x1 x2; rewrite !prod_includedN; intros [??]; simpl. + by split; apply includedN_preserving. * by intros n x [??]; split; simpl; apply validN_preserving. Qed. Definition prodRA_map {A A' B B' : cmraT} diff --git a/iris/cmra_maps.v b/iris/cmra_maps.v index 68591bece3b6bdabf4ba85c8938218d105dd461d..d4a20f725ba5d58e11b54654106d181a04f2fbee 100644 --- a/iris/cmra_maps.v +++ b/iris/cmra_maps.v @@ -3,18 +3,28 @@ Require Import prelude.pmap prelude.nmap prelude.zmap. Require Import prelude.stringmap prelude.natmap. (** option *) -Instance option_valid `{Valid A} : Valid (option A) := λ x, - match x with Some x => valid x | None => True end. -Instance option_validN `{ValidN A} : ValidN (option A) := λ n x, - match x with Some x => validN n x | None => True end. +Instance option_valid `{Valid A} : Valid (option A) := λ mx, + match mx with Some x => valid x | None => True end. +Instance option_validN `{ValidN A} : ValidN (option A) := λ n mx, + match mx with Some x => validN 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) := difference_with (λ x y, Some (x ⩪ y)). -Inductive option_included `{Included A} : Included (option A) := - | Some_included x y : x ≼ y → Some x ≼ Some y - | None_included x : None ≼ x. -Existing Instance option_included. +Lemma option_includedN `{CMRA A} n mx my : + mx ≼{n} my ↔ n = 0 ∨ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y. +Proof. + split. + * intros [mz Hmz]; destruct n as [|n]; [by left|right]. + 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. + + by exists z. + + by cofe_subst. + * 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). Proof. split. @@ -27,8 +37,6 @@ Proof. eapply (_ : Proper (dist _ ==> impl) (validN _)); eauto. * by destruct 1; inversion_clear 1; constructor; repeat apply (_ : Proper (dist _ ==> _ ==> _) _). - * intros [x|]; destruct 1; inversion_clear 1; constructor; - eapply (_ : Proper (equiv ==> impl) (included _)); eauto. * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0. * intros n [x|]; unfold validN, option_validN; auto using cmra_valid_S. * by intros [x|]; unfold valid, validN, option_validN, option_valid; @@ -37,19 +45,21 @@ Proof. * intros [x|] [y|]; constructor; rewrite 1?(commutative _); auto. * by intros [x|]; constructor; rewrite cmra_unit_l. * by intros [x|]; constructor; rewrite cmra_unit_idempotent. - * intros [x|] [y|]; constructor; auto using cmra_unit_weaken. + * intros n mx my; rewrite !option_includedN;intros [|[->|(x&y&->&->&?)]];auto. + 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. - * intros [x|] [y|]; constructor; auto using cmra_included_l. - * destruct 1 as [|[]]; constructor; eauto using cmra_op_minus. + * 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). Proof. - intros mx my1 my2 n; destruct (decide (n = 0)) as [->|]. + intros n mx my1 my2; destruct (decide (n = 0)) as [->|]. { by exists (mx, None); repeat constructor; destruct mx; constructor. } destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx'; try (by exfalso; inversion Hx'; auto). - * destruct (cmra_extend_op x y1 y2 n) as ([z1 z2]&?&?&?); auto. + * destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto. { by inversion_clear Hx'. } by exists (Some z1, Some z2); repeat constructor. * by exists (Some x,None); inversion Hx'; repeat constructor. @@ -57,10 +67,11 @@ Proof. * exists (None,None); repeat constructor. Qed. Instance option_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A → B) - `{!CMRAPreserving f} : CMRAPreserving (fmap f : option A → option B). + `{!CMRAMonotone f} : CMRAMonotone (fmap f : option A → option B). Proof. split. - * by destruct 1 as [|[?|]]; constructor; apply included_preserving. + * 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. @@ -74,14 +85,28 @@ Section map. Instance map_valid `{Valid A} : Valid (M A) := λ m, ∀ i, valid (m !! i). Instance map_validN `{ValidN A} : ValidN (M A) := λ n m, ∀ i, validN n (m!!i). Instance map_minus `{Minus A} : Minus (M A) := merge minus. - Instance map_included `{Included A} : Included (M A) := λ m1 m2, - ∀ i, m1 !! i ≼ m2 !! i. Lemma lookup_op `{Op A} 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. Proof. by apply lookup_merge. Qed. Lemma lookup_unit `{Unit A} m i : unit m !! i = unit (m !! i). Proof. by apply lookup_fmap. Qed. + Lemma map_included_spec `{CMRA A} (m1 m2 : M A) : + m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i. + Proof. + split. + * intros [m Hm]; intros i; exists (m !! i). by 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 : M A) n : + m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i. + Proof. + split. + * intros [m Hm]; intros i; exists (m !! i). by rewrite <-lookup_op, Hm. + * intros Hm; exists (m2 ⩪ m1); intros i. + by rewrite lookup_op, lookup_minus, cmra_op_minus. + Qed. Instance map_cmra `{CMRA A} : CMRA (M A). Proof. split. @@ -91,7 +116,6 @@ Section map. * by intros n m1 m2 Hm ? i; rewrite <-(Hm i). * intros n m1 m1' Hm1 m2 m2' Hm2 i. by rewrite !lookup_minus, (Hm1 i), (Hm2 i). - * by intros m1 m2 m2' Hm2 ? i; rewrite <-(Hm2 i). * intros m i; apply cmra_valid_0. * intros n m Hm i; apply cmra_valid_S, Hm. * intros m; split; [by intros Hm n i; apply cmra_valid_validN|]. @@ -100,11 +124,12 @@ Section map. * by intros m1 m2 i; rewrite !lookup_op, (commutative _). * by intros m i; rewrite lookup_op, !lookup_unit, ra_unit_l. * by intros m i; rewrite !lookup_unit, ra_unit_idempotent. - * intros m1 m2 i; rewrite !lookup_unit, lookup_op; apply ra_unit_weaken. + * intros n x y; rewrite !map_includedN_spec; intros Hm i. + by rewrite !lookup_unit; apply cmra_unit_preserving. * intros n m1 m2 Hm i; apply cmra_valid_op_l with (m2 !! i). by rewrite <-lookup_op. - * intros m1 m2 i; rewrite lookup_op; apply ra_included_l. - * by intros m1 m2 Hm i; rewrite lookup_op, lookup_minus, ra_op_minus. + * intros x y n; rewrite map_includedN_spec; intros ? i. + by rewrite lookup_op, lookup_minus, cmra_op_minus by done. Qed. Instance map_ra_empty `{RA A} : RAEmpty (M A). Proof. @@ -114,10 +139,10 @@ Section map. Qed. Instance map_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (M A). Proof. - intros m m1 m2 n Hm Hm12. + 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). - set (f i := cmra_extend_op (m !! i) (m1 !! i) (m2 !! i) n (Hm i) (Hm12' i)). + set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)). 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; simpl; intros i; rewrite ?lookup_op, !lookup_imap. @@ -131,11 +156,12 @@ Section map. by destruct (m1 !! i), (m2 !! i); inversion_clear Hm12''. Qed. Definition mapRA (A : cmraT) : cmraT := CMRAT (M A). - Global Instance map_fmap_cmra_preserving `{CMRA A, CMRA B} (f : A → B) - `{!CMRAPreserving f} : CMRAPreserving (fmap f : M A → M B). + Global Instance map_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) + `{!CMRAMonotone f} : CMRAMonotone (fmap f : M A → M B). Proof. split. - * by intros m1 m2 Hm i; rewrite !lookup_fmap; apply included_preserving. + * 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. Hint Resolve (map_fmap_ne (M:=M)) : typeclass_instances. @@ -143,8 +169,8 @@ Section map. 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_mapcmra_preserving {A B : cmraT} (f : A -n> B) - `{!CMRAPreserving f} : CMRAPreserving (mapRA_map f) := _. + Global Instance mapRA_mapcmra_monotone {A B : cmraT} (f : A -n> B) + `{!CMRAMonotone f} : CMRAMonotone (mapRA_map f) := _. End map. Arguments mapRA {_} _ {_ _ _ _ _ _ _ _ _} _. diff --git a/iris/dra.v b/iris/dra.v index b7f573f0c406faf4fa30d5af6dd7958912dba615..aa3e707d88e0b91dec388ba41eea9a4a82276926 100644 --- a/iris/dra.v +++ b/iris/dra.v @@ -30,14 +30,19 @@ Instance validity_valid_proper `{Equiv A} (P : A → Prop) : Proof. intros ?? [??]; naive_solver. Qed. Local Notation V := valid. -Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := { + +Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y, + ∃ z, y ≡ x ⋅ z ∧ V z ∧ x ⊥ z. +Instance: Params (@dra_included) 4. +Local Infix "≼" := dra_included. + +Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := { (* setoids *) dra_equivalence :> Equivalence ((≡) : relation A); dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅); dra_unit_proper :> Proper ((≡) ==> (≡)) unit; dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x); dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus; - dra_included_proper :> Proper ((≡) ==> (≡) ==> impl) included; (* validity *) dra_op_valid x y : V x → V y → x ⊥ y → V (x ⋅ y); dra_unit_valid x : V x → V (unit x); @@ -51,20 +56,21 @@ Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := { dra_unit_disjoint_l x : V x → unit x ⊥ x; dra_unit_l x : V x → unit x ⋅ x ≡ x; dra_unit_idempotent x : V x → unit (unit x) ≡ unit x; - dra_unit_weaken x y : V x → V y → x ⊥ y → unit x ≼ unit (x ⋅ y); - dra_included_l x y : V x → V y → x ⊥ y → x ≼ x ⋅ y; - dra_disjoint_difference x y : V x → V y → x ≼ y → x ⊥ y ⩪ x; - dra_op_difference x y : V x → V y → x ≼ y → x ⋅ y ⩪ x ≡ y + dra_unit_preserving x y : V x → V y → x ≼ y → unit x ≼ unit y; + dra_disjoint_minus x y : V x → V y → x ≼ y → x ⊥ y ⩪ x; + dra_op_minus x y : V x → V y → x ≼ y → x ⋅ y ⩪ x ≡ y }. Section dra. Context A `{DRA A}. Arguments valid _ _ !_ /. +Hint Immediate dra_op_proper : typeclass_instances. -Instance: Proper ((≡) ==> (≡) ==> impl) (⊥). +Instance: Proper ((≡) ==> (≡) ==> iff) (⊥). Proof. - intros x1 x2 Hx y1 y2 Hy. - by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx. + intros x1 x2 Hx y1 y2 Hy; split. + * by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx. + * by rewrite <-Hy, (symmetry_iff (⊥) x2), (symmetry_iff (⊥) x1), <-Hx. Qed. Lemma dra_disjoint_rl x y z : V x → V y → V z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y. Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed. @@ -78,10 +84,8 @@ Proof. intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl. apply dra_disjoint_move_l; auto; by rewrite dra_commutative. Qed. -Hint Immediate dra_associative dra_commutative dra_unit_disjoint_l - dra_unit_l dra_unit_idempotent dra_unit_weaken dra_included_l - dra_op_difference dra_disjoint_difference dra_disjoint_rl - dra_disjoint_lr dra_disjoint_move_l dra_disjoint_move_r. +Hint Immediate dra_disjoint_move_l dra_disjoint_move_r. +Hint Unfold dra_included. Notation T := (validity (valid : A → Prop)). Program Instance validity_unit : Unit T := λ x, @@ -91,8 +95,6 @@ Program Instance validity_op : Op T := λ x y, Validity (validity_car x ⋅ validity_car y) (V x ∧ V y ∧ validity_car x ⊥ validity_car y) _. Next Obligation. by apply dra_op_valid; try apply validity_prf. Qed. -Instance validity_included : Included T := λ x y, - V y → V x ∧ validity_car x ≼ validity_car y. Program Instance validity_minus : Minus T := λ x y, Validity (validity_car x ⩪ validity_car y) (V x ∧ V y ∧ validity_car y ≼ validity_car x) _. @@ -108,21 +110,25 @@ Proof. * by intros ?? Heq ?; rewrite <-Heq. * intros x1 x2 [? Hx] y1 y2 [? Hy]; split; simpl; [|by intros (?&?&?); rewrite Hx, Hy]. - split; intros (?&?&?); split_ands'; try tauto. - + by rewrite <-Hx, <-Hy by done. - + by rewrite Hx, Hy by tauto. - * intros ??? [? Heq] Hle; split; [apply Hle; tauto|]. - rewrite <-Heq by tauto; apply Hle; tauto. - * intros [x px ?] [y py ?] [z pz ?]; - split; simpl; [naive_solver|intros; apply (associative _)]. - * intros [x px ?] [y py ?]; split; naive_solver. - * intros [x px ?]; split; naive_solver. - * intros [x px ?]; split; naive_solver. - * intros [x px ?] [y py ?]; split; naive_solver. + split; intros (?&?&z&?&?); split_ands'; try tauto. + + exists z. by rewrite <-Hy, <-Hx. + + exists z. by rewrite Hx, Hy by tauto. + * intros [x px ?] [y py ?] [z pz ?]; split; simpl; + [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl + |intros; apply (associative _)]. + * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative. + * intros [x px ?]; split; + naive_solver eauto using dra_unit_l, dra_unit_disjoint_l. + * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent. + * intros x y Hxy; exists (unit y ⩪ unit x). + destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *. + assert (py → unit x ≼ unit y) + by intuition eauto 10 using dra_unit_preserving. + constructor; [|symmetry]; simpl in *; + intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid. * by intros [x px ?] [y py ?] (?&?&?). - * intros [x px ?] [y py ?]; split; naive_solver. - * intros [x px ?] [y py ?]; - unfold included, validity_included; split; naive_solver. + * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *; + intuition eauto 10 using dra_disjoint_minus, dra_op_minus. Qed. Definition dra_update (x y : T) : (∀ z, V x → V z → validity_car x ⊥ z → V y ∧ validity_car y ⊥ z) → x ⇝ y. diff --git a/iris/excl.v b/iris/excl.v index 698fc40a7ad23549b76e7b4da0e72d9e72585b22..7f4edafd2a3f8ef2fae745ee080aa30fdc5fc4a2 100644 --- a/iris/excl.v +++ b/iris/excl.v @@ -1,6 +1,5 @@ Require Export iris.cmra. Local Arguments disjoint _ _ !_ !_ /. -Local Arguments included _ _ !_ !_ /. Inductive excl (A : Type) := | Excl : A → excl A @@ -32,15 +31,6 @@ Instance excl_minus {A} : Minus (excl A) := λ x y, | Excl _, Excl _ => ExclUnit | _, _ => ExclBot end. -Instance excl_included `{Equiv A} : Included (excl A) := λ x y, - match x, y with - | Excl x, Excl y => x ≡ y - | ExclUnit, _ => True - | _, ExclBot => True - | _, _ => False - end. -Definition excl_above `{Included A} (x : A) (y : excl A) : Prop := - match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end. Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A). Proof. split. @@ -52,21 +42,23 @@ Proof. * constructor. * by destruct 1. * by do 2 destruct 1; constructor. - * by intros []; destruct 1; simpl; try (intros Hx; rewrite Hx). * by intros [?| |] [?| |] [?| |]; constructor. * by intros [?| |] [?| |]; constructor. * by intros [?| |]; constructor. * constructor. + * intros [?| |] [?| |]; exists ∅; constructor. * by intros [?| |] [?| |]. - * by intros [?| |] [?| |]. - * by intros [?| |] [?| |]; simpl; try constructor. - * by intros [?| |] [?| |] ?; try constructor. + * by intros [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor. Qed. Instance excl_empty_ra `{Equiv A, !Equivalence (@equiv A _)} : RAEmpty (excl A). Proof. split. done. by intros []. Qed. Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y. Proof. by destruct y; intros ? [?| |]. Qed. +Definition excl_above `{Equiv A, Op A} (x : A) (y : excl A) : Prop := + match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end. +Instance: Params (@excl_above) 3. + Section excl_above. Context `{RA A}. Global Instance excl_above_proper : Proper ((≡) ==> (≡) ==> iff) excl_above. @@ -74,7 +66,8 @@ Section excl_above. Lemma excl_above_weaken (a b : A) x y : excl_above b y → a ≼ b → x ≼ y → excl_above a x. Proof. - destruct x as [a'| |], y as [b'| |]; simpl; intros ??; try done. - by intros Hab; rewrite Hab; transitivity b. + destruct x as [a'| |], y as [b'| |]; + intros ?? [[] Hz]; inversion_clear Hz; simpl in *; try done. + by setoid_subst; transitivity b. Qed. End excl_above. diff --git a/iris/language.v b/iris/language.v new file mode 100644 index 0000000000000000000000000000000000000000..c9d26dc74826b7494967edb91aa2161fb543ddb9 --- /dev/null +++ b/iris/language.v @@ -0,0 +1,31 @@ +Require Import prelude.prelude. + +Class language (E V S : Type) := Language { + to_expr : V → E; + of_expr : E → option V; + atomic : E → Prop; + prim_step : (E * S) → (E * S) → option E → Prop; + of_to_expr v : of_expr (to_expr v) = Some v; + to_of_expr e v : of_expr e = Some v → to_expr v = e; + values_stuck e σ s' ef : prim_step (e,σ) s' ef → of_expr e = None; + atomic_not_value e : atomic e → of_expr e = None; + atomic_step e1 σ1 e2 σ2 ef : + atomic e1 → + prim_step (e1,σ1) (e2,σ2) ef → + is_Some (of_expr e2) +}. + +Section foo. + Context `{language E V St}. + + Definition cfg : Type := (list E * St)%type. + Inductive step (ρ1 ρ2 : cfg) : Prop := + | step_atomic e1 σ1 e2 σ2 ef t1 t2 : + ρ1 = (t1 ++ e1 :: t2, σ1) → + ρ1 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) → + prim_step (e1, σ1) (e2, σ2) ef → + step ρ1 ρ2. + + Definition steps := rtc step. + Definition stepn := nsteps step. +End foo. \ No newline at end of file diff --git a/iris/logic.v b/iris/logic.v index d3165e625a1ea8908d0a881fb0353a06ff4015ab..0e1ff71a0349369e55ae7a0fbb23fd6c888cdf33 100644 --- a/iris/logic.v +++ b/iris/logic.v @@ -48,7 +48,7 @@ Canonical Structure uPredC (M : cmraT) : cofeT := CofeT (uPred M). (** functor *) Program Definition uPred_map {M1 M2 : cmraT} (f : M2 → M1) - `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f} + `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} (P : uPred M1) : uPred M2 := {| uPred_holds n x := P n (f x) |}. Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed. Next Obligation. intros M1 M2 f _ _ P x; apply uPred_0. Qed. @@ -56,15 +56,15 @@ Next Obligation. naive_solver eauto using uPred_weaken, included_preserving, validN_preserving. Qed. Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 → M1) - `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f} : + `{!∀ n, Proper (dist n ==> dist n) f, !CMRAMonotone f} : Proper (dist n ==> dist n) (uPred_map f). Proof. by intros n x1 x2 Hx y n'; split; apply Hx; auto using validN_preserving. Qed. -Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAPreserving f} : +Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} : uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2). Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1) - `{!CMRAPreserving f, !CMRAPreserving g} n : + `{!CMRAMonotone f, !CMRAMonotone g} n : f ={n}= g → uPredC_map f ={n}= uPredC_map g. Proof. by intros Hfg P y n' ??; simpl; rewrite (dist_le _ _ _ _(Hfg y)) by lia. @@ -125,8 +125,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 ? Hvalid. assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?). - { rewrite ra_included_spec in Hxy; 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. } rewrite Hy in Hvalid; exists x1, x2'; split_ands; auto. * apply uPred_weaken with x1 n1; eauto using cmra_valid_op_l. @@ -165,11 +164,11 @@ Next Obligation. Qed. Program Definition uPred_own {M : cmraT} (a : M) : uPred M := - {| uPred_holds n x := ∃ a', x ={n}= a ⋅ a' |}. -Next Obligation. by intros M a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed. + {| uPred_holds n x := a ≼{n} x |}. +Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite <-Hx. Qed. Next Obligation. by intros M a x; exists x. Qed. Next Obligation. - intros M a x1 x n1 n2; rewrite ra_included_spec; intros [a' Hx1] [x2 Hx] ??. + intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??. exists (a' ⋅ x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx. Qed. Program Definition uPred_valid {M : cmraT} (a : M) : uPred M := @@ -571,7 +570,7 @@ Lemma uPred_later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I. Proof. intros x n ?; split. * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)]. - destruct (cmra_extend_op x x1 x2 n) + destruct (cmra_extend_op n x x1 x2) as ([y1 y2]&Hx'&Hy1&Hy2); auto 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&?&?)]. @@ -682,10 +681,9 @@ Proof. Qed. Lemma uPred_own_unit (a : M) : uPred_own (unit a) ≡ (□ uPred_own (unit a))%I. Proof. - intros x n; split; [intros [a' Hx]|by apply uPred_always_elim]. - assert (∃ a'', unit (unit a ⋅ a') ≡ unit (unit a) ⋅ a'') as [a'' Ha] - by (rewrite <-ra_included_spec; auto using ra_unit_weaken). - by exists a''; rewrite Hx, Ha, ra_unit_idempotent. + intros x n; split; [intros [a' Hx]|by apply uPred_always_elim]. simpl. + rewrite <-(ra_unit_idempotent a), Hx. + apply cmra_unit_preserving, cmra_included_l. Qed. Lemma uPred_own_empty `{Empty M, !RAEmpty M} : True%I ⊆ uPred_own ∅. Proof. intros x [|n] ??; [done|]. by exists x; rewrite (left_id _ _). Qed. @@ -712,7 +710,7 @@ Global Instance uPred_sep_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ★ Q). Proof. intros ?? x [|n] Hvalid (x1&x2&Hx12&?&?); [done|]. - destruct (cmra_extend_op x x1 x2 1) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *. + destruct (cmra_extend_op 1 x x1 x2) as ([y1 y2]&Hx&Hy1&Hy2); auto; simpl in *. rewrite Hx12 in Hvalid; exists y1, y2; split_ands; [by rewrite Hx| |]. * apply timelessP; rewrite Hy1; eauto using cmra_valid_op_l. * apply timelessP; rewrite Hy2; eauto using cmra_valid_op_r. @@ -738,7 +736,7 @@ Global Instance uPred_own_timeless (a : M) : Timeless a → TimelessP (uPred_own a). Proof. intros ? x n ? [a' ?]. - destruct (cmra_extend_op x a a' 1) as ([b b']&Hx&Hb&Hb'); auto; simpl in *. + destruct (cmra_extend_op 1 x a a') as ([b b']&Hx&Hb&Hb'); auto; simpl in *. by exists b'; rewrite Hx, (timeless a b) by done. Qed. End logic. diff --git a/iris/ra.v b/iris/ra.v index a668bafe150a04978a1c19ee8b935e960ef946a2..001ffdb812a7d9318677419bb7c4f92df5ec2984 100644 --- a/iris/ra.v +++ b/iris/ra.v @@ -11,32 +11,30 @@ Instance: Params (@op) 2. Infix "⋅" := op (at level 50, left associativity) : C_scope. Notation "(⋅)" := op (only parsing) : C_scope. -Class Included (A : Type) := included : relation A. -Instance: Params (@included) 2. +Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z. Infix "≼" := included (at level 70) : C_scope. Notation "(≼)" := included (only parsing) : C_scope. Hint Extern 0 (?x ≼ ?x) => reflexivity. +Instance: Params (@included) 3. Class Minus (A : Type) := minus : A → A → A. Instance: Params (@minus) 2. Infix "⩪" := minus (at level 40) : C_scope. -Class RA A `{Equiv A, Valid A, Unit A, Op A, Included A, Minus A} : Prop := { +Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := { (* setoids *) ra_equivalence :> Equivalence ((≡) : relation A); ra_op_proper x :> Proper ((≡) ==> (≡)) (op x); ra_unit_proper :> Proper ((≡) ==> (≡)) unit; ra_valid_proper :> Proper ((≡) ==> impl) valid; ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus; - ra_included_proper x :> Proper ((≡) ==> impl) (included x); (* monoid *) ra_associative :> Associative (≡) (⋅); ra_commutative :> Commutative (≡) (⋅); ra_unit_l x : unit x ⋅ x ≡ x; ra_unit_idempotent x : unit (unit x) ≡ unit x; - ra_unit_weaken x y : unit x ≼ unit (x ⋅ y); + ra_unit_preserving x y : x ≼ y → unit x ≼ unit y; ra_valid_op_l x y : valid (x ⋅ y) → valid x; - ra_included_l x y : x ≼ x ⋅ y; ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y }. Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := { @@ -44,6 +42,12 @@ Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := { ra_empty_l :> LeftId (≡) ∅ (⋅) }. +Class RAMonotone + `{Equiv A, Op A, Valid A, Equiv B, Op B, Valid B} (f : A → B) := { + included_preserving x y : x ≼ y → f x ≼ f y; + valid_preserving x : valid x → valid (f x) +}. + (** Big ops *) Fixpoint big_op `{Op A, Empty A} (xs : list A) : A := match xs with [] => ∅ | x :: xs => x ⋅ big_op xs end. @@ -87,38 +91,27 @@ Lemma ra_unit_unit x : unit x ⋅ unit x ≡ unit x. Proof. by rewrite <-(ra_unit_idempotent x) at 2; rewrite ra_unit_r. Qed. (** ** Order *) -Lemma ra_included_spec x y : x ≼ y ↔ ∃ z, y ≡ x ⋅ z. -Proof. - split; [by exists (y ⩪ x); rewrite ra_op_minus|]. - intros [z Hz]; rewrite Hz; apply ra_included_l. -Qed. -Global Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> iff) (≼). -Proof. - intros x1 x2 Hx y1 y2 Hy; rewrite !ra_included_spec. - by setoid_rewrite Hx; setoid_rewrite Hy. -Qed. +Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> impl) (≼). +Proof. intros x1 x2 Hx y1 y2 Hy [z Hz]; exists z. by rewrite <-Hy, Hz, Hx. Qed. +Global Instance ra_included_proper : Proper ((≡) ==> (≡) ==> iff) (≼). +Proof. by split; apply ra_included_proper'. Qed. +Lemma ra_included_l x y : x ≼ x ⋅ y. +Proof. by exists y. Qed. +Lemma ra_included_r x y : y ≼ x ⋅ y. +Proof. rewrite (commutative op); apply ra_included_l. Qed. Global Instance: PreOrder included. Proof. split. - * by intros x; rewrite ra_included_spec; exists (unit x); rewrite ra_unit_r. - * intros x y z; rewrite ?ra_included_spec; intros [z1 Hy] [z2 Hz]. - exists (z1 ⋅ z2). by rewrite (associative _), <-Hy, <-Hz. + * by intros x; exists (unit x); rewrite ra_unit_r. + * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). + by rewrite (associative _), <-Hy, <-Hz. Qed. Lemma ra_included_unit x : unit x ≼ x. -Proof. by rewrite ra_included_spec; exists x; rewrite ra_unit_l. Qed. -Lemma ra_included_r x y : y ≼ x ⋅ y. -Proof. rewrite (commutative _); apply ra_included_l. Qed. +Proof. by exists x; rewrite ra_unit_l. Qed. Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. -Proof. - rewrite !ra_included_spec. - by intros (z1&Hz1); exists z1; rewrite Hz1, (associative (⋅)). -Qed. +Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1, (associative (⋅)). Qed. Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed. -Lemma ra_unit_preserving x y : x ≼ y → unit x ≼ unit y. -Proof. - rewrite ra_included_spec; intros [z Hy]; rewrite Hy; apply ra_unit_weaken. -Qed. (** ** Properties of [(⇝)] relation *) Global Instance ra_update_preorder : PreOrder ra_update. @@ -132,7 +125,7 @@ Proof. by intros x; rewrite (commutative op), (left_id _ _). Qed. Lemma ra_unit_empty x : unit ∅ ≡ ∅. Proof. by rewrite <-(ra_unit_l ∅) at 2; rewrite (right_id _ _). Qed. Lemma ra_empty_least x : ∅ ≼ x. -Proof. by rewrite ra_included_spec; exists x; rewrite (left_id _ _). Qed. +Proof. by exists x; rewrite (left_id _ _). Qed. (** * Big ops *) Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op. diff --git a/iris/sts.v b/iris/sts.v index 71dbcdfd67eb3abc1fb1174c742292a767b3ac89..ceee5ea16c9e1cac54c2905e06d7bc5dac6678c5 100644 --- a/iris/sts.v +++ b/iris/sts.v @@ -1,34 +1,34 @@ Require Export iris.ra. -Require Import prelude.sets prelude.bsets iris.dra. +Require Import prelude.sets iris.dra. Local Arguments valid _ _ !_ /. Local Arguments op _ _ !_ !_ /. Local Arguments unit _ _ !_ /. Module sts. -Inductive t {A B} (R : relation A) (tok : A → bset B) := - | auth : A → bset B → t R tok - | frag : set A → bset B → t R tok. +Inductive t {A B} (R : relation A) (tok : A → set B) := + | auth : A → set B → t R tok + | frag : set A → set B → t R tok. Arguments auth {_ _ _ _} _ _. Arguments frag {_ _ _ _} _ _. Section sts_core. -Context {A B : Type} `{∀ x y : B, Decision (x = y)}. -Context (R : relation A) (tok : A → bset B). +Context {A B : Type} (R : relation A) (tok : A → set B). +Infix "≼" := dra_included. Inductive sts_equiv : Equiv (t R tok) := | auth_equiv s T1 T2 : T1 ≡ T2 → auth s T1 ≡ auth s T2 | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2. Global Existing Instance sts_equiv. -Inductive step : relation (A * bset B) := +Inductive step : relation (A * set B) := | Step s1 s2 T1 T2 : R s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ → tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2). Hint Resolve Step. -Inductive frame_step (T : bset B) (s1 s2 : A) : Prop := +Inductive frame_step (T : set B) (s1 s2 : A) : Prop := | Frame_step T1 T2 : T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2. Hint Resolve Frame_step. -Record closed (T : bset B) (S : set A) : Prop := Closed { +Record closed (T : set B) (S : set A) : Prop := Closed { closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅; closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S }. @@ -37,8 +37,8 @@ Lemma closed_steps S T s1 s2 : Proof. induction 3; eauto using closed_step. Qed. Global Instance sts_valid : Valid (t R tok) := λ x, match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end. -Definition up (T : bset B) (s : A) : set A := mkSet (rtc (frame_step T) s). -Definition up_set (T : bset B) (S : set A) : set A := S ≫= up T. +Definition up (T : set B) (s : A) : set A := mkSet (rtc (frame_step T) s). +Definition up_set (T : set B) (S : set A) : set A := S ≫= up T. Global Instance sts_unit : Unit (t R tok) := λ x, match x with | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅ @@ -55,12 +55,6 @@ Global Instance sts_op : Op (t R tok) := λ x1 x2, | frag _ T1, auth s T2 => auth s (T1 ∪ T2) | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *) end. -Inductive sts_included : Included (t R tok) := - | frag_frag_included S1 S2 T1 T2 S' : - T1 ⊆ T2 → S2 ≡ S1 ∩ S' → closed (T2 ∖ T1) S' → frag S1 T1 ≼ frag S2 T2 - | frag_auth_included s S T1 T2 : s ∈ S → T1 ⊆ T2 → frag S T1 ≼ auth s T2 - | auth_auth_included s T1 T2 : T1 ⊆ T2 → auth s T1 ≼ auth s T2. -Global Existing Instance sts_included. Global Instance sts_minus : Minus (t R tok) := λ x1 x2, match x1, x2 with | frag S1 T1, frag S2 T2 => frag (up_set (T1 ∖ T2) S1) (T1 ∖ T2) @@ -69,10 +63,9 @@ Global Instance sts_minus : Minus (t R tok) := λ x1 x2, | auth s T1, auth _ T2 => frag (up (T1 ∖ T2) s) (T1 ∖ T2) end. -Hint Extern 5 (equiv (A:=set _) _ _) => esolve_elem_of : sts. -Hint Extern 5 (equiv (A:=bset _) _ _) => esolve_elem_of : sts. -Hint Extern 5 (_ ∈ _) => esolve_elem_of : sts. -Hint Extern 5 (_ ⊆ _) => esolve_elem_of : sts. +Hint Extern 10 (equiv (A:=set _) _ _) => esolve_elem_of : sts. +Hint Extern 10 (_ ∈ _) => esolve_elem_of : sts. +Hint Extern 10 (_ ⊆ _) => esolve_elem_of : sts. Instance: Equivalence ((≡) : relation (t R tok)). Proof. split. @@ -112,7 +105,7 @@ Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set. Proof. by intros T1 T2 HT S1 S2 HS; unfold up_set; rewrite HS, HT. Qed. Lemma elem_of_up s T : s ∈ up T s. Proof. constructor. Qed. -Lemma subseteq_up_set S T : S ⊆ up_set T S. +Lemma suseteq_up_set S T : S ⊆ up_set T S. Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → closed T (up_set T S). Proof. @@ -135,16 +128,10 @@ Lemma closed_up_empty s : closed ∅ (up ∅ s). Proof. eauto using closed_up with sts. Qed. Lemma up_closed S T : closed T S → up_set T S ≡ S. Proof. - intros; split; auto using subseteq_up_set; intros s. + intros; split; auto using suseteq_up_set; intros s. unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?). induction Hstep; eauto using closed_step. Qed. -Lemma up_set_subseteq T1 T2 S1 S2 : - closed (T2 ∖ T1) S2 → up_set (T2 ∖ T1) (S1 ∩ S2) ⊆ S2. -Proof. - intros ? s2; unfold up_set; rewrite elem_of_bind; intros (s1&?&?). - apply closed_steps with (T2 ∖ T1) s1; auto with sts. -Qed. Global Instance sts_dra : DRA (t R tok). Proof. split. @@ -153,13 +140,13 @@ Proof. * by destruct 1; constructor; setoid_subst. * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst. * by do 2 destruct 1; constructor; setoid_subst. - * by do 2 destruct 1; inversion_clear 1; econstructor; setoid_subst. * assert (∀ T T' S s, closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). { intros S T T' s [??]; esolve_elem_of. } destruct 3; simpl in *; auto using closed_op with sts. * intros []; simpl; eauto using closed_up, closed_up_set with sts. - * destruct 3; simpl in *; setoid_subst; eauto using closed_up with sts. + * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst; + rewrite ?disjoint_union_difference; auto using closed_up with sts. eapply closed_up_set; eauto 2 using closed_disjoint with sts. * intros [] [] []; constructor; rewrite ?(associative _); auto with sts. * destruct 4; inversion_clear 1; constructor; auto with sts. @@ -168,22 +155,24 @@ Proof. * destruct 3; constructor; auto with sts. * intros []; constructor; auto using elem_of_up with sts. * intros [|S T]; constructor; auto with sts. - assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts. + assert (S ⊆ up_set ∅ S); auto using suseteq_up_set with sts. * intros [s T|S T]; constructor; auto with sts. + by rewrite (up_closed (up _ _)) by auto using closed_up with sts. + by rewrite (up_closed (up_set _ _)) by auto using closed_up_set with sts. - * destruct 3 as [S1 S2| |]; simpl; - match goal with |- _ ≼ frag ?S _ => apply frag_frag_included with S end; - eauto using closed_up_empty, closed_up_set_empty; - unfold up_set; esolve_elem_of. - * destruct 3 as [S1 S2 T1 T2| |]; econstructor; eauto with sts. - by setoid_replace ((T1 ∪ T2) ∖ T1) with T2 by esolve_elem_of. - * destruct 3; constructor; eauto using elem_of_up with sts. - * destruct 3 as [S1 S2 T1 T2 S'| |]; constructor; - rewrite ?(commutative _ (_ ∖ _)), <-?union_difference; auto with sts. - assert (S2 ⊆ up_set (T2 ∖ T1) S2) by eauto using subseteq_up_set. - assert (up_set (T2 ∖ T1) (S1 ∩ S') ⊆ S') by eauto using up_set_subseteq. - esolve_elem_of. + * intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)). + destruct Hxz; inversion_clear Hy; simpl; split_ands; + auto using closed_up_set_empty, closed_up_empty; + constructor; unfold up_set; auto with sts. + * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; + constructor; eauto using elem_of_up; auto with sts. + * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |]; + inversion Hy; clear Hy; constructor; setoid_subst; + rewrite ?disjoint_union_difference by done; auto. + split; [|apply intersection_greatest; auto using suseteq_up_set with sts]. + apply intersection_greatest; [auto with sts|]. + intros s2; rewrite elem_of_intersection. + unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?). + apply closed_steps with T2 s1; auto with sts. Qed. Lemma step_closed s1 s2 T1 T2 S Tf : step (s1,T1) (s2,T2) → closed Tf S → s1 ∈ S → T1 ∩ Tf ≡ ∅ → @@ -198,16 +187,15 @@ End sts. Section sts_ra. Context {A B : Type} `{∀ x y : B, Decision (x = y)}. -Context (R : relation A) (tok : A → bset B). +Context (R : relation A) (tok : A → set B). Definition sts := validity (valid : sts.t R tok → Prop). Global Instance sts_unit : Unit sts := validity_unit _. Global Instance sts_op : Op sts := validity_op _. -Global Instance sts_included : Included sts := validity_included _. Global Instance sts_minus : Minus sts := validity_minus _. Global Instance sts_ra : RA sts := validity_ra _. -Definition sts_auth (s : A) (T : bset B) : sts := to_validity (sts.auth s T). -Definition sts_frag (S : set A) (T : bset B) : sts := +Definition sts_auth (s : A) (T : set B) : sts := to_validity (sts.auth s T). +Definition sts_frag (S : set A) (T : set B) : sts := to_validity (sts.frag S T). Lemma sts_update s1 s2 T1 T2 : sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇝ sts_auth s2 T2. diff --git a/prelude/collections.v b/prelude/collections.v index 619134db21a72ae5717e1a6659093b43f7b76dac..a0bbafe61a4e368eec1ba446070aa5e391823556 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -297,6 +297,8 @@ Section collection. Proof. esolve_elem_of. Qed. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Proof. esolve_elem_of. Qed. + Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y. + Proof. esolve_elem_of. Qed. Section leibniz. Context `{!LeibnizEquiv C}. @@ -315,6 +317,8 @@ Section collection. Lemma difference_intersection_distr_l_L X Y Z : (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. + Lemma disjoint_union_difference_L X Y : X ∩ Y = ∅ → (X ∪ Y) ∖ X = Y. + Proof. unfold_leibniz. apply disjoint_union_difference. Qed. End leibniz. Section dec.