Merge pull request #555 from chdoc/disjoint-lemmas

some lemmas for disjoint

4 files changed, 30 insertions, 7 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e5a6ade..a80641c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -135,6 +135,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `eqtype.v` new lemmas `contra_not_neq`, `contra_eq_not`.
 - in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of
   dual lattices.
+- in `finset.v` new lemma `disjoints1`
+- in `fintype.v` new lemmas: `disjointFr`, `disjointFl`, `disjointWr`, `disjointW`
 
 - in `interval.v`:
   + Intervals and their bounds of `T` now have canonical ordered type instances
@@ -190,6 +192,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `order.v`, `\join^d_` and `\meet^d_` notations are now properly specialized
   for `dual_display`.
+- in `fintype.v`, rename `disjoint_trans` to `disjointWl`
 
 - in `interval.v`:
   + `x <= y ?< if c` (`lersif`) has been generalized to `porderType`, relocated
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 6495ef6..b77d1a8 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -92,7 +92,7 @@ apply: (@equivP (exists2 x1, x1 \in a & dfs_path v1 x1 y)); last first.
   case/andP=> a_x1 g_p1 /andP[not_p1x _] /subsetP p_p1 p1y not_pv.
   exists x1 => //; exists p1 => //.
   rewrite disjoint_sym disjoint_cons not_p1x disjoint_sym.
-  by move: not_pv; rewrite disjoint_cons => /andP[_ /disjoint_trans->].
+  by move: not_pv; rewrite disjoint_cons => /andP[_ /disjointWl->].
 have{neq_yx not_vy}: y \notin v1 by apply/norP.
 have{le_v'_n not_vx}: #|T| <= #|v1| + n by rewrite cardU1 not_vx addSnnS.
 elim: {x v}a v1 => [|x a IHa] v /= le_v'_n not_vy.
@@ -104,7 +104,7 @@ apply: {IHa}(equivP (IHa _ _ not_v2y)).
   by rewrite (leq_trans le_v'_n) // leq_add2r subset_leq_card.
 split=> [] [x1 a_x1 [p g_p p_y not_pv]].
   exists x1; [exact: predU1r | exists p => //].
-  by rewrite disjoint_sym (disjoint_trans v2v) // disjoint_sym.
+  by rewrite disjoint_sym (disjointWl v2v) // disjoint_sym.
 suffices not_p1v2: [disjoint x1 :: p & v2].
   case/predU1P: a_x1 => [def_x1 | ]; last by exists x1; last exists p.
   case/pred0Pn: not_p1v2; exists x; rewrite /= def_x1 mem_head /=.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 4262ed7..7d41b12 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -940,6 +940,9 @@ Proof. by rewrite disjoints_subset -setD_eq0 setDE setCK. Qed.
 Lemma disjoint_setI0 A B : [disjoint A & B] -> A :&: B = set0.
 Proof. by rewrite -setI_eq0; move/eqP. Qed.
 
+Lemma disjoints1 A x : [disjoint [set x] & A] = (x \notin A).
+Proof. by rewrite (@eq_disjoint1 _ x) // => y; rewrite !inE. Qed.
+
 Lemma subsetD1 A B x : (A \subset B :\ x) = (A \subset B) && (x \notin A).
 Proof. by rewrite setDE subsetI subsetC sub1set inE. Qed.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index f4f34a4..dca9a48 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -461,7 +461,7 @@ Section OpsTheory.
 
 Variable T : finType.
 
-Implicit Types (A B C : {pred T}) (P Q : pred T) (x y : T) (s : seq T).
+Implicit Types (A B C D: {pred T}) (P Q : pred T) (x y : T) (s : seq T).
 
 Lemma enumP : Finite.axiom (Finite.enum T).
 Proof. by rewrite unlock; case T => ? [? []]. Qed.
@@ -848,10 +848,25 @@ Proof.
 by rewrite subset_disjoint; apply: eq_disjoint_r => x; rewrite !inE /= negbK.
 Qed.
 
-Lemma disjoint_trans A B C :
+Lemma disjointFr A B x : [disjoint A & B] -> x \in A -> x \in B = false.
+Proof. by move/pred0P/(_ x) => /=; case: (x \in A). Qed.
+
+Lemma disjointFl A B x : [disjoint A & B] -> x \in B -> x \in A = false.
+Proof. rewrite disjoint_sym; exact: disjointFr. Qed.
+
+Lemma disjointWl A B C :
    A \subset B -> [disjoint B & C] -> [disjoint A & C].
 Proof. by rewrite 2!disjoint_subset; apply: subset_trans. Qed.
 
+Lemma disjointWr A B C : A \subset B -> [disjoint C & B] -> [disjoint C & A].
+Proof. rewrite ![[disjoint C & _]]disjoint_sym. exact:disjointWl. Qed.
+
+Lemma disjointW A B C D :
+  A \subset B -> C \subset D -> [disjoint B & D] -> [disjoint A & C].
+Proof.
+by move=> subAB subCD BD; apply/(disjointWl subAB)/(disjointWr subCD).
+Qed.
+
 Lemma disjoint0 A : [disjoint pred0 & A].
 Proof. exact/pred0P. Qed.
 
@@ -888,9 +903,8 @@ Proof. exact: disjointU1. Qed.
 
 Lemma disjoint_has s A : [disjoint s & A] = ~~ has (mem A) s.
 Proof.
-rewrite -(@eq_has _ (mem (enum A))) => [|x]; last exact: mem_enum.
-rewrite has_sym has_filter -filter_predI -has_filter has_count -eqn0Ngt.
-by rewrite -size_filter /disjoint /pred0b unlock.
+apply/negbRL; apply/pred0Pn/hasP => [[x /andP[]]|[x]]; exists x => //.
+exact/andP.
 Qed.
 
 Lemma disjoint_cat s1 s2 A :
@@ -899,6 +913,9 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed.
 
 End OpsTheory.
 
+Notation disjoint_trans := 
+  (deprecate disjoint_trans disjointWl _ _ _ _) (only parsing).
+
 Hint Resolve subxx_hint : core.
 
 Arguments pred0P {T P}.