Commit 87b4a225 authored by Ralf Jung's avatar Ralf Jung

new notation for ndot, to avoid conflict with autosubst

parent 04d0796d
......@@ -29,11 +29,11 @@ Section ClosedProofs.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
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 "⊆ ⊤"?!? *)
by move=>? _. }
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. *)
by apply ndot_ne_disjoint.
Qed.
......
......@@ -7,8 +7,8 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Infix ".:" := ndot (at level 19, left associativity) : C_scope.
Notation "(.:)" := ndot (only parsing) : C_scope.
Infix "..:" := ndot (at level 19, left associativity) : C_scope.
Notation "(..:)" := ndot (only parsing) : C_scope.
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
......@@ -16,13 +16,13 @@ Lemma nclose_nroot : nclose nroot = ⊤.
Proof. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N.
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.
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.
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.
Instance ndisjoint : Disjoint namespace := λ N1 N2,
......@@ -36,16 +36,16 @@ Section ndisjoint.
Global Instance ndisjoint_comm : Comm iff ndisjoint.
Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
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.
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.
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.
intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
split_and?; try done; []. by apply suffix_of_cons_r.
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.
Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2 = .
......
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