From 5f13409c43880035de356d0f4d99dd247fd6809c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 14 Dec 2015 11:04:10 +0100
Subject: [PATCH] Some more namespace lemmas.

---
 iris/namespace.v | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/iris/namespace.v b/iris/namespace.v
index 768518a0c..daf9b7d99 100644
--- a/iris/namespace.v
+++ b/iris/namespace.v
@@ -8,15 +8,19 @@ Definition nclose (I : namespace) : coPset := coPset_suffixes (encode I).
 
 Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros I1 x1 I2 x2 ?; simplify_equality. Qed.
-Definition nclose_nnil : nclose nnil = coPset_all.
+Lemma nclose_nnil : nclose nnil = coPset_all.
 Proof. by apply (sig_eq_pi _). Qed.
-Definition nclose_subseteq `{Countable A} I x : nclose (ndot I x) ⊆ nclose I.
+Lemma encode_nclose I : encode I ∈ nclose I.
+Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
+Lemma nclose_subseteq `{Countable A} I x : nclose (ndot I x) ⊆ nclose I.
 Proof.
   intros p; unfold nclose; rewrite !elem_coPset_suffixes; intros [q ->].
   destruct (list_encode_suffix I (ndot I x)) as [q' ?]; [by exists [encode x]|].
   by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
 Qed.
-Definition nclose_disjoint `{Countable A} I (x y : A) :
+Lemma ndot_nclose `{Countable A} I x : encode (ndot I x) ∈ nclose I.
+Proof. apply nclose_subseteq with x, encode_nclose. Qed.
+Lemma nclose_disjoint `{Countable A} I (x y : A) :
   x ≠ y → nclose (ndot I x) ∩ nclose (ndot I y) = ∅.
 Proof.
   intros Hxy; apply elem_of_equiv_empty_L; intros p; unfold nclose, ndot.
-- 
GitLab