Commit 2392dc03 authored by Robbert Krebbers's avatar Robbert Krebbers

Move namespace stuff to separate file.

Now that there is more of it, it deserves its own place :).
parent 3034d8ef
......@@ -70,6 +70,7 @@ program_logic/ghost_ownership.v
program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
heap_lang/heap_lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......
From algebra Require Export base.
From prelude Require Export countable co_pset.
From program_logic Require Import ownership.
From program_logic Require Export pviewshifts weakestpre.
From program_logic Require Export namespaces pviewshifts weakestpre.
Import uPred.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_ _) => solve_elem_of.
Local Hint Extern 99 ({[ _ ]} _) => apply elem_of_subseteq_singleton.
Definition namespace := list positive.
Definition nnil : namespace := nil.
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Lemma nclose_nnil : nclose nnil = coPset_all.
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.
Proof.
intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
destruct (list_encode_suffix N (ndot 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.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Instance ndisjoint : Disjoint namespace := λ N1 N2,
N1' N2', N1' `suffix_of` N1 N2' `suffix_of` N2
length N1' = length N2' N1' N2'.
Section ndisjoint.
Context `{Countable A}.
Implicit Types x y : A.
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_preserve_disjoint_l N1 N2 x : N1 N2 ndot N1 x N2.
Proof.
intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
split_ands; try done; []. by apply suffix_of_cons_r.
Qed.
Lemma ndot_preserve_disjoint_r N1 N2 x : N1 N2 N1 ndot N2 x .
Proof. rewrite ![N1 _]comm. apply ndot_preserve_disjoint_l. Qed.
Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2 = .
Proof.
intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne).
apply elem_of_equiv_empty_L=> p; unfold nclose.
rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
rewrite !list_encode_app !assoc in Hq.
by eapply Hne, list_encode_suffix_eq.
Qed.
End ndisjoint.
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
( i, (i nclose N) ownI i P)%I.
......
From prelude Require Export countable co_pset.
From algebra Require Export base.
Definition namespace := list positive.
Definition nnil : namespace := nil.
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Lemma nclose_nnil : nclose nnil = coPset_all.
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.
Proof.
intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
destruct (list_encode_suffix N (ndot 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.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Instance ndisjoint : Disjoint namespace := λ N1 N2,
N1' N2', N1' `suffix_of` N1 N2' `suffix_of` N2
length N1' = length N2' N1' N2'.
Section ndisjoint.
Context `{Countable A}.
Implicit Types x y : A.
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_preserve_disjoint_l N1 N2 x : N1 N2 ndot N1 x N2.
Proof.
intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
split_ands; try done; []. by apply suffix_of_cons_r.
Qed.
Lemma ndot_preserve_disjoint_r N1 N2 x : N1 N2 N1 ndot N2 x .
Proof. rewrite ![N1 _]comm. apply ndot_preserve_disjoint_l. Qed.
Lemma ndisj_disjoint N1 N2 : N1 N2 nclose N1 nclose N2 = .
Proof.
intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne).
apply elem_of_equiv_empty_L=> p; unfold nclose.
rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
rewrite !list_encode_app !assoc in Hq.
by eapply Hne, list_encode_suffix_eq.
Qed.
End ndisjoint.
\ No newline at end of file
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