Commit f6909092 authored by Ralf Jung's avatar Ralf Jung

change notation of step-indexed equality to ≡{n}≡

parent fbedbd17
......@@ -16,16 +16,16 @@ Section agree.
Context {A : cofeT}.
Instance agree_validN : ValidN (agree A) := λ n x,
agree_is_valid x n n', n' n x n' ={n'}= x n.
agree_is_valid x n n', n' n x n' {n'} x n.
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.
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).
( n, agree_is_valid x n x n {n} y n).
Instance agree_dist : Dist (agree A) := λ n x y,
( n', n' n agree_is_valid x n' agree_is_valid y n')
( n', n' n agree_is_valid x n' x n' ={n'}= y n').
( n', n' n agree_is_valid x n' x n' {n'} y n').
Program Instance agree_compl : Compl (agree A) := λ c,
{| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
Next Obligation. intros; apply agree_valid_0. Qed.
......@@ -51,14 +51,14 @@ Proof.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
Lemma agree_car_ne (x y : agree A) n : {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} x i n x i ={i}= x n.
Lemma agree_cauchy (x : agree A) n i : {n} x i n x i {i} x n.
Proof. by intros [? Hx]; apply Hx. Qed.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x ={n}= y |}.
agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}.
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.
Instance agree_unit : Unit (agree A) := id.
......@@ -91,7 +91,7 @@ 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.
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.
......@@ -109,9 +109,9 @@ Proof.
* by intros x y n [(?&?&?) ?].
* by intros x y n; rewrite agree_includedN.
Qed.
Lemma agree_op_inv (x1 x2 : agree A) n : {n} (x1 x2) x1 ={n}= x2.
Lemma agree_op_inv (x1 x2 : agree A) n : {n} (x1 x2) x1 {n} x2.
Proof. intros Hxy; apply Hxy. Qed.
Lemma agree_valid_includedN (x y : agree A) n : {n} y x {n} y x ={n}= y.
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.
......@@ -133,7 +133,7 @@ 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).
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.
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.
End agree.
......
......@@ -19,7 +19,7 @@ Implicit Types x y : auth A.
Instance auth_equiv : Equiv (auth A) := λ x y,
authoritative x authoritative y own x own y.
Instance auth_dist : Dist (auth A) := λ n x y,
authoritative x ={n}= authoritative y own x ={n}= own y.
authoritative x {n} authoritative y own x {n} own y.
Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Proof. by split. Qed.
......@@ -148,7 +148,7 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_update a a' b b' :
( n af, {S n} a a ={S n}= a' af b ={S n}= b' af {S n} b)
( n af, {S n} a a {S n} a' af b {S n} b' af {S n} b)
a a' ~~> b b'.
Proof.
move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
......
......@@ -27,7 +27,7 @@ Instance: Params (@valid) 2.
Notation "✓" := valid (at level 1).
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.
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.
......@@ -49,11 +49,11 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
mixin_cmra_unit_idempotent 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
mixin_cmra_op_minus n x y : x {n} y x y x {n} y
}.
Definition CMRAExtendMixin A `{Equiv A, Dist A, Op A, ValidN A} := n x y1 y2,
{n} x x ={n}= y1 y2
{ z | x z.1 z.2 z.1 ={n}= y1 z.2 ={n}= y2 }.
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }.
(** Bundeled version *)
Structure cmraT := CMRAT {
......@@ -115,11 +115,11 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_unit_preservingN _ (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 n x y : x {n} y x y x {n} y.
Proof. apply (mixin_cmra_op_minus _ (cmra_mixin A)). Qed.
Lemma cmra_extend_op n x y1 y2 :
{n} x x ={n}= y1 y2
{ z | x z.1 z.2 z.1 ={n}= y1 z.2 ={n}= y2 }.
{n} x x {n} y1 y2
{ z | x z.1 z.2 z.1 {n} y1 z.2 {n} y2 }.
Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.
......@@ -277,7 +277,7 @@ Lemma cmra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
Proof. by intros; rewrite -!(commutative _ 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.
x1 x2 x1' {n} x1 x2', x1' x2' x2' {n} x2.
Proof.
intros [z Hx2] Hx1; exists (x1' z); split; auto using cmra_included_l.
by rewrite Hx1 Hx2.
......
......@@ -3,10 +3,10 @@ Require Export algebra.base.
(** Unbundeled version *)
Class Dist A := dist : nat relation A.
Instance: Params (@dist) 3.
Notation "x ={ n }= y" := (dist n x y)
(at level 70, n at next level, format "x ={ n }= y").
Hint Extern 0 (?x ={_}= ?y) => reflexivity.
Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Hint Extern 0 (?x {_} ?y) => reflexivity.
Hint Extern 0 (_ {_} _) => symmetry; assumption.
Tactic Notation "cofe_subst" ident(x) :=
repeat match goal with
......@@ -23,18 +23,18 @@ Tactic Notation "cofe_subst" :=
Record chain (A : Type) `{Dist A} := {
chain_car :> nat A;
chain_cauchy n i : n i chain_car n ={n}= chain_car i
chain_cauchy n i : n i chain_car n {n} chain_car i
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A A.
Record CofeMixin A `{Equiv A, Compl A} := {
mixin_equiv_dist x y : x y n, x ={n}= y;
mixin_equiv_dist x y : x y n, x {n} y;
mixin_dist_equivalence n : Equivalence (dist n);
mixin_dist_S n x y : x ={S n}= y x ={n}= y;
mixin_dist_0 x y : x ={0}= y;
mixin_conv_compl (c : chain A) n : compl c ={n}= c n
mixin_dist_S n x y : x {S n} y x {n} y;
mixin_dist_0 x y : x {0} y;
mixin_conv_compl (c : chain A) n : compl c {n} c n
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
contractive n : Proper (dist n ==> dist (S n)) f.
......@@ -60,19 +60,19 @@ Arguments cofe_mixin : simpl never.
Section cofe_mixin.
Context {A : cofeT}.
Implicit Types x y : A.
Lemma equiv_dist x y : x y n, x ={n}= y.
Lemma equiv_dist x y : x y n, x {n} y.
Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
Global Instance dist_equivalence n : Equivalence (@dist A _ n).
Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
Lemma dist_S n x y : x ={S n}= y x ={n}= y.
Lemma dist_S n x y : x {S n} y x {n} y.
Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
Lemma dist_0 x y : x ={0}= y.
Lemma dist_0 x y : x {0} y.
Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
Lemma conv_compl (c : chain A) n : compl c ={n}= c n.
Lemma conv_compl (c : chain A) n : compl c {n} c n.
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
Hint Extern 0 (_ ={0}= _) => apply dist_0.
Hint Extern 0 (_ {0} _) => apply dist_0.
(** General properties *)
Section cofe.
......@@ -97,7 +97,7 @@ Section cofe.
Qed.
Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
Lemma dist_le (x y : A) n n' : x ={n}= y n' n x ={n'}= y.
Lemma dist_le (x y : A) n n' : x {n} y n' n x {n'} y.
Proof. induction 2; eauto using dist_S. Qed.
Instance ne_proper {B : cofeT} (f : A B)
`{! n, Proper (dist n ==> dist n) f} : Proper (() ==> ()) f | 100.
......@@ -109,7 +109,7 @@ Section cofe.
unfold Proper, respectful; setoid_rewrite equiv_dist.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n compl c1 ={n}= compl c2.
Lemma compl_ne (c1 c2: chain A) n : c1 n {n} c2 n compl c1 {n} compl c2.
Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Lemma compl_ext (c1 c2 : chain A) : ( i, c1 i c2 i) compl c1 compl c2.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
......@@ -127,9 +127,9 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y x y.
Class Timeless {A : cofeT} (x : A) := timeless y : x {1} y x y.
Arguments timeless {_} _ {_} _ _.
Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x x y x ={S n}= y.
Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x x y x {S n} y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with (S n); auto with lia.
......@@ -154,7 +154,7 @@ Section fixpoint.
by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z ={n}= g z) fixpoint f ={n}= fixpoint g.
( z, f z {n} g z) fixpoint f {n} fixpoint g.
Proof.
intros Hfg; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
......@@ -181,7 +181,7 @@ Section cofe_mor.
Global Instance cofe_mor_proper (f : cofeMor A B) : Proper (() ==> ()) f.
Proof. apply ne_proper, cofe_mor_ne. Qed.
Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, x, f x g x.
Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, x, f x ={n}= g x.
Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, x, f x {n} g x.
Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
{| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
......@@ -230,7 +230,7 @@ Definition ccompose {A B C}
Instance: Params (@ccompose) 3.
Infix "◎" := ccompose (at level 40, left associativity).
Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
f1 ={n}= f2 g1 ={n}= g2 f1 g1 ={n}= f2 g2.
f1 {n} f2 g1 {n} g2 f1 g1 {n} f2 g2.
Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
(** unit *)
......@@ -325,7 +325,7 @@ Section later.
Context {A : cofeT}.
Instance later_equiv : Equiv (later A) := λ x y, later_car x later_car y.
Instance later_dist : Dist (later A) := λ n x y,
match n with 0 => True | S n => later_car x ={n}= later_car y end.
match n with 0 => True | S n => later_car x {n} later_car y end.
Program Definition later_chain (c : chain (later A)) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
......
......@@ -42,7 +42,7 @@ Proof.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Qed.
Lemma fg {n k} (x : A (S k)) : n k f (g x) ={n}= x.
Lemma fg {n k} (x : A (S k)) : n k f (g x) {n} x.
Proof.
intros Hnk; apply dist_le with k; auto; clear Hnk.
induction k as [|k IH]; simpl; [apply dist_0|].
......@@ -57,7 +57,7 @@ Record tower := {
g_tower k : g (tower_car (S k)) tower_car k
}.
Instance tower_equiv : Equiv tower := λ X Y, k, X k Y k.
Instance tower_dist : Dist tower := λ n X Y, k, X k ={n}= Y k.
Instance tower_dist : Dist tower := λ n X Y, k, X k {n} Y k.
Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) :=
{| chain_car i := c i k |}.
Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
......@@ -91,9 +91,9 @@ Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
match i with 0 => cid | S i => gg i g end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) x.
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Lemma f_tower {n k} (X : tower) : n k f (X k) ={n}= X (S k).
Lemma f_tower {n k} (X : tower) : n k f (X k) {n} X (S k).
Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed.
Lemma ff_tower {n} k i (X : tower) : n k ff i (X k) ={n}= X (i + k).
Lemma ff_tower {n} k i (X : tower) : n k ff i (X k) {n} X (i + k).
Proof.
intros; induction i as [|i IH]; simpl; [done|].
by rewrite IH (f_tower X); last lia.
......@@ -170,7 +170,7 @@ Proof.
* assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=.
by erewrite coerce_proper by done.
Qed.
Lemma embed_tower j n (X : T) : n j embed j (X j) ={n}= X.
Lemma embed_tower j n (X : T) : n j embed j (X j) {n} X.
Proof.
move=> Hn i; rewrite /= /embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
* rewrite -(gg_tower i (j - i) X).
......
......@@ -23,10 +23,10 @@ Inductive excl_equiv : Equiv (excl A) :=
| ExclBot_equiv : ExclBot ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist `{Dist A} : Dist (excl A) :=
| excl_dist_0 (x y : excl A) : x ={0}= y
| Excl_dist (x y : A) n : x ={n}= y Excl x ={n}= Excl y
| ExclUnit_dist n : ExclUnit ={n}= ExclUnit
| ExclBot_dist n : ExclBot ={n}= ExclBot.
| excl_dist_0 (x y : excl A) : x {0} y
| Excl_dist (x y : A) n : x {n} y Excl x {n} Excl y
| ExclUnit_dist n : ExclUnit {n} ExclUnit
| ExclBot_dist n : ExclBot {n} ExclBot.
Existing Instance excl_dist.
Global Instance Excl_ne : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
......@@ -138,7 +138,7 @@ Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
Proof. by destruct y. Qed.
Lemma excl_validN_inv_r n x y : {S n} (x Excl y) x = .
Proof. by destruct x. Qed.
Lemma Excl_includedN n x y : {n} y Excl x {n} y y ={n}= Excl x.
Lemma Excl_includedN n x y : {n} y Excl x {n} y y {n} Excl x.
Proof.
intros Hvalid; split; [destruct n as [|n]; [done|]|by intros ->].
by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
......
......@@ -6,7 +6,7 @@ Context `{Countable K} {A : cofeT}.
Implicit Types m : gmap K A.
Instance map_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i ={n}= m2 !! i.
i, m1 !! i {n} m2 !! i.
Program Definition map_chain (c : chain (gmap K A))
(k : K) : chain (option A) := {| chain_car n := c n !! k |}.
Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
......@@ -60,7 +60,7 @@ Qed.
Global Instance map_lookup_timeless m i : Timeless m Timeless (m !! i).
Proof.
intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
assert (m ={1}= <[i:=x]> m)
assert (m {1} <[i:=x]> m)
by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
Qed.
......@@ -132,7 +132,7 @@ Qed.
Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
Proof.
intros n m m1 m2 Hm Hm12.
assert ( i, m !! i ={n}= m1 !! i m2 !! i) as 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 n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
set (f_proj i := proj1_sig (f i)).
......@@ -166,7 +166,7 @@ Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types a : A.
Lemma map_lookup_validN n m i x : {n} m m !! i ={n}= Some x {n} x.
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).
Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed.
......@@ -201,7 +201,7 @@ Lemma map_op_singleton (i : K) (x y : A) :
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Lemma singleton_includedN n m i x :
{[ i x ]} {n} m y, m !! i ={n}= Some y x y.
{[ i x ]} {n} m y, m !! i {n} Some y x y.
(* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
Proof.
split.
......
......@@ -21,7 +21,7 @@ Section iprod_cofe.
Implicit Types f g : iprod B.
Instance iprod_equiv : Equiv (iprod B) := λ f g, x, f x g x.
Instance iprod_dist : Dist (iprod B) := λ n f g, x, f x ={n}= g x.
Instance iprod_dist : Dist (iprod B) := λ n f g, x, f x {n} g x.
Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
{| chain_car n := c n x |}.
Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
......
......@@ -5,9 +5,9 @@ Require Import algebra.functor.
Section cofe.
Context {A : cofeT}.
Inductive option_dist : Dist (option A) :=
| option_0_dist (x y : option A) : x ={0}= y
| Some_dist n x y : x ={n}= y Some x ={n}= Some y
| None_dist n : None ={n}= None.
| option_0_dist (x y : option A) : x {0} y
| Some_dist n x y : x {n} y Some x {n} Some y
| None_dist n : None {n} None.
Existing Instance option_dist.
Program Definition option_chain
(c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
......@@ -134,9 +134,9 @@ Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
Proof.
destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
Qed.
Lemma option_op_positive_dist_l n mx my : mx my ={n}= None mx ={n}= None.
Lemma option_op_positive_dist_l n mx my : mx my {n} None mx {n} None.
Proof. by destruct mx, my; inversion_clear 1. Qed.
Lemma option_op_positive_dist_r n mx my : mx my ={n}= None my ={n}= None.
Lemma option_op_positive_dist_r n mx my : mx my {n} None my {n} None.
Proof. by destruct mx, my; inversion_clear 1. Qed.
Lemma option_updateP (P : A Prop) (Q : option A Prop) x :
......
......@@ -5,7 +5,7 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Record uPred (M : cmraT) : Type := IProp {
uPred_holds :> nat M Prop;
uPred_ne x1 x2 n : uPred_holds n x1 x1 ={n}= x2 uPred_holds n x2;
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 {n2} x2 uPred_holds n2 x2
......@@ -54,7 +54,7 @@ Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
P1 ={n}= P2 {n} x P1 n x P2 n x.
P1 {n} P2 {n} x P1 n x P2 n x.
Proof. intros HP ?; apply HP; auto. Qed.
Lemma uPred_weaken' {M} (P : uPred M) x1 x2 n1 n2 :
x1 x2 n2 n1 {n2} x2 P n1 x1 P n2 x2.
......@@ -90,7 +90,7 @@ 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)
`{!CMRAMonotone f, !CMRAMonotone g} n :
f ={n}= g uPredC_map f ={n}= uPredC_map g.
f {n} g uPredC_map f {n} uPredC_map g.
Proof.
by intros Hfg P y n' ??;
rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
......@@ -120,7 +120,7 @@ Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
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 (x2' {n2} x2) as Hx2' by (by apply dist_le with n1).
assert ({n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
eauto using uPred_weaken, uPred_ne.
Qed.
......@@ -140,18 +140,18 @@ Next Obligation.
Qed.
Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
{| uPred_holds n x := a1 ={n}= a2 |}.
{| uPred_holds n x := a1 {n} a2 |}.
Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := x1 x2, x ={n}= x1 x2 P n x1 Q n x2 |}.
{| uPred_holds n x := x1 x2, x {n} x1 x2 P n x1 Q n x2 |}.
Next Obligation.
by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
Qed.
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 ??.
assert ( x2', y ={n2}= x1 x2' x2 x2') as (x2'&Hy&?).
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. }
clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
......
......@@ -65,7 +65,7 @@ Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *)
Lemma ownI_spec r n i P :
{n} r
(ownI i P) n r wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
(ownI i P) n r wld r !! i {n} Some (to_agree (Later (iProp_unfold P))).
Proof.
intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
* intros [(P'&Hi&HP) _]; rewrite Hi.
......@@ -73,7 +73,7 @@ Proof.
(cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
* intros ?; split_ands; try apply cmra_empty_leastN; eauto.
Qed.
Lemma ownP_spec r n σ : {n} r (ownP σ) n r pst r ={n}= Excl σ.
Lemma ownP_spec r n σ : {n} r (ownP σ) n r pst r {n} Excl σ.
Proof.
intros (?&?&?); rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
naive_solver (apply cmra_empty_leastN).
......
......@@ -24,7 +24,7 @@ Inductive res_equiv' (r1 r2 : res Λ Σ A) := Res_equiv :
wld r1 wld r2 pst r1 pst r2 gst r1 gst r2 res_equiv' r1 r2.
Instance res_equiv : Equiv (res Λ Σ A) := res_equiv'.
Inductive res_dist' (n : nat) (r1 r2 : res Λ Σ A) := Res_dist :
wld r1 ={n}= wld r2 pst r1 ={n}= pst r2 gst r1 ={n}= gst r2
wld r1 {n} wld r2 pst r1 {n} pst r2 gst r1 {n} gst r2
res_dist' n r1 r2.
Instance res_dist : Dist (res Λ Σ A) := res_dist'.
Global Instance Res_ne n :
......@@ -148,14 +148,14 @@ Proof. done. Qed.
Lemma Res_unit w σ m : unit (Res w σ m) = Res (unit w) (unit σ) (unit m).
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
{n} (r1r2) wld r1 !! i ={n}= Some P (wld r1 wld r2) !! i ={n}= Some P.
{n} (r1r2) wld r1 !! i {n} Some P (wld r1 wld r2) !! i {n} Some P.
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
by constructor; rewrite (agree_op_inv P P') // agree_idempotent.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
{n} (r1r2) wld r2 !! i ={n}= Some P (wld r1 wld r2) !! i ={n}= Some P.
{n} (r1r2) wld r2 !! i {n} Some P (wld r1 wld r2) !! i {n} Some P.
Proof.
rewrite (commutative _ r1) (commutative _ (wld r1)); apply lookup_wld_op_l.
Qed.
......
......@@ -66,7 +66,7 @@ Transparent uPred_holds.
Global Instance wp_ne E e n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ E e).
Proof.
cut ( Q1 Q2, ( v, Q1 v ={n}= Q2 v)
cut ( Q1 Q2, ( v, Q1 v {n} Q2 v)
r n', n' n {n'} r wp E e Q1 n' r wp E e Q2 n' r).
{ by intros help Q Q' HQ; split; apply help. }
intros Q1 Q2 HQ r n'; revert e r.
......
......@@ -12,7 +12,7 @@ Record wsat_pre {Λ Σ} (n : nat) (E : coPset)
wsat_pre_dom i : is_Some (rs !! i) i E is_Some (wld r !! i);
wsat_pre_wld i P :
i E
wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P)))
wld r !! i {S n} Some (to_agree (Later (iProp_unfold P)))
r', rs !! i = Some r' P n r'
}.
Arguments wsat_pre_valid {_ _ _ _ _ _ _} _.
......@@ -50,11 +50,11 @@ Proof.
intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto.
intros i P ? HiP; destruct (wld (r big_opM rs) !! i) as [P'|] eqn:HP';
[apply (injective Some) in HiP|inversion_clear HiP].
assert (P' ={S n}= to_agree $ Later $ iProp_unfold $
assert (P' {S n} to_agree $ Later $ iProp_unfold $
iProp_fold $ later_car $ P' (S n)) as HPiso.
{ rewrite iProp_unfold_fold later_eta to_agree_car //.
apply (map_lookup_validN _ (wld (r big_opM rs)) i); rewrite ?HP'; auto. }
assert (P ={n'}= iProp_fold (later_car (P' (S n)))) as HPP'.
assert (P {n'} iProp_fold (later_car (P' (S n)))) as HPP'.
{ apply (injective iProp_unfold), (injective Later), (injective to_agree).
by rewrite -HiP -(dist_le _ _ _ _ HPiso). }
destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto.
......@@ -77,7 +77,7 @@ Proof.
* intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
Qed.
Lemma wsat_open n E σ r i P :
wld r !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) i E
wld r !! i {S n} Some (to_agree (Later (iProp_unfold P))) i E
wsat (S n) ({[i]} E) σ r rP, wsat (S n) E σ (rP r) P n rP.
Proof.
intros HiP Hi [rs [Hval Hσ HE Hwld]].
......@@ -92,7 +92,7 @@ Proof.
apply Hwld; [solve_elem_of +Hj|done].
Qed.
Lemma wsat_close n E σ r i P rP :
wld rP !! i ={S n}= Some (to_agree (Later (iProp_unfold P))) i E
wld rP !! i {S n} Some (to_agree (Later (iProp_unfold P))) i E
wsat (S n) E σ (rP r) P n rP wsat (S n) ({[i]} E) σ r.
Proof.
intros HiP HiE [rs [Hval Hσ HE Hwld]] ?.
......@@ -112,7 +112,7 @@ Proof.
exists r'; rewrite lookup_insert_ne; naive_solver.
Qed.