Commit 2cbe04e6 by Robbert Krebbers

### Use checkmark for valid.

parent 5696cb01
 ... ... @@ -19,7 +19,7 @@ Global Instance agree_validN : ValidN (agree A) := λ n x, Lemma agree_valid_le (x : agree A) n n' : agree_is_valid x n → n' ≤ n → agree_is_valid x n'. Proof. induction 2; eauto using agree_valid_S. Qed. Global Instance agree_valid : Valid (agree A) := λ x, ∀ n, validN n x. Global Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x. Global Instance agree_equiv : Equiv (agree A) := λ x y, (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧ (∀ n, agree_is_valid x n → x n ={n}= y n). ... ... @@ -100,7 +100,7 @@ Proof. * 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. ✓{n} x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2. Proof. by intros [??] Hxy; apply Hxy. Qed. Global Instance agree_extend : CMRAExtend (agree A). Proof. ... ... @@ -113,12 +113,12 @@ Program Definition to_agree (x : A) : agree A := 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. Lemma agree_car_ne (x y : agree A) n : validN n x → x ={n}= y → x n ={n}= y n. Lemma agree_car_ne (x y : agree A) n : ✓{n} x → x ={n}= y → x n ={n}= y n. Proof. by intros [??] Hxy; apply Hxy. Qed. Lemma agree_cauchy (x : agree A) n i : n ≤ i → validN i x → x n ={n}= x i. Lemma agree_cauchy (x : agree A) n i : n ≤ i → ✓{i} x → x n ={n}= x i. Proof. by intros ? [? Hx]; apply Hx. Qed. Lemma agree_to_agree_inj (x y : agree A) a n : validN n x → x ={n}= to_agree a ⋅ y → x n ={n}= a. ✓{n} x → x ={n}= to_agree a ⋅ y → x n ={n}= a. Proof. by intros; transitivity ((to_agree a ⋅ y) n); [by apply agree_car_ne|]. Qed. ... ...
 ... ... @@ -45,15 +45,15 @@ Qed. Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅. Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x, match authoritative x with | Excl a => own x ≼ a ∧ valid a | ExclUnit => valid (own x) | Excl a => own x ≼ a ∧ ✓ a | ExclUnit => ✓ (own x) | ExclBot => False end. Arguments auth_valid _ _ _ _ !_ /. Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x, match authoritative x with | Excl a => own x ≼{n} a ∧ validN n a | ExclUnit => validN n (own x) | Excl a => own x ≼{n} a ∧ ✓{n} a | ExclUnit => ✓{n} (own x) | ExclBot => n = 0 end. Arguments auth_validN _ _ _ _ _ !_ /. ... ... @@ -76,9 +76,9 @@ Proof. intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto. Qed. Lemma authoritative_validN `{CMRA A} n (x : auth A) : validN n x → validN n (authoritative x). ✓{n} x → ✓{n} (authoritative x). Proof. by destruct x as [[]]. Qed. Lemma own_validN `{CMRA A} n (x : auth A) : validN n x → validN n (own x). Lemma own_validN `{CMRA A} n (x : auth A) : ✓{n} x → ✓{n} (own x). Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed. Instance auth_cmra `{CMRA A} : CMRA (auth A). Proof. ... ...
 ... ... @@ -2,6 +2,7 @@ Require Export iris.ra iris.cofe. Class ValidN (A : Type) := validN : nat → A → Prop. Instance: Params (@validN) 3. Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }"). Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅ z. Notation "x ≼{ n } y" := (includedN n x y) ... ... @@ -14,32 +15,32 @@ Class CMRA A `{Equiv A, Compl A, Unit A, Op A, Valid A, ValidN A, Minus A} := { 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_valid_ne n :> Proper (dist n ==> impl) (✓{n}); cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus; (* valid *) cmra_valid_0 x : validN 0 x; cmra_valid_S n x : validN (S n) x → validN n x; cmra_valid_validN x : valid x ↔ ∀ n, validN n x; cmra_valid_0 x : ✓{0} x; cmra_valid_S n x : ✓{S n} x → ✓{n} x; cmra_valid_validN x : ✓ x ↔ ∀ n, ✓{n} x; (* monoid *) cmra_associative : Associative (≡) (⋅); cmra_commutative : Commutative (≡) (⋅); cmra_unit_l x : unit x ⋅ x ≡ x; cmra_unit_idempotent x : unit (unit x) ≡ unit x; 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_valid_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; 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 n x y1 y2 : validN n x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }. ✓{n} x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }. 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) validN_preserving n x : ✓{n} x → ✓{n} (f x) }. Hint Extern 0 (validN 0 _) => apply cmra_valid_0. Hint Extern 0 (✓{0} _) => apply cmra_valid_0. (** Bundeled version *) Structure cmraT := CMRAT { ... ... @@ -73,12 +74,12 @@ Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A. Canonical Structure cmra_cofeC. (** Updates *) Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A → Prop) := ∀ z n, validN n (x ⋅ z) → ∃ y, P y ∧ validN n (y ⋅ z). Definition cmra_updateP `{Op A, ValidN A} (x : A) (P : A → Prop) := ∀ z n, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z). Instance: Params (@cmra_updateP) 3. Infix "⇝:" := cmra_updateP (at level 70). Definition cmra_update `{Op A, ValidN A} (x y : A) := ∀ z n, validN n (x ⋅ z) → validN n (y ⋅ z). ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z). Infix "⇝" := cmra_update (at level 70). Instance: Params (@cmra_update) 3. ... ... @@ -94,9 +95,9 @@ Proof. symmetry; apply cmra_op_minus, Hxy. Qed. Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n) | 1. Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (✓{n}) | 1. Proof. by split; apply cmra_valid_ne. Qed. Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n) | 1. Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (✓{n}) | 1. Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed. Global Instance cmra_ra : RA A. Proof. ... ... @@ -110,19 +111,19 @@ Proof. * 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. Lemma cmra_valid_op_r x y n : ✓{n} (x ⋅ y) → ✓{n} y. Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed. Lemma cmra_valid_le x n n' : validN n x → n' ≤ n → validN n' x. Lemma cmra_valid_le x n n' : ✓{n} x → n' ≤ n → ✓{n'} x. Proof. induction 2; eauto using cmra_valid_S. Qed. Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (⋅). Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2). Qed. Lemma cmra_unit_valid x n : validN n x → validN n (unit x). Lemma cmra_unit_valid x n : ✓{n} x → ✓{n} (unit x). Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed. Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 : validN 1 (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). ✓{1} (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2). Proof. intros ??? z Hz. destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. ... ... @@ -159,9 +160,9 @@ Proof. * 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. Lemma cmra_valid_includedN x y n : ✓{n} y → x ≼{n} y → ✓{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. Lemma cmra_valid_included x y n : ✓{n} y → x ≼ y → ✓{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. ... ... @@ -203,7 +204,7 @@ Section discrete. Existing Instances discrete_dist discrete_compl. Let discrete_cofe' : Cofe A := discrete_cofe. Instance discrete_validN : ValidN A := λ n x, match n with 0 => True | S n => valid x end. match n with 0 => True | S n => ✓ x end. Instance discrete_cmra : CMRA A. Proof. split; try by (destruct ra; auto). ... ... @@ -224,13 +225,12 @@ Section discrete. Qed. Definition discreteRA : cmraT := CMRAT A. Lemma discrete_updateP (x : A) (P : A → Prop) `{!Inhabited (sig P)} : (∀ z, valid (x ⋅ z) → ∃ y, P y ∧ valid (y ⋅ z)) → x ⇝: P. (∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ⇝: P. Proof. intros Hvalid z [|n]; [|apply Hvalid]. by destruct (_ : Inhabited (sig P)) as [[y ?]]; exists y. Qed. Lemma discrete_update (x y : A) : (∀ z, valid (x ⋅ z) → valid (y ⋅ z)) → x ⇝ y. Lemma discrete_update (x y : A) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ⇝ y. Proof. intros Hvalid z [|n]; [done|apply Hvalid]. Qed. End discrete. Arguments discreteRA _ {_ _ _ _ _ _}. ... ... @@ -241,9 +241,9 @@ Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (∅, ∅). Instance prod_unit `{Unit A, Unit B} : Unit (A * B) := λ x, (unit (x.1), unit (x.2)). Instance prod_valid `{Valid A, Valid B} : Valid (A * B) := λ x, valid (x.1) ∧ valid (x.2). ✓ (x.1) ∧ ✓ (x.2). Instance prod_validN `{ValidN A, ValidN B} : ValidN (A * B) := λ n x, validN n (x.1) ∧ validN n (x.2). ✓{n} (x.1) ∧ ✓{n} (x.2). 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) : ... ...
 ... ... @@ -4,9 +4,9 @@ Require Import prelude.stringmap prelude.natmap. (** option *) Instance option_valid `{Valid A} : Valid (option A) := λ mx, match mx with Some x => valid x | None => True end. match mx with Some x => ✓ 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. match mx with Some x => ✓{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) := ... ... @@ -34,7 +34,7 @@ Proof. * by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _). * destruct 1 as [[?|] [?|]| |]; unfold validN, option_validN; simpl; intros ?; auto using cmra_valid_0; eapply (_ : Proper (dist _ ==> impl) (validN _)); eauto. eapply (_ : Proper (dist _ ==> impl) (✓{_})); eauto. * by destruct 1; inversion_clear 1; constructor; repeat apply (_ : Proper (dist _ ==> _ ==> _) _). * intros [x|]; unfold validN, option_validN; auto using cmra_valid_0. ... ... @@ -82,8 +82,8 @@ Section map. Existing Instances map_dist map_compl map_cofe. Instance map_op `{Op A} : Op (M A) := merge op. Instance map_unit `{Unit A} : Unit (M A) := fmap unit. 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_valid `{Valid A} : Valid (M A) := λ m, ∀ i, ✓ (m !! i). Instance map_validN `{ValidN A} : ValidN (M A) := λ n m, ∀ i, ✓{n} (m!!i). Instance map_minus `{Minus A} : Minus (M A) := merge minus. Lemma lookup_op `{Op A} m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i. Proof. by apply lookup_merge. Qed. ... ... @@ -116,7 +116,7 @@ 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). * intros m i; apply cmra_valid_0. * by intros m i. * intros n m Hm i; apply cmra_valid_S, Hm. * intros m; split; [by intros Hm n i; apply cmra_valid_validN|]. intros Hm i; apply cmra_valid_validN; intros n; apply Hm. ... ...
 ... ... @@ -26,13 +26,11 @@ Proof. split; [|intros; transitivity y]; tauto. Qed. Instance validity_valid_proper `{Equiv A} (P : A → Prop) : Proper ((≡) ==> iff) (valid : validity P → Prop). Proper ((≡) ==> iff) (✓ : validity P → Prop). Proof. intros ?? [??]; naive_solver. Qed. Local Notation V := valid. Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y, ∃ z, y ≡ x ⋅ z ∧ V z ∧ x ⊥ z. ∃ z, y ≡ x ⋅ z ∧ ✓ z ∧ x ⊥ z. Instance: Params (@dra_included) 4. Local Infix "≼" := dra_included. ... ... @@ -44,21 +42,21 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := { dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x); dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* validity *) dra_op_valid x y : V x → V y → x ⊥ y → V (x ⋅ y); dra_unit_valid x : V x → V (unit x); dra_minus_valid x y : V x → V y → x ≼ y → V (y ⩪ x); dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y); dra_unit_valid x : ✓ x → ✓ (unit x); dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x); (* monoid *) dra_associative :> Associative (≡) (⋅); dra_disjoint_ll x y z : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z; dra_disjoint_move_l x y z : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z; 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 : V x → V y → x ⊥ y → x ⋅ y ≡ y ⋅ x; 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_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 dra_commutative 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_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 }. Section dra. ... ... @@ -72,14 +70,14 @@ Proof. * 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. 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 : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z. Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z. Proof. intros ????. rewrite dra_commutative by done. by apply dra_disjoint_ll. Qed. Lemma dra_disjoint_move_r x y z : V x → V y → V z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z. ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z. Proof. intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl. apply dra_disjoint_move_l; auto; by rewrite dra_commutative. ... ... @@ -87,20 +85,20 @@ Qed. Hint Immediate dra_disjoint_move_l dra_disjoint_move_r. Hint Unfold dra_included. Notation T := (validity (valid : A → Prop)). Lemma validity_valid_car_valid (z : T) : V z → V (validity_car z). Notation T := (validity (✓ : A → Prop)). Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ (validity_car z). Proof. apply validity_prf. Qed. Hint Resolve validity_valid_car_valid. Program Instance validity_unit : Unit T := λ x, Validity (unit (validity_car x)) (V x) _. Validity (unit (validity_car x)) (✓ x) _. Solve Obligations with naive_solver auto using dra_unit_valid. 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) _. (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _. Solve Obligations with naive_solver auto using dra_op_valid. 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) _. (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _. Solve Obligations with naive_solver auto using dra_minus_valid. Instance validity_ra : RA T. Proof. ... ... @@ -135,7 +133,7 @@ Proof. Qed. Definition validityRA : cmraT := discreteRA T. Definition validity_update (x y : validityRA) : (∀ z, V x → V z → validity_car x ⊥ z → V y ∧ validity_car y ⊥ z) → x ⇝ y. (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ⇝ y. Proof. intros Hxy; apply discrete_update. intros z (?&?&?); split_ands'; try eapply Hxy; eauto. ... ...
 ... ... @@ -114,7 +114,7 @@ Proof. Qed. (* Updates *) Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y. Lemma excl_update {A} (x : A) y : ✓ y → Excl x ⇝ y. Proof. by destruct y; intros ? [?| |]. Qed. (* Functor *) ... ...
 ... ... @@ -8,7 +8,7 @@ Structure uPred (M : cmraT) : Type := IProp { uPred_ne x1 x2 n : uPred_holds n x1 → x1 ={n}= x2 → uPred_holds n x2; uPred_0 x : uPred_holds 0 x; uPred_weaken x1 x2 n1 n2 : uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → validN n2 x2 → uPred_holds n2 x2 uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2 }. Arguments uPred_holds {_} _ _ _. Hint Resolve uPred_0. ... ... @@ -16,9 +16,9 @@ Add Printing Constructor uPred. Instance: Params (@uPred_holds) 3. Instance uPred_equiv (M : cmraT) : Equiv (uPred M) := λ P Q, ∀ x n, validN n x → P n x ↔ Q n x. ✓{n} x → P n x ↔ Q n x. Instance uPred_dist (M : cmraT) : Dist (uPred M) := λ n P Q, ∀ x n', n' ≤ n → validN n' x → P n' x ↔ Q n' x. n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x. Program Instance uPred_compl (M : cmraT) : Compl (uPred M) := λ c, {| uPred_holds n x := c n n x |}. Next Obligation. by intros M c x y n ??; simpl in *; apply uPred_ne with x. Qed. ... ... @@ -72,7 +72,7 @@ Qed. (** logical entailement *) Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q, ∀ x n, validN n x → P n x → Q n x. ✓{n} x → P n x → Q n x. (** logical connectives *) Program Definition uPred_const {M} (P : Prop) : uPred M := ... ... @@ -89,12 +89,12 @@ Program Definition uPred_or {M} (P Q : uPred M) : uPred M := Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken. Program Definition uPred_impl {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ x' n', x ≼ x' → n' ≤ n → validN n' x' → P n' x' → Q n' x' |}. x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}. Next Obligation. intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????. destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto. assert (x2' ={n2}= x2) as Hx2' by (by apply dist_le with n1). assert (validN n2 x2') by (by rewrite Hx2'); rewrite <-Hx2'. assert (✓{n2} x2') by (by rewrite Hx2'); rewrite <-Hx2'. eauto using uPred_weaken, uPred_ne. Qed. Next Obligation. intros M P Q x1 x2 [|n]; auto with lia. Qed. ... ... @@ -134,7 +134,7 @@ Qed. Program Definition uPred_wand {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ x' n', n' ≤ n → validN n' (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}. n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}. Next Obligation. intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *. rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto. ... ... @@ -172,7 +172,7 @@ Next Obligation. exists (a' ⋅ x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx. Qed. Program Definition uPred_valid {M : cmraT} (a : M) : uPred M := {| uPred_holds n x := validN n a |}. {| uPred_holds n x := ✓{n} a |}. Solve Obligations with naive_solver eauto 2 using cmra_valid_le, cmra_valid_0. Delimit Scope uPred_scope with I. ... ... @@ -196,11 +196,12 @@ Notation "∃ x .. y , P" := Notation "▷ P" := (uPred_later P) (at level 20) : uPred_scope. Notation "□ P" := (uPred_always P) (at level 20) : uPred_scope. Infix "≡" := uPred_eq : uPred_scope. Notation "✓" := uPred_valid (at level 1) : uPred_scope. Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I. Infix "↔" := uPred_iff : uPred_scope. Class TimelessP {M} (P : uPred M) := timelessP x n : validN 1 x → P 1 x → P n x. Class TimelessP {M} (P : uPred M) := timelessP x n : ✓{1} x → P 1 x → P n x. Section logic. Context {M : cmraT}. ... ... @@ -687,7 +688,7 @@ Proof. 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. Lemma uPred_own_valid (a : M) : uPred_own a ⊆ uPred_valid a. Lemma uPred_own_valid (a : M) : uPred_own a ⊆ (✓ a)%I. Proof. intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l. Qed. ... ...
 ... ... @@ -2,6 +2,7 @@ Require Export prelude.collections prelude.relations prelude.fin_maps. Class Valid (A : Type) := valid : A → Prop. Instance: Params (@valid) 2. Notation "✓" := valid (at level 1). Class Unit (A : Type) := unit : A → A. Instance: Params (@unit) 2. ... ... @@ -26,7 +27,7 @@ Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := { ra_equivalence :> Equivalence ((≡) : relation A); ra_op_proper x :> Proper ((≡) ==> (≡)) (op x); ra_unit_proper :> Proper ((≡) ==> (≡)) unit; ra_valid_proper :> Proper ((≡) ==> impl) valid; ra_valid_proper :> Proper ((≡) ==> impl) ✓; ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* monoid *) ra_associative :> Associative (≡) (⋅); ... ... @@ -34,18 +35,18 @@ Class RA A `{Equiv A, Valid A, Unit A, Op A, Minus A} : Prop := { ra_unit_l x : unit x ⋅ x ≡ x; ra_unit_idempotent x : unit (unit x) ≡ unit x; ra_unit_preserving x y : x ≼ y → unit x ≼ unit y; ra_valid_op_l x y : valid (x ⋅ y) → valid x; ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x; ra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y }. Class RAEmpty A `{Equiv A, Valid A, Op A, Empty A} : Prop := { ra_empty_valid : valid ∅; ra_empty_valid : ✓ ∅; 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) valid_preserving x : ✓ x → ✓ (f x) }. (** Big ops *) ... ... @@ -60,11 +61,11 @@ Instance: Params (@big_opM) 4. (** Updates *) Definition ra_update_set `{Op A, Valid A} (x : A) (P : A → Prop) := ∀ z, valid (x ⋅ z) → ∃ y, P y ∧ valid (y ⋅ z). ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z). Instance: Params (@ra_update_set) 3. Infix "⇝:" := ra_update_set (at level 70). Definition ra_update `{Op A, Valid A} (x y : A) := ∀ z, valid (x ⋅ z) → valid (y ⋅ z). ✓ (x ⋅ z) → ✓ (y ⋅ z). Infix "⇝" := ra_update (at level 70). Instance: Params (@ra_update) 3. ... ... @@ -74,14 +75,14 @@ Context `{RA A}. Implicit Types x y z : A. Implicit Types xs ys zs : list A. Global Instance ra_valid_proper' : Proper ((≡) ==> iff) valid. Global Instance ra_valid_proper' : Proper ((≡) ==> iff) ✓. Proof. by intros ???; split; apply ra_valid_proper. Qed. Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (⋅). Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2). Qed. Lemma ra_valid_op_r x y : valid (x ⋅ y) → valid y. Lemma ra_valid_op_r x y : ✓ (x ⋅ y) → ✓ y. Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed. (** ** Units *) ... ...
 ... ... @@ -188,7 +188,7 @@ End sts. Section sts_ra. Context {A B : Type} (R : relation A) (tok : A → set B). Definition sts := validity (valid : sts.t R tok → Prop). Definition sts := validity (✓ : sts.t R tok → Prop). Global Instance sts_equiv : Equiv sts := validity_equiv _. Global Instance sts_unit : Unit sts := validity_unit _. Global Instance sts_op : Op sts := validity_op _. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!