Require Import RelationClasses Setoid.
From mathcomp Require Import all_ssreflect.
Require Import edone set_tac finite_quotient preliminaries digraph sgraph treewidth minor equiv.
Require Import setoid_bigop structures mgraph pttdom ptt mgraph2 skeleton.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

Section Subalgebra.
Variable (Lv : comMonoid) (Le : elabelType).
Notation graph := (graph Lv Le).
Notation graph2 := (graph2 Lv Le).

Implicit Types (G H : graph) (U : sgraph) (T : forest).

Open Scope implicit_scope.

Arguments sdecomp T G B : clear implicits.

Definition compatible (T : forest) (G : graph2) (B : T → {set G}) :=
  ∃ t, (input \in B t) && (output \in B t).

Lemma sdecomp_sskel (T : forest) (G : graph2) (B : T → {set G}) :
  sdecomp T (sskeleton G) B ↔ (sdecomp T G B ∧ compatible B).
Proof.
  split.
  - case ⇒ [D1 D2 D3]. split. split ⇒ //.
    + move ⇒ x y /= xy. apply: D2. by rewrite /edge_rel/= xy.
    + case: (altP (input =P output :> skeleton G)) ⇒ E.
      × case: (D1 input) ⇒ t Ht. ∃ t. by rewrite -E !Ht.
      × suff: (input : sskeleton G) -- output by apply: D2. by rewrite /edge_rel/= E !eqxx.
  - move ⇒ [[D1 D2 D3] C]. split ⇒ //= x y. case/or3P; first exact: D2.
    + case/and3P ⇒ ? /eqP E1 /eqP E2. by subst.
    + case/and3P ⇒ ? /eqP E1 /eqP E2. subst.
      case: C ⇒ t. rewrite andbC. by ∃ t.
Qed.

Lemma hom_eqL (V : finType) (e1 e2 : rel V) (G : sgraph) (h : V → G)
      (e1_sym : symmetric e1) (e1_irrefl : irreflexive e1)
      (e2_sym : symmetric e2) (e2_irrefl : irreflexive e2):
  e1 =2 e2 →
  @hom_s (SGraph e1_sym e1_irrefl) G h →
  @hom_s (SGraph e2_sym e2_irrefl) G h.
Proof. move ⇒ E hom_h x y. rewrite /edge_rel/= -E. exact: hom_h. Qed.

Lemma skel_union_join (G1 G2 : graph) : @sk_rel _ _ (union G1 G2) =2 @join_rel G1 G2.
Proof.
  move ⇒ [x|x] [y|y] /=.
  - rewrite /edge_rel/=/sk_rel sum_eqE.
    case: (boolP (x == y)) ⇒ //= E. apply/existsP/existsP.
    + move ⇒ [[e|e]]; rewrite !inE //= !sum_eqE. by ∃ e; rewrite !inE.
    + move ⇒ [e] H. ∃ (inl e). by rewrite !inE /= !sum_eqE in H ×.
  - apply: contraTF isT ⇒ /existsP [[e|e]]; by rewrite !inE //= andbC.
  - apply: contraTF isT ⇒ /existsP [[e|e]]; by rewrite !inE //= andbC.
  - rewrite /edge_rel/=/sk_rel sum_eqE.
    case: (boolP (x == y)) ⇒ //= E. apply/existsP/existsP.
    + move ⇒ [[e|e]]; rewrite !inE //= !sum_eqE. by ∃ e; rewrite !inE.
    + move ⇒ [e] H. ∃ (inr e). by rewrite !inE /= !sum_eqE in H ×.
Qed.

