Commit d1b91fbe authored by Ralf Jung's avatar Ralf Jung
Browse files

move some general set lemmas to sets.v; organize ndisj hints a bit

parent 7c3203e7
...@@ -67,13 +67,6 @@ Section namespace. ...@@ -67,13 +67,6 @@ Section namespace.
Lemma ndot_preserve_disjoint_r N E x : E ## N E ## N.@x. Lemma ndot_preserve_disjoint_r N E x : E ## N E ## N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed. Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma namespace_subseteq_difference E1 E2 E3 :
E1 ## E3 E1 E2 E1 E2 E3.
Proof. set_solver. Qed.
Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 E3 E1 E2 E3.
Proof. set_solver. Qed.
Lemma ndisj_difference_l E N1 N2 : N2 (N1 : coPset) E N1 ## N2. Lemma ndisj_difference_l E N1 N2 : N2 (N1 : coPset) E N1 ## N2.
Proof. set_solver. Qed. Proof. set_solver. Qed.
End namespace. End namespace.
...@@ -84,14 +77,16 @@ of the forms: ...@@ -84,14 +77,16 @@ of the forms:
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn] - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *) - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj. Create HintDb ndisj.
Hint Resolve namespace_subseteq_difference : ndisj. (* Rules for goals of the form [_ ⊆ _] *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj. Hint Resolve nclose_subseteq' : ndisj.
Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
(* Fall-back rules that lose information (but let other rules above apply). *) Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj. (* Rules for goals of the form [_ ## _] *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
Hint Resolve ndisj_difference_l : ndisj.
Hint Resolve (disjoint_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj. Hint Resolve (disjoint_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Ltac solve_ndisj := Ltac solve_ndisj :=
......
...@@ -653,6 +653,12 @@ Section set. ...@@ -653,6 +653,12 @@ Section set.
Lemma difference_mono_r X1 X2 Y : X1 X2 X1 Y X2 Y. Lemma difference_mono_r X1 X2 Y : X1 X2 X1 Y X2 Y.
Proof. set_solver. Qed. Proof. set_solver. Qed.
Lemma subseteq_difference_r X Y1 Y2 :
X ## Y2 X Y1 X Y1 Y2.
Proof. set_solver. Qed.
Lemma subseteq_difference_l X1 X2 Y : X1 Y X1 X2 Y.
Proof. set_solver. Qed.
(** Disjointness *) (** Disjointness *)
Lemma disjoint_intersection X Y : X ## Y X Y . Lemma disjoint_intersection X Y : X ## Y X Y .
Proof. set_solver. Qed. Proof. set_solver. Qed.
......
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