Commit 75a2c511 authored by Ralf Jung's avatar Ralf Jung
Browse files

change ndot notation, again

parent 83767d70
...@@ -29,11 +29,11 @@ Section ClosedProofs. ...@@ -29,11 +29,11 @@ Section ClosedProofs.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}. Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
Proof. Proof.
apply ht_alt. rewrite (heap_alloc (nroot ..: "Barrier")); last first. apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last first.
{ (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *) { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
by move=>? _. } by move=>? _. }
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l. apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -(client_safe (nroot ..: "Heap" ) (nroot ..: "Barrier" )) //. rewrite -(client_safe (nroot .@ "Heap" ) (nroot .@ "Barrier" )) //.
(* This, too, should be automated. *) (* This, too, should be automated. *)
by apply ndot_ne_disjoint. by apply ndot_ne_disjoint.
Qed. Qed.
......
...@@ -23,7 +23,7 @@ Class inG (Λ : language) (Σ : iFunctorG) (A : cmraT) := InG { ...@@ -23,7 +23,7 @@ Class inG (Λ : language) (Σ : iFunctorG) (A : cmraT) := InG {
Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) := Definition to_globalF `{inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}. iprod_singleton inG_id {[ γ := cmra_transport inG_prf a ]}.
Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iProp Λ (globalF Σ) := Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
ownG (to_globalF γ a). ownG (to_globalF γ a).
Instance: Params (@to_globalF) 5. Instance: Params (@to_globalF) 5.
Instance: Params (@own) 5. Instance: Params (@own) 5.
......
...@@ -7,8 +7,8 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := ...@@ -7,8 +7,8 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N. encode x :: N.
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Infix "..:" := ndot (at level 19, left associativity) : C_scope. Infix ".@" := ndot (at level 19, left associativity) : C_scope.
Notation "(..:)" := ndot (only parsing) : C_scope. Notation "(.@)" := ndot (only parsing) : C_scope.
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _). Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed. Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
...@@ -16,13 +16,13 @@ Lemma nclose_nroot : nclose nroot = ⊤. ...@@ -16,13 +16,13 @@ Lemma nclose_nroot : nclose nroot = ⊤.
Proof. by apply (sig_eq_pi _). Qed. Proof. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N. Lemma encode_nclose N : encode N nclose N.
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
Lemma nclose_subseteq `{Countable A} N x : nclose (N ..: x) nclose N. Lemma nclose_subseteq `{Countable A} N x : nclose (N .@ x) nclose N.
Proof. Proof.
intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
destruct (list_encode_suffix N (N ..: x)) as [q' ?]; [by exists [encode x]|]. destruct (list_encode_suffix N (N .@ x)) as [q' ?]; [by exists [encode x]|].
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal. by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed. Qed.
Lemma ndot_nclose `{Countable A} N x : encode (N ..: x) nclose N. Lemma ndot_nclose `{Countable A} N x : encode (N .@ x) nclose N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed. Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Instance ndisjoint : Disjoint namespace := λ N1 N2, Instance ndisjoint : Disjoint namespace := λ N1 N2,
...@@ -36,16 +36,16 @@ Section ndisjoint. ...@@ -36,16 +36,16 @@ Section ndisjoint.
Global Instance ndisjoint_comm : Comm iff ndisjoint. Global Instance ndisjoint_comm : Comm iff ndisjoint.
Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed. Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
Lemma ndot_ne_disjoint N (x y : A) : x y N ..: x N ..: y. Lemma ndot_ne_disjoint N (x y : A) : x y N .@ x N .@ y.
Proof. intros Hxy. exists (N ..: x), (N ..: y); naive_solver. Qed. Proof. intros Hxy. exists (N .@ x), (N .@ y); naive_solver. Qed.
Lemma ndot_preserve_disjoint_l N1 N2 x : N1 N2 N1 ..: x N2. Lemma ndot_preserve_disjoint_l N1 N2 x : N1 N2 N1 .@ x N2.
Proof. Proof.
intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'. intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
split_and?; try done; []. by apply suffix_of_cons_r. split_and?; try done; []. by apply suffix_of_cons_r.
Qed. Qed.
Lemma ndot_preserve_disjoint_r N1 N2 x : N1 N2 N1 N2 ..: x . Lemma ndot_preserve_disjoint_r N1 N2 x : N1 N2 N1 N2 .@ x .
Proof. rewrite ![N1 _]comm. apply ndot_preserve_disjoint_l. Qed. Proof. rewrite ![N1 _]comm. apply ndot_preserve_disjoint_l. Qed.
Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2 = . Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2 = .
......
Supports Markdown
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