Commit 1c4b9888 authored by Ralf Jung's avatar Ralf Jung

add notation for ndot

parent 95c486ef
Pipeline #71 passed with stage
......@@ -38,7 +38,7 @@ Section ClosedProofs.
{ (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
move=>? _. exact I. }
apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
rewrite -(client_safe (ndot nroot "Heap" ) (ndot nroot "Barrier" )) //.
rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
(* This, too, should be automated. *)
apply ndot_ne_disjoint. discriminate.
Qed.
......
......@@ -7,19 +7,22 @@ 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 : C_scope.
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
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 (ndot 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 (ndot 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 (ndot 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,
......@@ -33,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 ndot N x ndot N y.
Proof. intros Hxy. exists (ndot N x), (ndot 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 ndot 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 ndot 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