Commit 267f4f99 authored by Robbert Krebbers's avatar Robbert Krebbers

Set level of ✓ to 20 (just like ■, ▷ and □).

parent f2082e90
......@@ -69,7 +69,7 @@ Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x {n} a {n} a
| ExclUnit => {n} (own x)
| ExclUnit => {n} own x
| ExclBot => False
end.
Global Arguments auth_validN _ !_ /.
......@@ -91,9 +91,9 @@ 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.
Lemma authoritative_validN n (x : auth A) : {n} x {n} (authoritative x).
Lemma authoritative_validN n (x : auth A) : {n} x {n} authoritative x.
Proof. by destruct x as [[]]. Qed.
Lemma own_validN n (x : auth A) : {n} x {n} (own x).
Lemma own_validN n (x : auth A) : {n} x {n} own x.
Proof. destruct x as [[]]; naive_solver eauto using cmra_validN_includedN. Qed.
Definition auth_cmra_mixin : CMRAMixin (auth A).
......@@ -158,7 +158,7 @@ Proof.
Qed.
Lemma auth_local_update L `{!LocalUpdate Lv L} a a' :
Lv a (L a')
Lv a L a'
a' a ~~> L a' L a.
Proof.
intros. apply auth_update=>n af ? EQ; split; last done.
......
......@@ -20,11 +20,12 @@ Infix "⩪" := minus (at level 40) : C_scope.
Class ValidN (A : Type) := validN : nat A Prop.
Instance: Params (@validN) 3.
Notation "✓{ n }" := (validN n) (at level 1, format "✓{ n }").
Notation "✓{ n } x" := (validN n x)
(at level 20, n at level 1, format "✓{ n } x").
Class Valid (A : Type) := valid : A Prop.
Instance: Params (@valid) 2.
Notation "✓" := valid (at level 1) : C_scope.
Notation "✓ x" := (valid x) (at level 20) : C_scope.
Instance validN_valid `{ValidN A} : Valid A := λ x, n, {n} x.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := z, y {n} x z.
......@@ -37,7 +38,7 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
(* setoids *)
mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
mixin_cmra_unit_ne n : Proper (dist n ==> dist n) unit;
mixin_cmra_validN_ne n : Proper (dist n ==> impl) ({n});
mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
(* valid *)
mixin_cmra_validN_S n x : {S n} x {n} x;
......@@ -133,7 +134,7 @@ Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅
(** * Morphisms *)
Class CMRAMonotone {A B : cmraT} (f : A B) := {
includedN_preserving n x y : x {n} y f x {n} f y;
validN_preserving n x : {n} x {n} (f x)
validN_preserving n x : {n} x {n} f x
}.
(** * Local updates *)
......@@ -225,9 +226,9 @@ Lemma cmra_unit_r x : x ⋅ unit x ≡ x.
Proof. by rewrite (commutative _ 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.
Lemma cmra_unit_validN x n : {n} x {n} (unit x).
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).
Lemma cmra_unit_valid x : x unit x.
Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
(** ** Order *)
......@@ -404,7 +405,7 @@ Section cmra_monotone.
Proof.
rewrite !cmra_included_includedN; eauto using includedN_preserving.
Qed.
Lemma valid_preserving x : x (f x).
Lemma valid_preserving x : x f x.
Proof. rewrite !cmra_valid_validN; eauto using validN_preserving. Qed.
End cmra_monotone.
......@@ -424,9 +425,9 @@ Section cmra_transport.
Proof. by destruct H. Qed.
Lemma cmra_transport_unit x : T (unit x) = unit (T x).
Proof. by destruct H. Qed.
Lemma cmra_transport_validN n x : {n} (T x) {n} x.
Lemma cmra_transport_validN n x : {n} T x {n} x.
Proof. by destruct H. Qed.
Lemma cmra_transport_valid x : (T x) x.
Lemma cmra_transport_valid x : T x x.
Proof. by destruct H. Qed.
Global Instance cmra_transport_timeless x : Timeless x Timeless (T x).
Proof. by destruct H. Qed.
......@@ -444,7 +445,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
(* setoids *)
ra_op_ne (x : A) : Proper (() ==> ()) (op x);
ra_unit_ne :> Proper (() ==> ()) unit;
ra_validN_ne :> Proper (() ==> impl) ;
ra_validN_ne :> Proper (() ==> impl) valid;
ra_minus_ne :> Proper (() ==> () ==> ()) minus;
(* monoid *)
ra_associative :> Associative () ();
......@@ -502,7 +503,7 @@ Section prod.
Instance prod_op : Op (A * B) := λ x y, (x.1 y.1, x.2 y.2).
Global Instance prod_empty `{Empty A, Empty B} : Empty (A * B) := (, ).
Instance prod_unit : Unit (A * B) := λ x, (unit (x.1), unit (x.2)).
Instance prod_validN : ValidN (A * B) := λ n x, {n} (x.1) {n} (x.2).
Instance prod_validN : ValidN (A * B) := λ n x, {n} x.1 {n} x.2.
Instance prod_minus : Minus (A * B) := λ x y, (x.1 y.1, x.2 y.2).
Lemma prod_included (x y : A * B) : x y x.1 y.1 x.2 y.2.
Proof.
......
......@@ -71,8 +71,7 @@ Proof.
rewrite Hxy -big_opM_insert; last auto using lookup_delete.
by rewrite insert_delete.
Qed.
Lemma big_opM_lookup_valid n m i x :
{n} (big_opM m) m !! i = Some x {n} x.
Lemma big_opM_lookup_valid n m i x : {n} big_opM m m !! i = Some x {n} x.
Proof.
intros Hm ?; revert Hm; rewrite -(big_opM_delete _ i x) //.
apply cmra_validN_op_l.
......
......@@ -26,7 +26,7 @@ Proof.
split; [|intros; transitivity y]; tauto.
Qed.
Instance validity_valid_proper `{Equiv A} (P : A Prop) :
Proper (() ==> iff) ( : validity P Prop).
Proper (() ==> iff) (valid : validity P Prop).
Proof. intros ?? [??]; naive_solver. Qed.
Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
......@@ -43,7 +43,7 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
dra_minus_proper :> Proper (() ==> () ==> ()) minus;
(* validity *)
dra_op_valid x y : x y x y (x y);
dra_unit_valid x : x (unit x);
dra_unit_valid x : x unit x;
dra_minus_valid x y : x y x y (y x);
(* monoid *)
dra_associative :> Associative () ();
......@@ -83,8 +83,8 @@ Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Unfold dra_included.
Notation T := (validity ( : A Prop)).
Lemma validity_valid_car_valid (z : T) : z (validity_car z).
Notation T := (validity (valid : 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,
......
......@@ -87,7 +87,7 @@ Context `{Countable K} {A : cmraT}.
Instance map_op : Op (gmap K A) := merge op.
Instance map_unit : Unit (gmap K A) := fmap unit.
Instance map_validN : ValidN (gmap K A) := λ n m, i, {n} (m!!i).
Instance map_validN : ValidN (gmap K A) := λ n m, i, {n} (m !! i).
Instance map_minus : Minus (gmap K A) := merge minus.
Lemma lookup_op m1 m2 i : (m1 m2) !! i = m1 !! i m2 !! i.
......@@ -171,7 +171,7 @@ Implicit Types a : A.
Lemma map_lookup_validN n m i x : {n} m m !! i {n} Some x {n} x.
Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
Lemma map_insert_validN n m i x : {n} x {n} m {n} (<[i:=x]>m).
Lemma map_insert_validN n m i x : {n} x {n} m {n} <[i:=x]>m.
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
Lemma map_singleton_validN n i x : {n} ({[ i x ]} : gmap K A) {n} x.
Proof.
......
......@@ -118,7 +118,7 @@ Section iprod_cmra.
Instance iprod_op : Op (iprod B) := λ f g x, f x g x.
Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
Instance iprod_validN : ValidN (iprod B) := λ n f, x, {n} (f x).
Instance iprod_validN : ValidN (iprod B) := λ n f, x, {n} f x.
Instance iprod_minus : Minus (iprod B) := λ f g x, f x g x.
Definition iprod_lookup_op f g x : (f g) x = f x g x := eq_refl.
......@@ -197,8 +197,7 @@ Section iprod_cmra.
(** Properties of iprod_singleton. *)
Context `{ x, Empty (B x), x, CMRAIdentity (B x)}.
Lemma iprod_singleton_validN n x (y : B x) :
{n} (iprod_singleton x y) {n} y.
Lemma iprod_singleton_validN n x (y: B x) : {n} iprod_singleton x y {n} y.
Proof.
split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
......
......@@ -87,13 +87,10 @@ Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
Definition option_cmra_mixin : CMRAMixin (option A).
Proof.
split.
* by intros n [x|]; destruct 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* by destruct 1; constructor; apply (_ : Proper (dist n ==> _) _).
* destruct 1; rewrite /validN /option_validN //=.
eapply (_ : Proper (dist _ ==> impl) ({_})); eauto.
* by destruct 1; inversion_clear 1; constructor;
repeat apply (_ : Proper (dist _ ==> _ ==> _) _).
* by intros n [x|]; destruct 1; constructor; cofe_subst.
* by destruct 1; constructor; cofe_subst.
* 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.
......
......@@ -211,7 +211,7 @@ 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.
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
Infix "↔" := uPred_iff : uPred_scope.
......
......@@ -20,9 +20,8 @@ Section auth.
Qed.
(* TODO: Need this to be proven somewhere. *)
(* FIXME ✓ binds too strong, I need parenthesis here. *)
Hypothesis auth_valid :
forall a b, ( (Auth (Excl a) b) : iPropG Λ Σ) ( b', a b b').
forall a b, ( Auth (Excl a) b : iPropG Λ Σ) ( b', a b b').
Definition auth_inv (γ : gname) : iPropG Λ Σ :=
( a, own AuthI γ ( a) φ a)%I.
......
......@@ -33,7 +33,7 @@ Implicit Types a : A.
(** * Properties of to_globalC *)
Instance to_globalF_ne γ n : Proper (dist n ==> dist n) (to_globalF i γ).
Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Lemma to_globalF_validN n γ a : {n} (to_globalF i γ a) {n} a.
Lemma to_globalF_validN n γ a : {n} to_globalF i γ a {n} a.
Proof.
by rewrite /to_globalF
iprod_singleton_validN map_singleton_validN cmra_transport_validN.
......
......@@ -76,7 +76,7 @@ Global Instance res_empty : Empty (res Λ Σ A) := Res ∅ ∅ ∅.
Instance res_unit : Unit (res Λ Σ A) := λ r,
Res (unit (wld r)) (unit (pst r)) (unit (gst r)).
Instance res_validN : ValidN (res Λ Σ A) := λ n r,
{n} (wld r) {n} (pst r) {n} (gst r).
{n} wld r {n} pst r {n} gst r.
Instance res_minus : Minus (res Λ Σ A) := λ r1 r2,
Res (wld r1 wld r2) (pst r1 pst r2) (gst r1 gst r2).
Lemma res_included (r1 r2 : res Λ Σ A) :
......@@ -136,9 +136,9 @@ Definition update_pst (σ : state Λ) (r : res Λ Σ A) : res Λ Σ A :=
Definition update_gst (m : Σ A) (r : res Λ Σ A) : res Λ Σ A :=
Res (wld r) (pst r) (Some m).
Lemma wld_validN n r : {n} r {n} (wld r).
Lemma wld_validN n r : {n} r {n} wld r.
Proof. by intros (?&?&?). Qed.
Lemma gst_validN n r : {n} r {n} (gst r).
Lemma gst_validN n r : {n} r {n} gst r.
Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
Res w1 σ1 m1 Res w2 σ2 m2 = Res (w1 w2) (σ1 σ2) (m1 m2).
......
......@@ -2,8 +2,8 @@ Require Export program_logic.model prelude.co_pset.
Require Export algebra.cmra_big_op algebra.cmra_tactics.
Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 10 ({_} _) => solve_validN.
Local Hint Extern 1 ({_} (gst _)) => apply gst_validN.
Local Hint Extern 1 ({_} (wld _)) => apply wld_validN.
Local Hint Extern 1 ({_} gst _) => apply gst_validN.
Local Hint Extern 1 ({_} wld _) => apply wld_validN.
Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
(σ : state Λ) (rs : gmap positive (iRes Λ Σ)) (r : iRes Λ Σ) := {
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment