# Library GraphTheory.helly

From mathcomp Require Import all_ssreflect.
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 i : 'I_3, P i.
Proof.
have H (i j : 'I_3) : i == j P i P j by move/eqP→.
moveP0 P1 P2 [[|[|[|//]]] Hi].
exact: H P0. exact: H P1. exact: H P2.
Qed.

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) :
( A B, P A P B P (A :&: B))
( f : 'I_3 {set T},
( i, P (f i)) ( i j, f i :&: f j != set0) x, i, x \in f i)
F : {set {set T}},
0 < #|F| ( A, A \in F P A) {in F &, A B, A :&: B != set0} x, A, A \in F x \in A.
Proof.
moveclosed_P helly3_P.
elim/card_ind ⇒ /= 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 : ( A, A \in F' P A).
{ rewrite -def_F'. moveA /setUP [/setDP []|/set1P->]; by auto. }
have F'_pw_in : {in F' &, A B : {set T}, A :&: B != set0}.
{ moveA B. rewrite -def_F' !in_setU !in_set1HA HB.
wlog [HA HB]: A B {HA HB} / A = X :&: Y B \in F.
{ moveW.
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.
- movex Hx. apply/set0Pn; x. rewrite !inE.
move: (Hx ord0) (Hx ord1) (Hx ord2). by rewrite /f /tnth /= ⇒ → → →. }
have card_F' : #|F'| < #|F|.
{
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. (X :&: Y). by rewrite -def_F' !inE eqxx. }
case: (IH F' _ _ _ _) ⇒ // x Hx.
xA 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/set0Pnx. rewrite setIidHx. xB.
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.
moveC1 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 pz zp. by rewrite !inE Sp ?Sq.
Qed.

NOTE: The irred p assumption could be removed, but it doesn't hurt
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 y, [/\ y \in p, y \in T1 & y \in T2].
Proof.
movetree_T1 tree_T2 cap_T12 X11 X22 Ip.
case/set0Pn : cap_T12z /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 /
z1 (p1 : Path x1 z1), [/\ z1 \in A, irred p1, p1 \subset T1 & 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.
z1. 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.
movez2 [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.
{ movep Ip.
have → : p = r by apply: forestT_unique.
z1. rewrite !inE /= -def_A in zA1 ×. by case/setIP : zA1 ⇒ → → . }
rewrite /r.
apply: irred_catI.
- movek. rewrite !inE. case/orPU 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}) :
( i, connected (T i)) ( i j, T i :&: T j != set0) z, i, z \in T i.
Proof.
movetree_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 ? ? ?].
z. exact: ord3P.
Qed.

Theorem tree_helly (F : {set {set G}}) :
( T : {set G}, T \in F connected T) F != set0
{in F &, A B, A :&: B != set0} \bigcap_(A in F) A != set0.
Proof.
rewrite -card_gt0. moveF_subtree F_inh F_pq_in.
case: (@helly3_lifting G (@connected G) _ _ F _ _ _) ⇒ //.
- exact: tree_connectI.
- exact: tree_I3.
- movex Hx. apply/set0Pn. x. apply/bigcapP. exact: Hx.
Qed.

End Tree.