Commit c218e1ab authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add nclose N ⊆ E → nclose (N .@ x) ⊆ E to ndisj hints.

parent fc0b90e4
...@@ -22,33 +22,38 @@ Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux. ...@@ -22,33 +22,38 @@ Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
Infix ".@" := ndot (at level 19, left associativity) : C_scope. Infix ".@" := ndot (at level 19, left associativity) : C_scope.
Notation "(.@)" := ndot (only parsing) : C_scope. Notation "(.@)" := ndot (only parsing) : C_scope.
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
Lemma nclose_nroot : nclose nroot = .
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N.
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Lemma nclose_subseteq `{Countable A} N x : nclose (N .@ x) nclose N.
Proof.
intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def 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 (N .@ x) nclose N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite (nclose N).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 nclose N2. Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 nclose N2.
Section ndisjoint. Section namespace.
Context `{Countable A}. Context `{Countable A}.
Implicit Types x y : A. Implicit Types x y : A.
Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
Lemma nclose_nroot : nclose nroot = .
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N.
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Lemma nclose_subseteq N x : nclose (N .@ x) nclose N.
Proof.
intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
{ by exists [encode x]. }
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Lemma nclose_subseteq' E N x : nclose N E nclose (N .@ x) E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N .@ x) nclose N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite (nclose N).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y. Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
Proof. Proof.
intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq. intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
...@@ -65,7 +70,7 @@ Section ndisjoint. ...@@ -65,7 +70,7 @@ Section ndisjoint.
Lemma ndisj_subseteq_difference N E F : Lemma ndisj_subseteq_difference N E F :
E nclose N E F E F nclose N. E nclose N E F E F nclose N.
Proof. set_solver. Qed. Proof. set_solver. Qed.
End ndisjoint. End namespace.
(* The hope is that registering these will suffice to solve most goals (* The hope is that registering these will suffice to solve most goals
of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *) of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *)
...@@ -73,5 +78,6 @@ Hint Resolve ndisj_subseteq_difference : ndisj. ...@@ -73,5 +78,6 @@ Hint Resolve ndisj_subseteq_difference : ndisj.
Hint Extern 0 (_ _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj. Hint Resolve ndot_preserve_disjoint_r : ndisj.
Hint Extern 1 (_ _) => apply nclose_subseteq' : ndisj.
Ltac solve_ndisj := solve [eauto with ndisj]. Ltac solve_ndisj := solve [eauto with ndisj].
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