Section Quotients.
  Variables (G1 G2 : graph2).

  Let P : {set union G1 G2} := [set unl input; unl output; unr input; unr output].

  Definition admissible (eqv : rel (union G1 G2)) :=
    ∀ x y, eqv x y → x = y ∨ [set x;y] \subset P.

  Lemma admissible_eqv_clot (l: pairs (union G1 G2)):
    (∀ p, p \in l → p.1 \in P ∧ p.2 \in P) → admissible (eqv_clot l).
  Proof.
    move ⇒ H x y. rewrite eqv_clotE. case/connectP ⇒ p.
    have relE u v : rel_of_pairs l u v → ((u \in P) × (v \in P)) %type.
    { by move /H ⇒ /= [-> ->]. }
    elim: p x ⇒ /= [x _ → //|z p IH x /andP [E pth_p] lst_p]; first by left.
    right. rewrite subUset !sub1set. case: (IH _ pth_p lst_p) ⇒ [Z|S]; subst.
    - rewrite -Z. case/orP : E ⇒ E; by rewrite !(relE _ _ E).
    - case/orP: E ⇒ E; rewrite (relE _ _ E) /=; by abstract (set_tac).
  Qed.

  Lemma decomp_quot (T1 T2 : forest) D1 D2 (e : equiv_rel (union G1 G2)):
    sdecomp T1 (sskeleton G1) D1 → sdecomp T2 (sskeleton G2) D2 →
    width D1 ≤ 3 → width D2 ≤ 3 →
    admissible e → #|[set pi e x | x in P]| ≤ 3 →
    ∃ T D, [/\ sdecomp T (skeleton (merge _ e)) D,
              width D ≤ 3 & ∃ t,
              D t = [set \pi x | x in P]].
  Proof using.
    move ⇒ /sdecomp_sskel [dec1 comp1] /sdecomp_sskel [dec2 comp2] W1 W2 adm_e collapse_P.
    move: comp1 comp2 ⇒ [t1 /andP[t1_in t1_out]] [t2 /andP[t2_in t2_out]].
    pose T := tjoin T1 T2.
    pose D : tjoin T1 T2 → {set sjoin G1 G2}:= decompU D1 D2.
    have dec_D: sdecomp T (sjoin G1 G2) D by exact: join_decomp.
    have dis_t1_t2 : ~~ connect (@sedge T)(inl t1) (inr t2) by rewrite join_disc.
    have dis_T12 : {in [set inl t1;inr t2] &, ∀ x y, x != y → ~~ connect (@sedge T) x y}.
    { move ⇒ [?|?] [?|?] /setUP[] /set1P→ /setUP[]/set1P →.
      all: by rewrite ?eqxx // ⇒ _; rewrite sconnect_sym. }
    pose T' := @tlink T _ dis_T12.
    pose D' := decompL D P : _ → {set sjoin G1 G2}.
    have dec_D' : sdecomp T' (sjoin G1 G2) D'.
    { apply: decomp_link ⇒ //.
      apply/subsetP ⇒ x.
      rewrite !inE -!orbA => /or4P [] /eqP→.
      all: apply/bigcupP; solve
        [ by ∃ (inl t1) ⇒ //; rewrite ?inE ?mem_imset ?eqxx
        | by ∃ (inr t2) ⇒ //; rewrite ?inE ?mem_imset ?eqxx]. }
    pose h := pi e : skeleton (union G1 G2) → skeleton (merge _ e).
    ∃ T'. ∃ (rename D' h); split; last by ∃ None.
    - apply: rename_decomp ⇒ //.
      + apply: hom_eqL (pi_hom (e := e)). exact: skel_union_join.
      + exact: pi_surj.
      + move ⇒ x y. move/sk_rel_mergeE ⇒ [? [x0] [y0] /= [? ? ?]].
        ∃ x0;∃ y0. split ⇒ //. by rewrite /edge_rel/= -skel_union_join.
      + move ⇒ x y. move/eqquotP ⇒ /=. case/adm_e ⇒ [<-|A].
        × case: (sbag_cover dec_D' x) ⇒ t Ht. left. ∃ t. by rewrite Ht.
        × left. ∃ None. by rewrite /= -!sub1set -subUset.
    - rewrite /width (bigop.bigID (pred1 None)).
      rewrite bigop.big_pred1_eq. rewrite geq_max. apply/andP;split ⇒ //.
      + rewrite (bigop.reindex Some) /=.
        × apply: (@leq_trans (maxn (width D1) (width D2))); last by rewrite geq_max W1 W2.
          apply: leq_trans (join_width _ _).
          apply: bigmax_leq_pointwise ⇒ t _. exact: leq_imset_card.
        × apply: subon_bij; last by (apply bij_on_codom ⇒ //; exact: (inl t1)).
          by move ⇒ [x|]; rewrite !in_simpl // codom_f.
  Qed.

  Lemma decomp_par2 (T1 T2 : forest) D1 D2 :
    sdecomp T1 (sskeleton G1) D1 → sdecomp T2 (sskeleton G2) D2 →
    width D1 ≤ 3 → width D2 ≤ 3 →
    ∃ T D, [/\ sdecomp T (sskeleton (G1 ∥ G2)) D & width D ≤ 3].
  Proof using.
    move ⇒ dec1 dec2 W1 W2.
    case: (decomp_quot (e:=eqv_clot [:: (unl input, unr input); (unl output, unr output)])
                       dec1 dec2 W1 W2 _ _).
    - apply admissible_eqv_clot. case ⇒ u v.
      rewrite !inE /= !xpair_eqE ⇒ /orP [] /andP [/eqP → /eqP->]; by rewrite !eqxx.
    - pose P' : {set union G1 G2} := [set unl input; unl output].
      apply: (@leq_trans #|P'|); last by rewrite cards2; by case (_ != _).
      apply: (@leq_trans #|[set (\pi x : G1 ∥ G2) | x in P']|); last exact: leq_imset_card.
      apply: subset_leq_card.
      apply/subsetP ⇒ ? /imsetP [x H1 ->]. case/setUP : H1 ⇒ H1; first case/setUP : H1 ⇒ H1.
      × by rewrite mem_imset.
      × move/set1P : H1 ⇒ →. apply/imsetP. ∃ (unl input); first by rewrite !inE eqxx ?orbT.
        apply/eqquotP. eqv.
      × move/set1P : H1 ⇒ →. apply/imsetP. ∃ (unl output); first by rewrite !inE eqxx ?orbT.
        apply/eqquotP. eqv.
    - move ⇒ T [D] [A B [t C]]. ∃ T. ∃ D. split ⇒ //.
      apply/sdecomp_sskel. split ⇒ //.
      ∃ t. by rewrite C !mem_imset // !inE ?eqxx ?orbT.
  Qed.

  Lemma decomp_dot2 (T1 T2 : forest) D1 D2 :
    sdecomp T1 (sskeleton G1) D1 → sdecomp T2 (sskeleton G2) D2 →
    width D1 ≤ 3 → width D2 ≤ 3 →
    ∃ T D, [/\ sdecomp T (sskeleton (G1 · G2)) D & width D ≤ 3].
  Proof using.
    move ⇒ dec1 dec2 W1 W2.
    case: (decomp_quot (e:=eqv_clot [:: (unl output, unr input)]) dec1 dec2 W1 W2 _ _).
    - apply admissible_eqv_clot. case ⇒ u v.
      rewrite !inE /= !xpair_eqE ⇒ /andP [/eqP → /eqP->]; by rewrite !eqxx.
    - pose P' : {set union G1 G2} := [set unl input; unl output; unr output].
      apply: (@leq_trans #|P'|); last apply cards3.
      apply: (@leq_trans #|[set (\pi x : G1 · G2) | x in P']|); last exact: leq_imset_card.
      apply: subset_leq_card.
      apply/subsetP ⇒ ? /imsetP [x H1 ->]. move: H1.
      rewrite /P -!setUA [[set _;_]]setUC !setUA. case/setUP ⇒ H1.
      × by rewrite mem_imset.
      × move/set1P : H1 ⇒ →. apply/imsetP. ∃ (unl output); first by rewrite !inE eqxx ?orbT.
        apply/eqquotP. eqv.
    - move ⇒ T [D] [A B [t C]]. ∃ T. ∃ D. split ⇒ //.
      apply/sdecomp_sskel. split ⇒ //.
      ∃ t. by rewrite C !mem_imset // !inE ?eqxx ?orbT.
  Qed.

End Quotients.

Lemma decomp_cnv (G : graph2) T D :
  sdecomp T (sskeleton G) D → sdecomp T (sskeleton (G°)) D.
Proof.
  move/sdecomp_sskel ⇒ [dec cmp]. apply/sdecomp_sskel; split ⇒ //.
  move: cmp ⇒ [t] H. ∃ t ⇒ /=. by rewrite andbC.
Qed.

Lemma decomp_dom (G : graph2) T D :
  sdecomp T (sskeleton G) D → sdecomp T (sskeleton (dom G)) D.
Proof.
  move/sdecomp_sskel ⇒ [dec cmp]. apply/sdecomp_sskel; split ⇒ //.
  move: cmp ⇒ [t] /andP [H _]. ∃ t ⇒ /=. by rewrite !H.
Qed.

Theorem eval_TW2 A (f: A → graph2):
  (∀ a, ∃ T D, [/\ sdecomp T (sskeleton (f a)) D & width D ≤ 3]) →
  ∀ u, ∃ T D, [/\ sdecomp T (sskeleton (eval f u)) D & width D ≤ 3].
Proof.
  move ⇒ Hf. elim ⇒ [u IHu v IHv | u IHu v IHv | u IHu | u IHu | | | a].
  - move: IHu IHv ⇒ [T1] [D1] [? ?] [T2] [D2] [? ?].
    exact: (decomp_dot2 (D1 := D1) (D2 := D2)).
  - move: IHu IHv ⇒ [T1] [D1] [? ?] [T2] [D2] [? ?].
    exact: (decomp_par2 (D1 := D1) (D2 := D2)).
  - move: IHu ⇒ [T] [D] [D1 D2]. ∃ T. ∃ D. split ⇒ //.
    exact: decomp_cnv.
  - move: IHu ⇒ [T] [D] [D1 D2]. ∃ T. ∃ D. split ⇒ //.
    exact: decomp_dom.
  - apply: decomp_small. by rewrite card_unit.
  - apply: decomp_small. by rewrite card_sum card_unit.
  - apply Hf.
Qed.

End Subalgebra.

Section s.
Variable A: Type.
Let graph_of_term: term A → graph2 unit (flat A) := eval (fun a : flat A ⇒ g2_var _ a).

Theorem graph_of_TW2 (u : term A) :
  ∃ T D, [/\ @sdecomp T (sskeleton (graph_of_term u)) D & width D ≤ 3].
Proof.
  apply eval_TW2 ⇒ a.
  apply: decomp_small. by rewrite card_sum card_unit.
Qed.

Lemma sskel_K4_free (u : term A) : K4_free (sskeleton (graph_of_term u)).
Proof.
  case: (graph_of_TW2 u) ⇒ T [B] [B1 B2].
  exact: TW2_K4_free B1 B2.
Qed.

Lemma skel_K4_free (u : term A) : K4_free (skeleton (graph_of_term u)).
Proof.
  apply: minor_K4_free (@sskel_K4_free u).
  exact: sub_minor (skel_sub _).
Qed.


End s.