introduce a notion of disjoint namespaces, and prove a few lemmas about it

program_logic/invariants.v

@@ -30,16 +30,42 @@ Proof.
 Qed.
 Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N.
 Proof. apply nclose_subseteq with x, encode_nclose. Qed.
-Lemma nclose_disjoint `{Countable A} N (x y : A) :
-  x ≠ y → nclose (ndot N x) ∩ nclose (ndot N y) = ∅.
+
+Definition ndisj (N1 N2 : namespace) :=
+  ∃ N1' N2', N1' `suffix_of` N1 ∧ N2' `suffix_of` N2 ∧
+             length N1' = length N2' ∧ N1' ≠ N2'.
+
+Global Instance ndisj_comm : Comm iff ndisj.
+Proof. intros N1 N2. rewrite /ndisj; naive_solver. Qed.
+
+Lemma ndot_ne_disj `{Countable A} N (x y : A) :
+  x ≠ y → ndisj (ndot N x) (ndot N y).
+Proof.
+  intros Hxy. exists (ndot N x), (ndot N y). split_ands; try done; [].
+  by apply not_inj2_2.
+Qed.
+
+Lemma ndot_preserve_disj_l `{Countable A} N1 N2 (x : A) :
+  ndisj N1 N2 → ndisj (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_disj_r `{Countable A} N1 N2 (x : A) :
+  ndisj N1 N2 → ndisj N1 (ndot N2 x).
+Proof.
+  rewrite ![ndisj N1 _]comm. apply ndot_preserve_disj_l.
+Qed.
+
+Lemma ndisj_disjoint N1 N2 :
+  ndisj N1 N2 → nclose N1 ∩ nclose N2 = ∅.
 Proof.
-  intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot.
+  intros (N1' & N2' & [N1'' Hpr1] & [N2'' Hpr2] & Hl & Hne). subst N1 N2.
+  apply elem_of_equiv_empty_L=> p; unfold nclose.
   rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
-  apply Hxy, (inj encode), (inj encode_nat); revert Hq.
-  rewrite !(list_encode_cons (encode _)).
-  rewrite !(assoc_L _) (inj_iff (++ _)%positive) /=.
-  generalize (encode_nat (encode y)).
-  induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
+  rewrite !list_encode_app !assoc in Hq.
+  apply Hne. eapply list_encode_suffix_eq; done.
 Qed.
 
 Local Hint Resolve nclose_subseteq ndot_nclose.