Commit aa947529 by Robbert Krebbers

### Simplify CMRA axioms.

```I have simplified the following CMRA axioms:

cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y;
cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y;

By dropping off the step-index, so into:

cmra_unit_preservingN x y : x ≼ y → unit x ≼ unit y;
cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y;

The old axioms can be derived.```
parent e38e903b
 ... ... @@ -92,6 +92,11 @@ Proof. by cofe_subst; rewrite !agree_idemp. Qed. Lemma agree_included (x y : agree A) : x ≼ y ↔ y ≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. by intros [z Hz]; rewrite Hz assoc agree_idemp. Qed. Lemma agree_includedN n (x y : agree A) : x ≼{n} y ↔ y ≡{n}≡ x ⋅ y. Proof. split; [|by intros ?; exists y]. ... ... @@ -114,7 +119,7 @@ Proof. symmetry; apply dist_le with n; try apply Hx; auto. - intros x; apply agree_idemp. - by intros n x y [(?&?&?) ?]. - by intros n x y; rewrite agree_includedN. - 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. ... ...
 ... ... @@ -125,13 +125,13 @@ Proof. - by split; simpl; rewrite comm. - by split; simpl; rewrite ?cmra_unit_l. - by split; simpl; rewrite ?cmra_unit_idemp. - intros n ??; rewrite! auth_includedN; intros [??]. by split; simpl; apply cmra_unit_preservingN. - intros ??; rewrite! auth_included; intros [??]. by split; simpl; apply cmra_unit_preserving. - assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a). { 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 n ??; rewrite auth_includedN; - by intros ??; rewrite auth_included; intros [??]; split; simpl; apply cmra_op_minus. - intros n x y1 y2 ? [??]; simpl in *. destruct (cmra_extend n (authoritative x) (authoritative y1) ... ...
 ... ... @@ -48,9 +48,9 @@ Record CMRAMixin A mixin_cmra_comm : Comm (≡) (⋅); mixin_cmra_unit_l x : unit x ⋅ x ≡ x; mixin_cmra_unit_idemp x : unit (unit x) ≡ unit x; mixin_cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y; mixin_cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y; mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; mixin_cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y; mixin_cmra_op_minus 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 } ... ... @@ -112,11 +112,11 @@ Section cmra_mixin. Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed. Lemma cmra_unit_idemp x : unit (unit x) ≡ unit x. Proof. apply (mixin_cmra_unit_idemp _ (cmra_mixin A)). Qed. Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y. Proof. apply (mixin_cmra_unit_preservingN _ (cmra_mixin A)). Qed. Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y. Proof. apply (mixin_cmra_unit_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_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. Lemma cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y. Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed. Lemma cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → ... ... @@ -243,12 +243,16 @@ Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed. Lemma cmra_unit_valid x : ✓ x → ✓ unit x. Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed. (** ** Minus *) Lemma cmra_op_minus' n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y. Proof. intros [z ->]. by rewrite cmra_op_minus; 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. symmetry; apply cmra_op_minus, Hxy. by rewrite cmra_op_minus'. Qed. Global Instance cmra_includedN_preorder n : PreOrder (@includedN A _ _ n). Proof. ... ... @@ -281,8 +285,11 @@ Proof. rewrite (comm op); apply cmra_includedN_l. Qed. Lemma cmra_included_r x y : y ≼ x ⋅ y. Proof. rewrite (comm op); apply cmra_included_l. Qed. Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y. Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed. Lemma cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y. Proof. intros [z ->]. apply cmra_included_includedN, cmra_unit_preserving, cmra_included_l. Qed. Lemma cmra_included_unit x : unit x ≼ x. Proof. by exists x; rewrite cmra_unit_l. Qed. Lemma cmra_preservingN_l n x y z : x ≼{n} y → z ⋅ x ≼{n} z ⋅ y. ... ... @@ -301,12 +308,6 @@ Proof. by rewrite Hx1 Hx2. Qed. (** ** Minus *) Lemma cmra_op_minus' x y : x ≼ y → x ⋅ y ⩪ x ≡ y. Proof. rewrite cmra_included_includedN equiv_dist; eauto using cmra_op_minus. Qed. (** ** Timeless *) Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y. Proof. ... ... @@ -565,10 +566,10 @@ Section prod. - by split; rewrite /= comm. - by split; rewrite /= cmra_unit_l. - by split; rewrite /= cmra_unit_idemp. - intros n x y; rewrite !prod_includedN. by intros [??]; split; apply cmra_unit_preservingN. - intros x y; rewrite !prod_included. by intros [??]; split; apply cmra_unit_preserving. - intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. - intros n x y; rewrite prod_includedN; intros [??]. - intros x y; rewrite prod_included; intros [??]. by split; apply cmra_op_minus. - intros n x y1 y2 [??] [??]; simpl in *. destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto. ... ...
 ... ... @@ -113,9 +113,9 @@ Proof. - by intros [?| |] [?| |]; constructor. - by intros [?| |]; constructor. - constructor. - by intros n [?| |] [?| |]; exists ∅. - by intros [?| |] [?| |]; exists ∅. - by intros n [?| |] [?| |]. - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor. - 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) ... ...
 ... ... @@ -110,7 +110,7 @@ Proof. split. - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm. - intros Hm; exists (m2 ⩪ m1); intros i. by rewrite lookup_op lookup_minus cmra_op_minus'. by rewrite lookup_op lookup_minus cmra_op_minus. Qed. Lemma map_includedN_spec (m1 m2 : gmap K A) n : m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i. ... ... @@ -118,7 +118,7 @@ Proof. split. - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm. - intros Hm; exists (m2 ⩪ m1); intros i. by rewrite lookup_op lookup_minus cmra_op_minus. by rewrite lookup_op lookup_minus cmra_op_minus'. Qed. Definition map_cmra_mixin : CMRAMixin (gmap K A). ... ... @@ -136,11 +136,11 @@ Proof. - by intros m1 m2 i; rewrite !lookup_op comm. - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l. - by intros m i; rewrite !lookup_unit cmra_unit_idemp. - intros n x y; rewrite !map_includedN_spec; intros Hm i. by rewrite !lookup_unit; apply cmra_unit_preservingN. - intros x y; rewrite !map_included_spec; intros Hm i. by rewrite !lookup_unit; apply cmra_unit_preserving. - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). by rewrite -lookup_op. - intros n x y; rewrite map_includedN_spec=> ? i. - intros x y; rewrite map_included_spec=> ? i. by rewrite lookup_op lookup_minus cmra_op_minus. - intros n m m1 m2 Hm Hm12. assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12' ... ...
 ... ... @@ -126,13 +126,20 @@ Section iprod_cmra. Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl. Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl. Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x. 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 /minus /iprod_minus cmra_op_minus. Qed. Lemma iprod_includedN_spec n (f g : iprod B) : f ≼{n} g ↔ ∀ x, f x ≼{n} 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 /minus /iprod_minus cmra_op_minus'. Qed. Definition iprod_cmra_mixin : CMRAMixin (iprod B). Proof. ... ... @@ -149,10 +156,10 @@ Section iprod_cmra. - by intros f1 f2 x; rewrite iprod_lookup_op comm. - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l. - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp. - intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x. by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf. - intros f1 f2; rewrite !iprod_included_spec=> Hf x. by rewrite iprod_lookup_unit; apply cmra_unit_preserving, Hf. - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x. - intros f1 f2; rewrite iprod_included_spec=> Hf x. by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf. - intros n f f1 f2 Hf Hf12. set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). ... ...
 ... ... @@ -71,6 +71,19 @@ Instance option_unit : Unit (option A) := fmap unit. Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)). Instance option_minus : Minus (option A) := difference_with (λ x y, Some (x ⩪ y)). Lemma option_included (mx my : option A) : mx ≼ my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼ y. Proof. split. - intros [mz Hmz]. 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_and?; auto; setoid_subst; eauto using cmra_included_l. - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. Lemma option_includedN n (mx my : option A) : mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y. Proof. ... ... @@ -83,6 +96,7 @@ Proof. - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor). by exists (Some z); constructor. Qed. Lemma None_includedN n (mx : option A) : None ≼{n} mx. Proof. rewrite option_includedN; auto. Qed. Lemma Some_Some_includedN n (x y : A) : x ≼{n} y → Some x ≼{n} Some y. ... ... @@ -102,11 +116,11 @@ Proof. - intros [x|] [y|]; constructor; rewrite 1?comm; auto. - by intros [x|]; constructor; rewrite cmra_unit_l. - by intros [x|]; constructor; rewrite cmra_unit_idemp. - intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto. right; exists (unit x), (unit y); eauto using cmra_unit_preservingN. - intros mx my; rewrite !option_included ;intros [->|(x&y&->&->&?)]; auto. right; exists (unit x), (unit y); eauto using cmra_unit_preserving. - intros n [x|] [y|]; rewrite /validN /option_validN /=; eauto using cmra_validN_op_l. - intros n mx my; rewrite option_includedN. - intros mx my; rewrite option_included. intros [->|(x&y&->&->&?)]; [by destruct my|]. by constructor; apply cmra_op_minus. - intros n mx my1 my2. ... ...
 ... ... @@ -111,11 +111,11 @@ Proof. - by intros ??; constructor; rewrite /= comm. - by intros ?; constructor; rewrite /= cmra_unit_l. - by intros ?; constructor; rewrite /= cmra_unit_idemp. - intros n r1 r2; rewrite !res_includedN. by intros (?&?&?); split_and!; apply cmra_unit_preservingN. - intros r1 r2; rewrite !res_included. by intros (?&?&?); split_and!; apply cmra_unit_preserving. - intros n r1 r2 (?&?&?); split_and!; simpl in *; eapply cmra_validN_op_l; eauto. - intros n r1 r2; rewrite res_includedN; intros (?&?&?). - intros r1 r2; rewrite res_included; intros (?&?&?). by constructor; apply cmra_op_minus. - intros n r r1 r2 (?&?&?) [???]; simpl in *. destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?), ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!