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→.
  move ⇒ P0 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.
  move ⇒ closed_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'. move ⇒ A /setUP [/setDP []|/set1P->]; by auto. }
    have F'_pw_in : {in F' &, ∀ 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; ∃ 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.
    ∃ 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. ∃ 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.

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.
  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 /
    ∃ 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.
  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.
    ∃ 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}) :
  (∀ i, connected (T i)) → (∀ i j, T i :&: T j != set0) → ∃ z , ∀ 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 ? ? ?].
  ∃ 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. 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. ∃ x. apply/bigcapP. exact: Hx.
Qed.

End Tree.