### Shorter names for common math notions.

`Also do some minor clean up.`
parent ba6d9390
 ... ... @@ -59,9 +59,9 @@ Program Instance agree_op : Op (agree A) := λ x y, Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed. Instance agree_unit : Unit (agree A) := id. Instance agree_minus : Minus (agree A) := λ x y, x. Instance: Commutative (≡) (@op (agree A) _). Instance: Comm (≡) (@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. Definition agree_idemp (x : agree A) : x ⋅ x ≡ x. Proof. split; naive_solver. Qed. Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n). Proof. ... ... @@ -79,18 +79,18 @@ Proof. eauto using agree_valid_le. Qed. Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _). Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed. Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed. Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _. Instance: Associative (≡) (@op (agree A) _). Instance: Assoc (≡) (@op (agree A) _). Proof. intros x y z; split; simpl; intuition; repeat match goal with H : agree_is_valid _ _ |- _ => clear H end; by cofe_subst; rewrite !agree_idempotent. by cofe_subst; rewrite !agree_idemp. 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. by intros [z Hz]; rewrite Hz assoc agree_idemp. Qed. Definition agree_cmra_mixin : CMRAMixin (agree A). Proof. ... ... @@ -99,7 +99,7 @@ Proof. * 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_idempotent. * intros x; apply agree_idemp. * by intros x y n [(?&?&?) ?]. * by intros x y n; rewrite agree_includedN. Qed. ... ... @@ -108,13 +108,13 @@ Proof. intros Hxy; apply Hxy. Qed. Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ≡{n}≡ y. Proof. move=> Hval [z Hy]; move: Hval; rewrite Hy. by move=> /agree_op_inv->; rewrite agree_idempotent. by move=> /agree_op_inv->; rewrite agree_idemp. Qed. Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A). Proof. intros n x y1 y2 Hval Hx; exists (x,x); simpl; split. * by rewrite agree_idempotent. * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent. * by rewrite agree_idemp. * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp. Qed. Canonical Structure agreeRA : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin. ... ... @@ -125,7 +125,7 @@ Solve Obligations with done. Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree. Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed. Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _. Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree). Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree). Proof. by intros x y [_ Hxy]; apply Hxy. Qed. Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x. Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed. ... ...
 ... ... @@ -106,10 +106,10 @@ Proof. * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'. * intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S. * by split; simpl; rewrite associative. * by split; simpl; rewrite commutative. * by split; simpl; rewrite assoc. * by split; simpl; rewrite comm. * by split; simpl; rewrite ?cmra_unit_l. * by split; simpl; rewrite ?cmra_unit_idempotent. * by split; simpl; rewrite ?cmra_unit_idemp. * intros n ??; rewrite! auth_includedN; intros [??]. by split; simpl; apply cmra_unit_preservingN. * assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a). ... ... @@ -153,8 +153,8 @@ Lemma auth_update a a' b b' : Proof. move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *. destruct (Hab n (bf1 ⋅ bf2)) as [Ha' ?]; auto. { by rewrite Ha left_id associative. } split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done]. { by rewrite Ha left_id assoc. } split; [by rewrite Ha' left_id assoc; apply cmra_includedN_l|done]. Qed. Lemma auth_local_update L `{!LocalUpdate Lv L} a a' : ... ... @@ -170,7 +170,7 @@ Lemma auth_update_op_l a a' b : Proof. by intros; apply (auth_local_update _). Qed. Lemma auth_update_op_r a a' b : ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b). Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed. Proof. rewrite -!(comm _ b); apply auth_update_op_l. Qed. (* This does not seem to follow from auth_local_update. The trouble is that given ✓ (L a ⋅ a'), Lv a ... ...
 ... ... @@ -43,10 +43,10 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := { (* valid *) mixin_cmra_validN_S n x : ✓{S n} x → ✓{n} x; (* monoid *) mixin_cmra_associative : Associative (≡) (⋅); mixin_cmra_commutative : Commutative (≡) (⋅); mixin_cmra_assoc : Assoc (≡) (⋅); mixin_cmra_comm : Comm (≡) (⋅); mixin_cmra_unit_l x : unit x ⋅ x ≡ x; mixin_cmra_unit_idempotent x : unit (unit x) ≡ unit 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_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 ... ... @@ -101,14 +101,14 @@ Section cmra_mixin. Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed. Lemma cmra_validN_S n x : ✓{S n} x → ✓{n} x. Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed. Global Instance cmra_associative : Associative (≡) (@op A _). Proof. apply (mixin_cmra_associative _ (cmra_mixin A)). Qed. Global Instance cmra_commutative : Commutative (≡) (@op A _). Proof. apply (mixin_cmra_commutative _ (cmra_mixin A)). Qed. Global Instance cmra_assoc : Assoc (≡) (@op A _). Proof. apply (mixin_cmra_assoc _ (cmra_mixin A)). Qed. Global Instance cmra_comm : Comm (≡) (@op A _). Proof. apply (mixin_cmra_comm _ (cmra_mixin A)). Qed. Lemma cmra_unit_l x : unit x ⋅ x ≡ x. Proof. apply (mixin_cmra_unit_l _ (cmra_mixin A)). Qed. Lemma cmra_unit_idempotent x : unit (unit x) ≡ unit x. Proof. apply (mixin_cmra_unit_idempotent _ (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_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x. ... ... @@ -166,7 +166,7 @@ Proof. apply (ne_proper _). Qed. Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _). Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy (commutative _ x1) Hx (commutative _ y2). by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed. Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _). Proof. apply (ne_proper_2 _). Qed. ... ... @@ -217,15 +217,15 @@ Proof. induction 2; eauto using cmra_validN_S. Qed. Lemma cmra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_l. Qed. Lemma cmra_validN_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y. Proof. rewrite (commutative _ x); apply cmra_validN_op_l. Qed. Proof. rewrite (comm _ x); apply cmra_validN_op_l. Qed. Lemma cmra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y. Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed. (** ** Units *) Lemma cmra_unit_r x : x ⋅ unit x ≡ x. Proof. by rewrite (commutative _ x) cmra_unit_l. Qed. Proof. by rewrite (comm _ x) cmra_unit_l. Qed. Lemma cmra_unit_unit x : unit x ⋅ unit x ≡ unit x. Proof. by rewrite -{2}(cmra_unit_idempotent x) cmra_unit_r. Qed. Proof. by rewrite -{2}(cmra_unit_idemp x) cmra_unit_r. Qed. Lemma cmra_unit_validN x n : ✓{n} x → ✓{n} unit x. Proof. rewrite -{1}(cmra_unit_l x); apply cmra_validN_op_l. Qed. Lemma cmra_unit_valid x : ✓ x → ✓ unit x. ... ... @@ -243,7 +243,7 @@ Proof. split. * by intros x; exists (unit x); rewrite cmra_unit_r. * intros x y z [z1 Hy] [z2 Hz]; exists (z1 ⋅ z2). by rewrite (associative _) -Hy -Hz. by rewrite assoc -Hy -Hz. Qed. Global Instance cmra_included_preorder: PreOrder (@included A _ _). Proof. ... ... @@ -265,22 +265,22 @@ Proof. by exists y. Qed. Lemma cmra_included_l x y : x ≼ x ⋅ y. Proof. by exists y. Qed. Lemma cmra_includedN_r n x y : y ≼{n} x ⋅ y. Proof. rewrite (commutative op); apply cmra_includedN_l. Qed. Proof. rewrite (comm op); apply cmra_includedN_l. Qed. Lemma cmra_included_r x y : y ≼ x ⋅ y. Proof. rewrite (commutative op); apply cmra_included_l. Qed. 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_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. Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed. Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. Lemma cmra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y. Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed. Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (assoc op). Qed. Lemma cmra_preservingN_r n x y z : x ≼{n} y → x ⋅ z ≼{n} y ⋅ z. Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed. Proof. by intros; rewrite -!(comm _ z); apply cmra_preservingN_l. Qed. Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z. Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed. Proof. by intros; rewrite -!(comm _ z); apply cmra_preserving_l. Qed. Lemma cmra_included_dist_l x1 x2 x1' n : x1 ≼ x2 → x1' ≡{n}≡ x1 → ∃ x2', x1' ≼ x2' ∧ x2' ≡{n}≡ x2. ... ... @@ -321,7 +321,7 @@ Section identity. Lemma cmra_empty_least x : ∅ ≼ x. Proof. by exists x; rewrite left_id. Qed. Global Instance cmra_empty_right_id : RightId (≡) ∅ (⋅). Proof. by intros x; rewrite (commutative op) left_id. Qed. Proof. by intros x; rewrite (comm op) left_id. Qed. Lemma cmra_unit_empty : unit ∅ ≡ ∅. Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed. End identity. ... ... @@ -336,7 +336,7 @@ Lemma local_update L `{!LocalUpdate Lv L} x y : Proof. by rewrite equiv_dist=>?? n; apply (local_updateN L). Qed. Global Instance local_update_op x : LocalUpdate (λ _, True) (op x). Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed. Proof. split. apply _. by intros n y1 y2 _ _; rewrite assoc. Qed. (** ** Updates *) Global Instance cmra_update_preorder : PreOrder (@cmra_update A). ... ... @@ -366,10 +366,10 @@ Lemma cmra_updateP_op (P1 P2 Q : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ~~>: Q. Proof. intros Hx1 Hx2 Hy z n ?. destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite associative. destruct (Hx1 (x2 ⋅ z) n) as (y1&?&?); first by rewrite assoc. destruct (Hx2 (y1 ⋅ z) n) as (y2&?&?); first by rewrite associative (commutative _ x2) -associative. exists (y1 ⋅ y2); split; last rewrite (commutative _ y1) -associative; auto. first by rewrite assoc (comm _ x2) -assoc. exists (y1 ⋅ y2); split; last rewrite (comm _ y1) -assoc; auto. Qed. Lemma cmra_updateP_op' (P1 P2 : A → Prop) x1 x2 : x1 ~~>: P1 → x2 ~~>: P2 → x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2. ... ... @@ -448,10 +448,10 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := { ra_validN_ne :> Proper ((≡) ==> impl) valid; ra_minus_ne :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* monoid *) ra_associative :> Associative (≡) (⋅); ra_commutative :> Commutative (≡) (⋅); ra_assoc :> Assoc (≡) (⋅); ra_comm :> Comm (≡) (⋅); ra_unit_l x : unit x ⋅ x ≡ x; ra_unit_idempotent x : unit (unit x) ≡ unit x; ra_unit_idemp x : unit (unit x) ≡ unit x; ra_unit_preserving x y : x ≼ y → unit x ≼ unit y; ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x; ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y ... ... @@ -524,10 +524,10 @@ Section prod. * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2]; split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2. * by intros n x [??]; split; apply cmra_validN_S. * split; simpl; apply (associative _). * split; simpl; apply (commutative _). * split; simpl; apply cmra_unit_l. * split; simpl; apply cmra_unit_idempotent. * by split; rewrite /= assoc. * 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 n x y [??]; split; simpl in *; eauto using cmra_validN_op_l. ... ...
 ... ... @@ -22,21 +22,21 @@ Global Instance big_op_permutation : Proper ((≡ₚ) ==> (≡)) big_op. Proof. induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto. * by rewrite IH. * by rewrite !(associative _) (commutative _ x). * by rewrite !assoc (comm _ x). * by transitivity (big_op xs2). Qed. Global Instance big_op_proper : Proper ((≡) ==> (≡)) big_op. Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed. Lemma big_op_app xs ys : big_op (xs ++ ys) ≡ big_op xs ⋅ big_op ys. Proof. induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _). by rewrite IH (associative _). induction xs as [|x xs IH]; simpl; first by rewrite ?left_id. by rewrite IH assoc. Qed. Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys. Proof. induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=. * by apply cmra_preserving_l. * by rewrite !associative (commutative _ y). * by rewrite !assoc (comm _ y). * by transitivity (big_op ys); last apply cmra_included_r. * by transitivity (big_op ys). Qed. ... ... @@ -58,7 +58,7 @@ Qed. Lemma big_opM_singleton i x : big_opM ({[i ↦ x]} : M A) ≡ x. Proof. rewrite -insert_empty big_opM_insert /=; last auto using lookup_empty. by rewrite big_opM_empty (right_id _ _). by rewrite big_opM_empty right_id. Qed. Global Instance big_opM_proper : Proper ((≡) ==> (≡)) (big_opM : M A → _). Proof. ... ...
 ... ... @@ -25,7 +25,7 @@ Module ra_reflection. Section ra_reflection. eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <\$> flatten e). Proof. by induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2. rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2. Qed. Lemma flatten_correct Σ e1 e2 : flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2. ... ...
 ... ... @@ -337,7 +337,7 @@ Section later. Canonical Structure laterC : cofeT := CofeT later_cofe_mixin. Global Instance Next_contractive : Contractive (@Next A). Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Next A). Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). Proof. by intros x y. Qed. End later. ... ...
 ... ... @@ -46,14 +46,14 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := { dra_unit_valid x : ✓ x → ✓ unit x; dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x); (* monoid *) dra_associative :> Associative (≡) (⋅); dra_assoc :> Assoc (≡) (⋅); dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z; dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z; dra_symmetric :> Symmetric (@disjoint A _); dra_commutative x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x; dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x; dra_unit_disjoint_l x : ✓ x → unit x ⊥ x; dra_unit_l x : ✓ x → unit x ⋅ x ≡ x; dra_unit_idempotent x : ✓ x → unit (unit x) ≡ unit x; dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x; dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y; dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x; dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y ... ... @@ -73,12 +73,12 @@ Qed. Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y. Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed. Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z. Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed. Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed. Lemma dra_disjoint_move_r x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z. Proof. intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl. apply dra_disjoint_move_l; auto; by rewrite dra_commutative. intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl. 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. ... ... @@ -114,11 +114,11 @@ Proof. + 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 |intros; apply (associative _)]. * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative. |by intros; rewrite assoc]. * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm. * 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 px ?]; split; naive_solver eauto using dra_unit_idemp. * 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) ... ...
 ... ... @@ -31,9 +31,9 @@ Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A). Proof. by constructor. Qed. Global Instance Excl_inj : Injective (≡) (≡) (@Excl A). Global Instance Excl_inj : Inj (≡) (≡) (@Excl A). Proof. by inversion_clear 1. Qed. Global Instance Excl_dist_inj n : Injective (dist n) (dist n) (@Excl A). Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A). Proof. by inversion_clear 1. Qed. Program Definition excl_chain (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A := ... ...
 ... ... @@ -121,10 +121,10 @@ Proof. * by intros n m1 m2 Hm ? i; rewrite -(Hm i). * by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i). * intros n m Hm i; apply cmra_validN_S, Hm. * by intros m1 m2 m3 i; rewrite !lookup_op associative. * by intros m1 m2 i; rewrite !lookup_op commutative. * by intros m1 m2 m3 i; rewrite !lookup_op assoc. * 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_idempotent. * 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 n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). ... ...
 ... ... @@ -141,10 +141,10 @@ Section iprod_cmra. * by intros n f1 f2 Hf ? x; rewrite -(Hf x). * by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i). * intros n f Hf x; apply cmra_validN_S, Hf. * by intros f1 f2 f3 x; rewrite iprod_lookup_op associative. * by intros f1 f2 x; rewrite iprod_lookup_op commutative. * by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc. * 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_idempotent. * 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 n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. ... ...
 ... ... @@ -45,7 +45,7 @@ Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A). Proof. by constructor. Qed. Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A). Proof. inversion_clear 1; split; eauto. Qed. Global Instance Some_dist_inj : Injective (dist n) (dist n) (@Some A). Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A). Proof. by inversion_clear 1. Qed. Global Instance None_timeless : Timeless (@None A). Proof. inversion_clear 1; constructor. Qed. ... ... @@ -92,10 +92,10 @@ Proof. * by destruct 1; rewrite /validN /option_validN //=; cofe_subst. * by destruct 1; inversion_clear 1; constructor; cofe_subst. * intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S. * intros [x|] [y|] [z|]; constructor; rewrite ?associative; auto. * intros [x|] [y|]; constructor; rewrite 1?commutative; auto. * intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto. * intros [x|] [y|]; constructor; rewrite 1?comm; auto. * by intros [x|]; constructor; rewrite cmra_unit_l. * by intros [x|]; constructor; rewrite cmra_unit_idempotent. * 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 n [x|] [y|]; rewrite /validN /option_validN /=; ... ...
 ... ... @@ -151,7 +151,7 @@ Proof. * 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. * intros [] [] []; constructor; rewrite ?assoc; auto with sts. * destruct 4; inversion_clear 1; constructor; auto with sts. * destruct 4; inversion_clear 1; constructor; auto with sts. * destruct 1; constructor; auto with sts. ... ...
 ... ... @@ -140,7 +140,7 @@ Next Obligation. intros M P Q x y n1 n2 (x1&x2&Hx&?&?) Hxy ??. assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?). { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l. apply dist_le with n1; auto. by rewrite (associative op) -Hx Hy. } apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. } clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |]. * apply uPred_weaken with x1 n1; eauto using cmra_validN_op_l. * apply uPred_weaken with x2 n1; eauto using cmra_validN_op_r. ... ... @@ -179,7 +179,7 @@ Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M := Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed. Next Obligation. intros M a x1 x n1 n2 [a' Hx1] [x2 Hx] ??. exists (a' ⋅ x2). by rewrite (associative op) -(dist_le _ _ _ _ Hx1) // Hx. exists (a' ⋅ x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx. Qed. Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M := {| uPred_holds n x := ✓{n} a |}. ... ... @@ -245,11 +245,11 @@ Arguments uPred_holds {_} !_ _ _ /. Global Instance: PreOrder (@uPred_entails M). Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed. Global Instance: AntiSymmetric (≡) (@uPred_entails M). Global Instance: AntiSymm (≡) (@uPred_entails M). Proof. intros P Q HPQ HQP; split; auto. Qed. Lemma equiv_spec P Q : P ≡ Q ↔ P ⊑ Q ∧ Q ⊑ P. Proof. split; [|by intros [??]; apply (anti_symmetric (⊑))]. split; [|by intros [??]; apply (anti_symm (⊑))]. intros HPQ; split; intros x i; apply HPQ. Qed. Global Instance entails_proper : ... ... @@ -434,7 +434,7 @@ Proof. intros; apply const_elim with φ; eauto. Qed. Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R. Proof. intros; apply const_elim with φ; eauto. Qed. Lemma const_equiv (φ : Prop) : φ → (■ φ : uPred M)%I ≡ True%I. Proof. intros; apply (anti_symmetric _); auto using const_intro. Qed. Proof. intros; apply (anti_symm _); auto using const_intro. Qed. Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b). Proof. intros ->; apply eq_refl. Qed. Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a). ... ... @@ -484,57 +484,57 @@ Global Instance exist_mono' A : Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_exist M A). Proof. intros P1 P2; apply exist_mono. Qed. Global Instance and_idem : Idempotent (≡) (@uPred_and M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Global Instance or_idem : Idempotent (≡) (@uPred_or M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Global Instance and_comm : Commutative (≡) (@uPred_and M). Proof. intros P Q; apply (anti_symmetric (⊑)); auto. Qed. Global Instance and_idem : IdemP (≡) (@uPred_and M). Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance or_idem : IdemP (≡) (@uPred_or M). Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance and_comm : Comm (≡) (@uPred_and M). Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed. Global Instance True_and : LeftId (≡) True%I (@uPred_and M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance and_True : RightId (≡) True%I (@uPred_and M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance False_and : LeftAbsorb (≡) False%I (@uPred_and M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance and_False : RightAbsorb (≡) False%I (@uPred_and M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance True_or : LeftAbsorb (≡) True%I (@uPred_or M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance or_True : RightAbsorb (≡) True%I (@uPred_or M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance False_or : LeftId (≡) False%I (@uPred_or M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance or_False : RightId (≡) False%I (@uPred_or M). Proof. intros P; apply (anti_symmetric (⊑)); auto. Qed. Global Instance and_assoc : Associative (≡) (@uPred_and M). Proof. intros P Q R; apply (anti_symmetric (⊑)); auto. Qed. Global Instance or_comm : Commutative (≡) (@uPred_or M). Proof. intros P Q; apply (anti_symmetric (⊑)); auto. Qed. Global Instance or_assoc : Associative (≡) (@uPred_or M). Proof. intros P Q R; apply (anti_symmetric (⊑)); auto. Qed. Proof. intros P; apply (anti_symm (⊑)); auto. Qed. Global Instance and_assoc : Assoc (≡) (@uPred_and M). Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed. Global Instance or_comm : Comm (≡) (@uPred_or M). Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed. Global Instance or_assoc : Assoc (≡) (@uPred_or M). Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed. Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M). Proof. intros P; apply (anti_symmetric (⊑)). intros P; apply (anti_symm (⊑)). * by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r. * by apply impl_intro_l; rewrite left_id. Qed. Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I. Proof. apply (anti_symmetric (⊑)); first auto. apply (anti_symm (⊑)); first auto. do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto. Qed. Lemma or_and_r P Q R : (P ∧ Q ∨ R)%I ≡ ((P ∨ R) ∧ (Q ∨ R))%I. Proof. by rewrite -!(commutative _ R) or_and_l. Qed. Proof. by rewrite -!(comm _ R) or_and_l. Qed. Lemma and_or_l P Q R : (P ∧ (Q ∨ R))%I ≡ (P ∧ Q ∨ P ∧ R)%I. Proof. apply (anti_symmetric (⊑)); last auto. apply (anti_symm (⊑)); last auto. apply impl_elim_r', or_elim; apply impl_intro_l; auto. Qed. Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I. Proof. by rewrite -!(commutative _ R) and_or_l. Qed. Proof. by rewrite -!(comm _ R) and_or_l. Qed. Lemma and_exist_l {A} P (Q : A → uPred M) : (P ∧ ∃ a, Q a)%I ≡ (∃ a, P ∧ Q a)%I. Proof. apply (anti_symmetric (⊑)). apply (anti_symm (⊑)). - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.