Require Import RelationClasses Morphisms Setoid Omega.

From mathcomp Require Import all_ssreflect.

Require Import edone finite_quotient preliminaries.
Require Import multigraph subalgebra.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Set Bullet Behavior "Strict Subproofs".

Local Open Scope quotient_scope.
Local Notation "\pi x" := (\pi_(_) x) (at level 4).

(* NOTE: We need to use foldr1 here since there is no neutral element
for parallel composition in the term syntax for connected graphs *)
Definition big_tmI : seq term -> term := foldr1 tm1 tmI id.

Definition iso2_congruence (op : graph2 -> graph2 -> graph2) :=
  forall (G1 G2 G1' G2' : graph2), G1 ≈ G1' -> G2 ≈ G2' -> op G1 G2 ≈ op G1' G2'.

Lemma par2_congr : iso2_congruence par2.
Proof.
  move => G1 G2 G1' G2' [f f1 f2] [g g1 g2].
  have [h [I1 I2 I3 I4]] := iso2_union f1 f2 g1 g2.
  apply: (merge_congr (h := h)) => //; try by rewrite I3 f1.
  move=> x y /=. rewrite !par2_equiv_of. apply: lift_equiv; first by case: I2.
  move=> {x y} [x|x] [y|y]; rewrite /par2_eq/= !(I3, I4) //.
  by rewrite !iso2_inv_in // !iso2_inv_out.
Qed.

Instance par2_morphisem :
  Proper (iso2 ==> iso2 ==> iso2) par2.
Proof. move => ? ? ? ? ? ?. exact: par2_congr. Qed.

Definition big_par2 (s : seq graph2) : graph2 :=
  \big[par2/top2]_(G <- s) G.

Lemma big_par2_cons G Gs :
  big_par2 (G::Gs) = par2 G (big_par2 Gs).
Proof. by rewrite /big_par2 big_cons. Qed.

Lemma par2_LR (G1 G2 : graph2) x y :
  inl x = inr y %[mod_eq @par2_eqv G1 G2] ->
  x = g_in /\ y = g_in \/ x = g_out /\ y = g_out.
Proof.
  move/eqmodP; rewrite /=/par2_eqv /eq_op/= -!/eq_op. case: ifP => i_o.
  - rewrite !inE !eqEsubset. case/orP=> /andP[H _]; move: H.
    all: rewrite subUset !sub1set !inE /eq_op/= orbF =>/andP[/eqP-> /eqP->].
    + by left.
    + by right.
  - move/negbT: i_o. rewrite negb_and !negbK. case/orP=> /eqP<-.
    all: rewrite subUset !sub1set !inE /eq_op/= !orbF orbb.
    + case/andP=> /eqP-> /orP[]/eqP->; by [left | right].
    + case/andP=> /orP[]/eqP-> /eqP->; by [left | right].
Qed.

Lemma par2_injL (G1 G2 : graph2) x y :
  g_in != g_out :> G2 ->
  inl x = inl y %[mod_eq @par2_eqv G1 G2] ->
  x = y.
