prove some things about invariants

program_logic/namespace.v

 Require Export algebra.base prelude.countable prelude.co_pset.
 Require Import program_logic.ownership.
 Require Export program_logic.pviewshifts.
+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.
@@ -34,7 +40,61 @@ Proof.
   induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
 Qed.
 
+Local Hint Resolve nclose_subseteq ndot_nclose.
+
 (** Derived forms and lemmas about them. *)
 Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
-  ownI (encode N) P.
-(* TODO: Add lemmas about inv here. *)
+  (∃ i : positive, ownI (encode $ ndot N i) P)%I.
+
+Section inv.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types i : positive.
+Implicit Types N : namespace.
+Implicit Types P Q R : iProp Λ Σ.
+
+Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
+Proof.
+  intros n ? ? EQ. apply exists_ne=>i.
+  by apply ownI_contractive.
+Qed.
+
+Global Instance inv_always_stable N P : AlwaysStable (inv N P) := _.
+
+Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
+Proof. by rewrite always_always. Qed.
+
+(* We actually pretty much lose the abolity to deal with mask-changing view
+   shifts when using `inv`. This is because we cannot exactly name the invariants
+   any more. But that's okay; all this means is that sugar like the atomic
+   triples will have to prove its own version of the open_close rule
+   by unfolding `inv`. *)
+Lemma pvs_open_close E N P Q R :
+  nclose N ⊆ E →
+  P ⊑ (inv N R ∧ (▷R -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷R ★ Q)))%I →
+  P ⊑ pvs E E Q.
+Proof.
+  move=>HN -> {P}.
+  rewrite /inv and_exist_r. apply exist_elim=>i.
+  (* Add this to the local context, so that solve_elem_of finds it. *)
+  assert ({[encode (ndot N i)]} ⊆ nclose N) by eauto.
+  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
+  rewrite {1}pvs_openI !pvs_frame_r.
+  (* TODO is there a common pattern here in the way we combine pvs_trans
+     and pvs_mask_frame_mono? *)
+  rewrite -(pvs_trans E (E ∖ {[ (encode (ndot N i)) ]}));
+    last by solve_elem_of. (* FIXME: Shouldn't eauto work, since I added a Hint Extern? *)
+  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  rewrite (commutative _ (▷R)%I) -associative wand_elim_r pvs_frame_l.
+  rewrite -(pvs_trans _ (E ∖ {[ (encode (ndot N i)) ]}) E); last by solve_elem_of.
+  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
+  apply pvs_mask_frame'; solve_elem_of.
+Qed.
+
+Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
+Proof.
+  (* FIXME: Can we have the E that contains exactly all (encode $ ndot N i) for all i?
+     If not, then we have to change the def. of inv. *)
+Abort.
+
+End inv.

program_logic/pviewshifts.v

@@ -144,6 +144,7 @@ Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q.
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
 Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.
 Proof. by rewrite (commutative _) pvs_impl_l. Qed.
+
 Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P.
 Proof.
@@ -151,13 +152,21 @@ Proof.
   - rewrite {2}HEE =>{HEE}. by rewrite -!union_difference_L.
   - solve_elem_of.
 Qed. 
+
+Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
+  E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
+  P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q.
+Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
+
 Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
 Proof.
   intros. apply pvs_mask_frame'; solve_elem_of.
 Qed.
+
 Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
 Proof.
   intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
+
 End pvs.