Commit 5f13409c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Some more namespace lemmas.

parent 6e9a9572
......@@ -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.
......
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