Proof.
  move=> iNo2 /eqmodP/=. rewrite /par2_eqv/= iNo2 andbT sum_eqE.
  case/orP=> [/eqP//|]. case: ifP => [iNo1 | /negbFE/eqP<-].
  - rewrite !inE !eqEsubset ![[set inl x; inl y] \subset _]subUset !sub1set !inE.
    rewrite /eq_op/= !orbF. by case/orP=> /andP[]/andP[/eqP-> /eqP->].
  - by rewrite subUset !sub1set !inE /eq_op/= !orbF !orbb => /andP[/eqP-> /eqP->].
Qed.

Lemma par2_injR (G1 G2 : graph2) x y :
  g_in != g_out :> G1 ->
  inr x = inr y %[mod_eq @par2_eqv G1 G2] ->
  x = y.
Proof.
  move=> iNo2 /eqmodP/=. rewrite /par2_eqv/= iNo2 /= sum_eqE.
  case/orP=> [/eqP//|]. case: ifP => [iNo1 | /negbFE/eqP<-].
  - rewrite !inE !eqEsubset ![[set inr x; inr y] \subset _]subUset !sub1set !inE.
    rewrite /eq_op/=. by case/orP=> /andP[]/andP[/eqP-> /eqP->].
  - by rewrite subUset !sub1set !inE /eq_op/= !orbb => /andP[/eqP-> /eqP->].
Qed.

Lemma par2_idR G : par2 G top2 ≈ G.
Proof
  with try solve [by move/par2_injL => <- //
                 |by case/par2_LR => [] [? ?];subst ].
  pose f (x : par2 G top2) : G :=
    match repr x with
    | inl x => x
    | inr false => g_in
    | inr true => g_out
    end.
  pose g (x : G) : par2 G top2 := \pi (inl x).
  have c1 : cancel f g.
  { move => x. rewrite /f /g.
    case e1 : (repr x) => [a|[|]]; first by rewrite -e1 reprK.
    - rewrite -[x]reprK e1. apply/eqmodP => /=. by rewrite par2_eqv_io.
    - rewrite -[x]reprK e1. apply/eqmodP => /=. by rewrite par2_eqv_io. }
  have c2 : cancel g f.
  { move => x. rewrite /f /g.
    case: piP => [[y|[]]] Hy.
    - symmetry. exact: par2_injL Hy.
    - case: (par2_LR Hy) => [] [? ?];by subst.
    - case: (par2_LR Hy) => [] [? ?];by subst. }
  pose h (e: edge (par2 G top2)) : edge G :=
    match e with inl e => e | inr e => match e with end end.
  exists (f,h); repeat split => //=. (* simpl takes long ... *)
  - case => // e. rewrite /f. case: piP => [[y|[|]]]...
  - case => // e. rewrite /f. case: piP => [[y|[|]]]...
  - by case.
  - rewrite /f. case: piP => [[y|[|]]]...
  - rewrite /f. case: piP => [[y|[|]]]...
  - exact: Bijective c1 c2.
  - by apply: (Bijective (g := inl)) => [[e|]|].
 Qed.

Lemma par2_idL G : par2 top2 G ≈ G.
Abort.

Lemma big_par2_1 G : big_par2 [:: G] ≈ G.
Proof. rewrite /big_par2 big_cons big_nil. exact: par2_idR. Qed.

Lemma big_par2_map (r : seq term) :
  ~~ nilp r -> big_par2 (map graph_of_term r) ≈ graph_of_term (big_tmI r).
Proof.
  elim: r => //= u s. case e : (nilp s).
  - move => _ _. by rewrite (nilP e) /= /big_par2_cons big_par2_1.
  - move/(_ isT) => IH _. by rewrite big_par2_cons /= IH.
Qed.

(* TOTHINK: Do we really need to prove this ? *)
Lemma par2_assoc G1 G2 G3 :
  par2 (par2 G1 G2) G3 ≈ par2 G1 (par2 G2 G3).
Abort.

Lemma big_par2_cat r1 r2 :
  big_par2 (r1 ++ r2) ≈ par2 (big_par2 r1) (big_par2 r2).
(* Proof. *)
  (* rewrite /big_par2 big_cat_nested.  *)
  (* elim: r1 => |G r1 IH. *)
  (* - by rewrite !big_nil par2_idL. *)
  (* - by rewrite !big_cons IH par2_assoc. *)
Abort.

Lemma big_par2_congr (T:finType) (s : seq T) (g1 g2 : T -> graph2) :
  (forall x, x \in s -> g1 x ≈ g2 x) ->
  big_par2 [seq g1 x | x <- s] ≈ big_par2 [seq g2 x | x <- s].
Abort.

Lemma big_par2_congrs (T:finType) (s : {set T}) (g1 g2 : T -> graph2) :
  (forall x, x \in s -> g1 x ≈ g2 x) ->
  big_par2 [seq g1 x | x in s] ≈ big_par2 [seq g2 x | x in s].
(* Proof. *)
  (* move => A. apply: big_par2_congr => x. by rewrite mem_enum => /A. *)
Abort.

Lemma seq2_congr : iso2_congruence seq2.
  move => G1 G2 G1' G2' [f f1 f2] [g g1 g2].
  have [h [I1 I2 I3 I4]] := iso2_union f1 f2 g1 g2.
  apply: (merge_congr (h := h)) => //; try by rewrite ?(I3,I4) ?f1 ?g1.
  move=> x y /=. rewrite !seq2_equiv_of. apply: lift_equiv; first by case: I2.
  move=> {x y} [x|x] [y|y]; rewrite /seq2_eq /= !(I3,I4) //.
  by rewrite !sum_eqE !iso2_inv_in // !iso2_inv_out.
Qed.

Instance seq2_morphism : Proper (iso2 ==> iso2 ==> iso2) seq2.
Proof. move => ? ? ? ? ? ?. exact: seq2_congr. Qed.

Lemma seq2_injL (G1 G2 : graph2) (x y : G1) :
  inl x = inl y %[mod_eq @seq2_eqv G1 G2] -> x = y.
Proof.
  move=> /eqmodP. rewrite /=/seq2_eqv/= sum_eqE. case/orP=> [/eqP//|].
  by rewrite eq_sym eqEcard subUset -andbA andbCA !sub1set !inE.
Qed.

Lemma seq2_injR (G1 G2 : graph2) (x y : G2) :
  inr x = inr y %[mod_eq @seq2_eqv G1 G2] -> x = y.
Proof.
  move=> /eqmodP. rewrite /=/seq2_eqv/= sum_eqE. case/orP=> [/eqP//|].
  by rewrite eq_sym eqEcard subUset !sub1set !inE.
Qed.

Lemma seq2_LR (G1 G2 : graph2) (x : G1) (y : G2) :
  inl x = inr y %[mod_eq @seq2_eqv G1 G2] -> x = g_out /\ y = g_in.
Proof.
  move=> /eqmodP. rewrite /=/seq2_eqv/=.
  rewrite eq_sym eqEcard subUset !sub1set !inE orbC /= !sum_eqE.
  by case/andP=> /andP[/eqP<- /eqP<-].
Qed.

Lemma seq2_idR G : seq2 G one2 ≈ G.
Abort.

Lemma seq2_idL G : seq2 one2 G ≈ G.
Abort.

Lemma seq2_assoc G1 G2 G3 :
  seq2 (seq2 G1 G2) G3 ≈ seq2 G1 (seq2 G2 G3).
(* Proof. *)
  (* pose x0 := (g_in : seq2 G1 (seq2 G2 G3)). *)
  (* pose f (x : seq2 (seq2 G1 G2) G3) :  seq2 G1 (seq2 G2 G3) :=  *)
  (*   match repr x with *)
  (*   | inl y => match repr y with *)
  (*             | inl z => \pi (inl z)  *)
  (*             | inr z => \pi (inr (\pi (inl z))) *)
  (*             end *)
  (*   | inr y => \pi (inr (\pi (inr y))) *)
  (*   end. *)
  (* pose g (x :  seq2 G1 (seq2 G2 G3)) : seq2 (seq2 G1 G2) G3 :=  *)
  (*   match repr x with *)
  (*   | inr y => match repr y with *)
  (*             | inl z => \pi (inl (\pi (inr z))) *)
  (*             | inr z => \pi (inr z) *)
  (*             end *)
  (*   | inl y => \pi (inl (\pi (inl y))) *)
  (*   end. *)
  (* have Cfg : cancel f g. *)
  (* { move => x. rewrite /f /g.  *)
  (*   case e1: (repr x) => a|a. *)
  (*   case e2: (repr a) => b|b. *)
  (*   case: piP => y Hy. rewrite /= in Hy. (* why does this take to long? *) *)
  (*   case e3: y => c|c. *)
Abort.

Definition big_seq2 (s : seq graph2) := \big[seq2/one2]_(G <- s) G.

Lemma big_seq2_cons G Gs : big_seq2 (G :: Gs) = seq2 G (big_seq2 Gs).
Proof. by rewrite /big_seq2 big_cons. Qed.

Lemma big_seq2_congr (T:finType) (s : seq T) (g1 g2 : T -> graph2) :
  (forall x, x \in s -> g1 x ≈ g2 x) ->
  big_seq2 [seq g1 x | x <- s] ≈ big_seq2 [seq g2 x | x <- s].
(* Proof. *)
  (* elim: s => //= a s IH. *)
Abort.

Lemma big_seq2_congrs (T:finType) (s : {set T}) (g1 g2 : T -> graph2) :
  (forall x, x \in s -> g1 x ≈ g2 x) ->
  big_seq2 [seq g1 x | x in s] ≈ big_seq2 [seq g2 x | x in s].
(* Proof.  *)
  (* move => A. apply: big_seq2_congr => x. by rewrite mem_enum => /A. *)
Abort.

Lemma big_seq2_map (I : Type) (r : seq I) F :
  big_seq2 [seq graph_of_term (F u) | u <- r] ≈
  graph_of_term (\big[tmS/tm1]_(u <- r) F u).
Proof.
  elim: r => /= [|a r IH].
  - by rewrite /big_seq2 !big_nil.
  - by rewrite big_cons big_seq2_cons /= IH.
Qed.

(* TOTHINK: This Lemma matches the Proof below, but does it really
order the element of r in the same way *)
Lemma big_seq2_maps (I : finType) (r : {set I}) F :
  big_seq2 [seq graph_of_term (F u) | u in r] ≈
  graph_of_term (\big[tmS/tm1]_(u in r) F u).
Proof. by rewrite big_seq2_map -filter_index_enum big_filter. Qed.

Instance dom2_morphism : Proper (iso2 ==> iso2) dom2.
Proof.
  move => G G' [h /= hom_h bij_h].
  exists (h.1,h.2) => //; repeat split => //=; rewrite ?hom_h //.
  all: by move => e; rewrite hom_h.
Qed.

Local Notation IO := ([set g_in; g_out]).

Lemma iso_split_par2 (G : graph2) (C D : {set G})
  (Ci : g_in \in C) (Co : g_out \in C) (Di : g_in \in D) (Do : g_out \in D) :
  C :&: D \subset IO -> C :|: D = setT ->
  edge_set C :&: edge_set D = set0 -> edge_set C :|: edge_set D = setT ->
  G ≈ (par2 (point (induced C) (Sub g_in Ci) (Sub g_out Co))
            (point (induced D) (Sub g_in Di) (Sub g_out Do))).
Proof.
  move => subIO fullCD disjE fullE. apply: iso2_sym.
  set G1 := point _ _ _. set G2 := point _ _ _. set G' := par2 _ _.

  have injL (x y : G1) : inl x = inl y %[mod_eq @par2_eqv G1 G2] -> x = y.
  { move=> /eqmodP/=. rewrite /par2_eqv sum_eqE -!(inj_eq val_inj) !SubK andbb.
    case/orP=> [/eqP|]; first exact: val_inj.
    case: ifPn; rewrite ?negbK ?in_set2 => Eio; first case/orP.
    all: rewrite 1?eqEcard subUset !sub1set !in_setU !in_set1 !sum_eqE !orbF.
    - by case/andP=> /andP[]/eqP->/eqP->.
    - by case/andP=> /andP[]/eqP->/eqP->.
    - by case/andP=> /orP[]/eqP-> /orP[]/eqP->; apply: val_inj => //=; rewrite -(eqP Eio). }
  have injR (x y : G2) : inr x = inr y %[mod_eq @par2_eqv G1 G2] -> x = y.
  { move=> /eqmodP/=. rewrite /par2_eqv sum_eqE -!(inj_eq val_inj) !SubK andbb.
    case/orP=> [/eqP|]; first exact: val_inj.
    case: ifPn; rewrite ?negbK ?in_set2 => Eio; first case/orP.
    all: rewrite 1?eqEcard subUset !sub1set !in_setU !in_set1 !sum_eqE.
    - by case/andP=> /andP[]/eqP->/eqP->.
    - by case/andP=> /andP[]/eqP->/eqP->.
    - by case/andP=> /orP[]/eqP-> /orP[]/eqP->; apply: val_inj => //=; rewrite -(eqP Eio). }
  pose valE := f_equal val. pose inLR := par2_LR.
  pose inRL := fun e => par2_LR (esym e).

  pose f (x : G') : G := match repr x with inl x => val x | inr x => val x end.
  pose h (e : edge G') : edge G := match e with inl e => val e | inr e => val e end.
  exists (f, h); split; first split; first apply: hom_gI => e.
  all: rewrite -?[(f, h).1]/f -?[(f, h).2]/h.

  - case: e => [e|e]; rewrite /f/h; split=> //; case: piP => -[]e'.
    all: first [move/injL | move/injR | case/inLR=>-[] | case/inRL=> -[]].
    all: by repeat move=> /valE/=->.
  - rewrite /f. by case: piP => -[y /injL<-|y /inLR[][/valE? ->]].
  - rewrite /f. by case: piP => -[y /injL<-|y /inLR[][/valE? ->]].

  - have decV (v : G) : ((v \in C) + (v \in D))%type.
    { have : v \in [set: G] by []. rewrite -fullCD in_setU.
      case: (boolP (v \in C)) => HC /= HD; by [left|right]. }
    pose g (x : G) : G' :=
      match decV x with
      | inl p => \pi_(_) (inl (Sub x p))
      | inr p => \pi_(_) (inr (Sub x p))
      end.
    exists g => x; rewrite /f/g.
    + case Ex: (repr x) => [y|y]; have Hy : val y \in _ := valP y; case: (decV _) => H.
      * rewrite -[x]reprK Ex. congr \pi (inl _). exact: val_inj.
      * have {Hy} /(subsetP subIO) Hy : val y \in C :&: D by rewrite in_setI Hy H.
        rewrite in_set2 in Hy. rewrite -[x]reprK Ex. apply/eqmodP.
        rewrite /equiv/equiv_pack/par2_eqv. case: ifPn => _; last first.
        { rewrite subUset !sub1set !in_setU !in_set1.
          by rewrite !sum_eqE -!(inj_eq val_inj) !SubK !Hy. }
        rewrite in_set2 2!eqEcard !cards2 2!subUset 4!sub1set.
        rewrite 4!in_set2 !sum_eqE -!(inj_eq val_inj) !SubK.
        by rewrite /= !orbF !andbT !andbb.
      * have {Hy} /(subsetP subIO) Hy : val y \in C :&: D by rewrite in_setI Hy H.
        rewrite in_set2 in Hy. rewrite -[x]reprK Ex. apply/eqmodP.
        rewrite /equiv/equiv_pack/par2_eqv. case: ifPn => _; last first.
        { rewrite subUset !sub1set !in_setU !in_set1.
          by rewrite !sum_eqE -!(inj_eq val_inj) !SubK !Hy. }
        rewrite in_set2 2!eqEcard !cards2 2!subUset 4!sub1set.
        rewrite 4!in_set2 !sum_eqE -!(inj_eq val_inj) !SubK.
        by rewrite /= !orbF !andbT !andbb.
      * rewrite -[x]reprK Ex. congr \pi (inr _). exact: val_inj.
    + case: (decV x) => Hx; case: piP => -[]y.
      * by move=> /injL<-.
      * by case/inLR=> -[]/valE/=->->.
      * by case/inRL=> -[->]/valE/=->.
      * by move=> /injR<-.

  - have decE (e : edge G) : ((e \in edge_set C) + (e \in edge_set D))%type.
    { have : e \in [set: edge G] by []. rewrite -fullE in_setU.
      case: (boolP (e \in edge_set C)) => HC /= HD; by [left|right]. }
    pose k (e : edge G) : edge G' :=
      match decE e with
      | inl p => inl (Sub e p)
      | inr p => inr (Sub e p)
      end.
    exists k => e; rewrite /h/k; last by case: (decE e). case: e => e.
    + have He : val e \in edge_set C := valP e.
      case: (decE _) => H; first by congr inl; exact: val_inj.
      suff : val e \in edge_set C :&: edge_set D by rewrite disjE inE.
      by rewrite in_setI He H.
    + have He : val e \in edge_set D := valP e.
      case: (decE _) => H; last by congr inr; exact: val_inj.
      suff : val e \in edge_set C :&: edge_set D by rewrite disjE inE.
      by rewrite in_setI He H.
Qed.

Lemma graph_of_big_tmI (T : eqType) (r : seq T) F :
  graph_of_term (\big[tmI/tmT]_(x <- r) F x) ≈
  \big[par2/top2]_(x <- r) graph_of_term (F x).
Proof. elim: r => [|i r IH]; by rewrite ?big_nil ?big_cons /= ?IH. Qed.

Lemma graph_of_big_tmIs (T : finType) (r : {set T}) F :
  graph_of_term (\big[tmI/tmT]_(x in r) F x) ≈
  \big[par2/top2]_(x in r) graph_of_term (F x).
Proof. by rewrite -!big_enum_in graph_of_big_tmI. Qed.

Lemma big_iso_congr op (con : iso2_congruence op)
  (T : eqType) (s : seq T) idx F G :
  (forall x, x \in s -> F x ≈ G x) ->
  \big[op/idx]_(x <- s) F x ≈ \big[op/idx]_(x <- s) G x.
Proof.
  move => A.
  elim: s A => [_|i s IH /all_cons [A B]]; first by rewrite !big_nil.
  rewrite !big_cons. apply: con => //. exact: IH.
Qed.

Definition big_par2_congr' := big_iso_congr par2_congr.

Lemma iso_top (G : graph2) :
  g_in != g_out :> G ->
  (forall x : G, x \in IO) ->
  (forall e : edge G, False) -> G ≈ top2.
Proof.
  move => Dio A B.
  pose f (x : G) : top2 :=
    if x == g_in then g_in else g_out.
  pose f' (x : top2) : G :=
    if x == g_in then g_in else g_out.
  pose g (e : edge G) : edge top2 :=
    match (B e) with end.
  pose g' (e : edge top2) : edge G :=
    match e with end.
  exists (f,g); repeat split => //=.
  - by rewrite /f eqxx.
  - by rewrite /f eq_sym (negbTE Dio).
  - apply: (Bijective (g := f')) => x; rewrite /f /f'.
    + case: (boolP (x == g_in)) => [/eqP <-|/=]; first by rewrite eqxx.
      move: (A x). case/setUP => /set1P => -> //. by rewrite eqxx.
    + case: (boolP (x == g_in)) => [/eqP <-|/=]; first by rewrite eqxx.
      case: x => // _. by rewrite eq_sym (negbTE Dio).
  - by apply: (Bijective (g := g')).
Qed.

Lemma iso_one (G : graph2) :
  g_in == g_out :> G ->
  (forall x : G, x \in IO) ->
  (forall e : edge G, False) -> G ≈ one2.
Proof.
  move => Dio A B.
  pose f (x : G) : one2 := g_in.
  pose f' (x : one2) : G := g_in.
  pose g (e : edge G) : edge one2 :=
    match (B e) with end.
  pose g' (e : edge one2) : edge G :=
    match e with end.
  exists (f,g); repeat split => //=.
  - apply: (Bijective (g := f')) => x; rewrite /f /f'.
    move: (A x). rewrite !inE -(eqP Dio) => /orP. by case => /eqP->.
    by case: x.
  - by apply: (Bijective (g := g')).
Qed.