From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries digraph sgraph set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import edone preliminaries digraph sgraph set_tac.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Preliminaries
Lemma ltn_subn n m o : n < m -> n - o < m.
Proof. apply: leq_ltn_trans. exact: leq_subr. Qed.
Lemma ord3P (P : 'I_3 -> Type) : P ord0 -> P ord1 -> P ord2 -> forall i : 'I_3, P i.
Proof.
have H (i j : 'I_3) : i == j -> P i -> P j by move/eqP->.
move => P0 P1 P2 [[|[|[|//]]] Hi].
exact: H P0. exact: H P1. exact: H P2.
Qed.
(* Notation "A ∩ B" := (A :&: B) (at level 30). *)
We first show that for intersection closed properties, the helly
property of families of size three extends to the families of
arbitrary (finite) cardinalities.
TOTHINK: This should extend also to T:choiceType using the finmap library
Lemma helly3_lifting (T : finType) (P : {set T} -> Prop) :
(forall A B, P A -> P B -> P (A :&: B)) ->
(forall f : 'I_3 -> {set T},
(forall i, P (f i)) -> (forall i j, f i :&: f j != set0) -> exists x, forall i, x \in f i) ->
forall F : {set {set T}},
0 < #|F| -> (forall A, A \in F -> P A) -> {in F &, forall A B, A :&: B != set0} -> exists x, forall A, A \in F -> x \in A.
Proof.
move => closed_P helly3_P.
apply: (nat_size_ind (f := (fun A : {set {set T}}=> #|A|))).
move => /= F IH inh_F F_sub_P F_pw_in.
case: (ltnP 1 #|F|) => card_F.
- case/card_gt1P : card_F => /= X [Y] [XF YF XY].
move def_F' : ((F :\: [set X;Y]) :|: [set X :&: Y]) => F'.
have F'_in_U : (forall A, A \in F' -> P A).
{ rewrite -def_F'. move => A /setUP [/setDP []|/set1P->]; by auto. }
have F'_pw_in : {in F' &, forall A B : {set T}, A :&: B != set0}.
{ move => A B. rewrite -def_F' !in_setU !in_set1 => HA HB.
wlog [HA HB]: A B {HA HB} / A = X :&: Y /\ B \in F.
{ move => W.
case/orP : HA => [/setDP [HA _]|/eqP HA]; case/orP : HB => [/setDP [HB _]|/eqP HB].
- exact: F_pw_in.
- rewrite setIC. by apply: W.
- exact: W.
- rewrite HA HB setIid. exact: F_pw_in. }
rewrite HA.
pose f := tnth [tuple X; Y; B].
case: (helly3_P f _ _).
- apply: ord3P; by rewrite /f /tnth /=; apply: F_sub_P.
- do 2 apply: ord3P; by rewrite /f /tnth /=; apply: F_pw_in.
- move => x Hx. apply/set0Pn; exists x. rewrite !inE.
move: (Hx ord0) (Hx ord1) (Hx ord2). by rewrite /f /tnth /= => -> -> ->. }
have card_F' : #|F'| < #|F|.
{ (* set reasoning with cardinalities *)
rewrite -def_F' cardsU cards1. apply: ltn_subn.
rewrite -setDDl [#|F|](cardsD1 X) [#|F :\ X|](cardsD1 Y).
rewrite !inE XF YF eq_sym XY /= add1n addnC. exact: leqnn. }
have inh_F' : 0 < #|F'|.
{ apply/card_gt0P. exists (X :&: Y). by rewrite -def_F' !inE eqxx. }
case: (IH F' _ _ _ _) => // x Hx.
exists x => A A_in_F. case: (boolP ((A == X) || (A == Y))) => H.
+ case : (setIP (Hx (X :&: Y) _)).
* by rewrite -def_F' !inE eqxx.
* by case/orP: H => /eqP ->.
+ apply: Hx. by rewrite -def_F' !inE H A_in_F.
- have/card1P [A HA] : #|F| == 1 by rewrite eqn_leq card_F.
move: (F_pw_in A A). rewrite !HA inE eqxx. case/(_ _ _)/Wrap => //.
case/set0Pn => x. rewrite setIid => Hx. exists x => B.
by rewrite HA inE => /eqP->.
Qed.
Section Tree.
Variable (G : sgraph).
Hypothesis tree_G : is_forest [set: G].
(forall A B, P A -> P B -> P (A :&: B)) ->
(forall f : 'I_3 -> {set T},
(forall i, P (f i)) -> (forall i j, f i :&: f j != set0) -> exists x, forall i, x \in f i) ->
forall F : {set {set T}},
0 < #|F| -> (forall A, A \in F -> P A) -> {in F &, forall A B, A :&: B != set0} -> exists x, forall A, A \in F -> x \in A.
Proof.
move => closed_P helly3_P.
apply: (nat_size_ind (f := (fun A : {set {set T}}=> #|A|))).
move => /= F IH inh_F F_sub_P F_pw_in.
case: (ltnP 1 #|F|) => card_F.
- case/card_gt1P : card_F => /= X [Y] [XF YF XY].
move def_F' : ((F :\: [set X;Y]) :|: [set X :&: Y]) => F'.
have F'_in_U : (forall A, A \in F' -> P A).
{ rewrite -def_F'. move => A /setUP [/setDP []|/set1P->]; by auto. }
have F'_pw_in : {in F' &, forall A B : {set T}, A :&: B != set0}.
{ move => A B. rewrite -def_F' !in_setU !in_set1 => HA HB.
wlog [HA HB]: A B {HA HB} / A = X :&: Y /\ B \in F.
{ move => W.
case/orP : HA => [/setDP [HA _]|/eqP HA]; case/orP : HB => [/setDP [HB _]|/eqP HB].
- exact: F_pw_in.
- rewrite setIC. by apply: W.
- exact: W.
- rewrite HA HB setIid. exact: F_pw_in. }
rewrite HA.
pose f := tnth [tuple X; Y; B].
case: (helly3_P f _ _).
- apply: ord3P; by rewrite /f /tnth /=; apply: F_sub_P.
- do 2 apply: ord3P; by rewrite /f /tnth /=; apply: F_pw_in.
- move => x Hx. apply/set0Pn; exists x. rewrite !inE.
move: (Hx ord0) (Hx ord1) (Hx ord2). by rewrite /f /tnth /= => -> -> ->. }
have card_F' : #|F'| < #|F|.
{ (* set reasoning with cardinalities *)
rewrite -def_F' cardsU cards1. apply: ltn_subn.
rewrite -setDDl [#|F|](cardsD1 X) [#|F :\ X|](cardsD1 Y).
rewrite !inE XF YF eq_sym XY /= add1n addnC. exact: leqnn. }
have inh_F' : 0 < #|F'|.
{ apply/card_gt0P. exists (X :&: Y). by rewrite -def_F' !inE eqxx. }
case: (IH F' _ _ _ _) => // x Hx.
exists x => A A_in_F. case: (boolP ((A == X) || (A == Y))) => H.
+ case : (setIP (Hx (X :&: Y) _)).
* by rewrite -def_F' !inE eqxx.
* by case/orP: H => /eqP ->.
+ apply: Hx. by rewrite -def_F' !inE H A_in_F.
- have/card1P [A HA] : #|F| == 1 by rewrite eqn_leq card_F.
move: (F_pw_in A A). rewrite !HA inE eqxx. case/(_ _ _)/Wrap => //.
case/set0Pn => x. rewrite setIid => Hx. exists x => B.
by rewrite HA inE => /eqP->.
Qed.
Section Tree.
Variable (G : sgraph).
Hypothesis tree_G : is_forest [set: G].
If the whole graph is a forest, every connected set of vertices is a subtree
Subtrees are closed under intersection
Lemma tree_connectI (T1 T2 : {set G}) :
connected T1 -> connected T2 -> connected (T1 :&: T2).
Proof.
move => C1 C2 x y /setIP [X1 X2] /setIP [Y1 Y2].
case: (path_in_connected C1 X1 Y1) => p Ip /subsetP Sp.
case: (path_in_connected C2 X2 Y2) => q Iq /subsetP Sq.
have {Iq Ip} ? : p = q by apply: tree_G.
subst q. apply connectRI with p => z zp. by rewrite !inE Sp ?Sq.
Qed.
connected T1 -> connected T2 -> connected (T1 :&: T2).
Proof.
move => C1 C2 x y /setIP [X1 X2] /setIP [Y1 Y2].
case: (path_in_connected C1 X1 Y1) => p Ip /subsetP Sp.
case: (path_in_connected C2 X2 Y2) => q Iq /subsetP Sq.
have {Iq Ip} ? : p = q by apply: tree_G.
subst q. apply connectRI with p => z zp. by rewrite !inE Sp ?Sq.
Qed.
Lemma subtree_cut (T1 T2 : {set G}) (x1 x2 : G) (p : Path x1 x2) :
connected T1 -> connected T2 -> T1 :&: T2 != set0 -> x1 \in T1 -> x2 \in T2 ->
irred p -> exists y, [/\ y \in p, y \in T1 & y \in T2].
Proof.
move => tree_T1 tree_T2 cap_T12 X11 X22 Ip.
case/set0Pn : cap_T12 => z /setIP [Z1 Z2].
move: p Ip. move def_A : (T1 :&: T2) => A.
have zA : z \in A by rewrite -def_A inE Z1.
gen have H,Hp1 : T1 T2 x1 x2 tree_T1 tree_T2 X11 X22 Z1 Z2 def_A zA /
exists z1 (p1 : Path x1 z1), [/\ z1 \in A, irred p1, p1 \subset T1 & forall k, k \in A -> k \in p1 -> k = z1].
{ case: (@path_in_connected _ T1 x1 z) => // p1 Ip1 subT1.
case: (split_at_first zA (path_end p1)) => z1 [p11] [p12] [E H1 H2]. subst.
exists z1. exists p11. split => //.
+ by case/irred_catE : Ip1.
+ apply: subset_trans subT1. exact: subset_pcatL. }
move: Hp1 => [z1] [p1] [zA1 Ip1 /subsetP sub_p1 H1].
case: (H T2 T1 x2 x1) => // {H}; first by rewrite setIC.
move => z2 [p2] [zA2 Ip2 /subsetP sub_p2 H2].
case: (path_in_connected _ zA1 zA2) => [|q Iq /subsetP qA].
{ rewrite -def_A. exact: tree_connectI. }
set r := pcat (pcat p1 q) (prev p2).
suff I: irred r.
{ move => p Ip.
have -> : p = r by apply: forestT_unique.
exists z1. rewrite !inE /= -def_A in zA1 *. by case/setIP : zA1 => -> -> . }
rewrite /r.
apply: irred_catI.
- move => k. rewrite !inE. case/orP => U V.
+ rewrite [k]H2 //. by rewrite -def_A inE sub_p1 ?sub_p2.
+ by rewrite [k]H2 // qA.
- apply: irred_catI => // k ? /qA ?. exact: H1.
- by rewrite irred_rev.
Qed.
Lemma tree_I3 (T : 'I_3 -> {set G}) :
(forall i, connected (T i)) -> (forall i j, T i :&: T j != set0) -> exists z, forall i, z \in T i.
Proof.
move => tree_T T_pw_in.
case/set0Pn : (T_pw_in ord0 ord1) => x /setIP [X0 X1].
case/set0Pn : (T_pw_in ord0 ord2) => y /setIP [Y0 Y1].
case: (path_in_connected _ X0 Y0) => [|p irr_p /subsetP sub_T0]; first exact: tree_T.
case: (@subtree_cut (T ord1) (T ord2) x y p) => // z [/sub_T0 ? ? ?].
exists z. exact: ord3P.
Qed.
Theorem tree_helly (F : {set {set G}}) :
(forall T : {set G}, T \in F -> connected T) -> F != set0 ->
{in F &, forall A B, A :&: B != set0} -> \bigcap_(A in F) A != set0.
Proof.
rewrite -card_gt0. move => F_subtree F_inh F_pq_in.
case: (@helly3_lifting G (@connected G) _ _ F _ _ _) => //.
- exact: tree_connectI.
- exact: tree_I3.
- move => x Hx. apply/set0Pn. exists x. apply/bigcapP. exact: Hx.
Qed.
End Tree.
connected T1 -> connected T2 -> T1 :&: T2 != set0 -> x1 \in T1 -> x2 \in T2 ->
irred p -> exists y, [/\ y \in p, y \in T1 & y \in T2].
Proof.
move => tree_T1 tree_T2 cap_T12 X11 X22 Ip.
case/set0Pn : cap_T12 => z /setIP [Z1 Z2].
move: p Ip. move def_A : (T1 :&: T2) => A.
have zA : z \in A by rewrite -def_A inE Z1.
gen have H,Hp1 : T1 T2 x1 x2 tree_T1 tree_T2 X11 X22 Z1 Z2 def_A zA /
exists z1 (p1 : Path x1 z1), [/\ z1 \in A, irred p1, p1 \subset T1 & forall k, k \in A -> k \in p1 -> k = z1].
{ case: (@path_in_connected _ T1 x1 z) => // p1 Ip1 subT1.
case: (split_at_first zA (path_end p1)) => z1 [p11] [p12] [E H1 H2]. subst.
exists z1. exists p11. split => //.
+ by case/irred_catE : Ip1.
+ apply: subset_trans subT1. exact: subset_pcatL. }
move: Hp1 => [z1] [p1] [zA1 Ip1 /subsetP sub_p1 H1].
case: (H T2 T1 x2 x1) => // {H}; first by rewrite setIC.
move => z2 [p2] [zA2 Ip2 /subsetP sub_p2 H2].
case: (path_in_connected _ zA1 zA2) => [|q Iq /subsetP qA].
{ rewrite -def_A. exact: tree_connectI. }
set r := pcat (pcat p1 q) (prev p2).
suff I: irred r.
{ move => p Ip.
have -> : p = r by apply: forestT_unique.
exists z1. rewrite !inE /= -def_A in zA1 *. by case/setIP : zA1 => -> -> . }
rewrite /r.
apply: irred_catI.
- move => k. rewrite !inE. case/orP => U V.
+ rewrite [k]H2 //. by rewrite -def_A inE sub_p1 ?sub_p2.
+ by rewrite [k]H2 // qA.
- apply: irred_catI => // k ? /qA ?. exact: H1.
- by rewrite irred_rev.
Qed.
Lemma tree_I3 (T : 'I_3 -> {set G}) :
(forall i, connected (T i)) -> (forall i j, T i :&: T j != set0) -> exists z, forall i, z \in T i.
Proof.
move => tree_T T_pw_in.
case/set0Pn : (T_pw_in ord0 ord1) => x /setIP [X0 X1].
case/set0Pn : (T_pw_in ord0 ord2) => y /setIP [Y0 Y1].
case: (path_in_connected _ X0 Y0) => [|p irr_p /subsetP sub_T0]; first exact: tree_T.
case: (@subtree_cut (T ord1) (T ord2) x y p) => // z [/sub_T0 ? ? ?].
exists z. exact: ord3P.
Qed.
Theorem tree_helly (F : {set {set G}}) :
(forall T : {set G}, T \in F -> connected T) -> F != set0 ->
{in F &, forall A B, A :&: B != set0} -> \bigcap_(A in F) A != set0.
Proof.
rewrite -card_gt0. move => F_subtree F_inh F_pq_in.
case: (@helly3_lifting G (@connected G) _ _ F _ _ _) => //.
- exact: tree_connectI.
- exact: tree_I3.
- move => x Hx. apply/set0Pn. exists x. apply/bigcapP. exact: Hx.
Qed.
End Tree.