Require Import Setoid Morphisms.
From mathcomp Require Import all_ssreflect.
Require Import edone finite_quotient preliminaries bij equiv.
Require Export structures mgraph ptt.

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

(* TODO:
 - input/output as a function from bool?
 - recheck status of unr/unl
 *)

Section s.

Variable L: labels.
Notation Lv := (lv L).
Notation Le := (le L).
Notation graph := (graph L).
Local Open Scope labels.

(* 2p-graphs  *)
Set Primitive Projections.
Record graph2 :=
  Graph2 {
      graph_of:> graph;
      input: graph_of;
      output: graph_of }.
Arguments input {_}.
Arguments output {_}.
Notation point G := (@Graph2 G).

(* basic operations *)
Definition add_vertex2 (G: graph2) a := point (add_vertex G a) (unl input) (unl output).
Definition add_edge2 (G: graph2) (x y: G) u := point (add_edge G x y u) input output.
Definition add_vlabel2 (G: graph2) (x: G) a := point (add_vlabel G x a) input output.
Definition merge2 (G: graph2) (r: equiv_rel G) := point (merge G r) (\pi input) (\pi output).
Arguments merge2 _ _: clear implicits.

Notation "G ∔ a" :=
  (add_vertex2 G a) (at level 20, left associativity).
Notation "G ∔ [ x , u , y ]" :=
  (@add_edge2 G x y u) (at level 20, left associativity).
Notation "G [tst x <- a ]" :=
  (@add_vlabel2 G x a) (at level 20, left associativity).
Notation merge2_seq G l := (merge2 G (eqv_clot l)).

(* basic graphs *)
Definition unit_graph2 a := point (unit_graph a) tt tt.
Definition two_graph2 a b := point (two_graph a b) (inl tt) (inr tt).
Definition edge_graph2 a u b := two_graph2 a b ∔ [inl tt, u, inr tt].

Universe S2.
Set Primitive Projections.
Record iso2 (F G: graph2): Type@{S2} :=
  Iso2 { iso2_iso:> F ≃ G;
         iso2_input: iso2_iso input = input;
         iso2_output: iso2_iso output = output }.
Infix "≃2" := iso2 (at level 79).

Definition iso2_id (G: graph2): G ≃2 G.
Proof. by exists iso_id. Defined.
Hint Resolve iso2_id : core. (* so that by gets it... *)

Definition iso2_sym F G: F ≃2 G -> G ≃2 F.
Proof.
  intro h. exists (iso_sym h).
    by rewrite /= -(bijK h input) iso2_input.
    by rewrite /= -(bijK h output) iso2_output.
Defined.

Definition iso2_comp F G H: F ≃2 G -> G ≃2 H -> F ≃2 H.
Proof.
  move => f g.
  exists (iso_comp f g); by rewrite /= ?iso2_input ?iso2_output.
Defined.

Global Instance iso2_Equivalence: CEquivalence iso2.
Proof. split. exact iso2_id. exact iso2_sym. exact iso2_comp. Qed.

(* Prop version *)
Definition iso2prop (F G: graph2) := inhabited (F ≃2 G).
Infix "≃2p" := iso2prop (at level 79).
Global Instance iso2prop_Equivalence: Equivalence iso2prop.
Proof.
  split.
  - by constructor.
  - intros G H [f]. constructor. by symmetry.
  - intros F G H [h] [k]. constructor. etransitivity; eassumption.
Qed.
Canonical Structure g2_setoid: setoid := Setoid iso2prop_Equivalence.

Tactic Notation "Iso2" uconstr(f) :=
  match goal with |- ?F ≃2 ?G => refine (@Iso2 F G f _ _)=>// end.

(* NOTE: used sparsely *)
Lemma iso_iso2 (F G: graph) (h: F ≃ G) (i o: F):
  point F i o ≃2 point G (h i) (h o).
Proof. now exists h. Defined.

(* NOTE: to be removed: the Iso2 tactic does the job... *)
Lemma iso_iso2' (F G: graph) (h: F ≃ G) (i o: F) (i' o': G):
  h i = i' -> h o = o' -> point F i o ≃2 point G i' o'.
Proof. intros. Iso2 h. Defined.

(* simple tactics for rewriting with isomorphisms at toplevel, in the lhs or in the rhs
   (used in place of setoid_rewrite or rewrite->, which are pretty slow, or just don't work) *)
Tactic Notation "irewrite" uconstr(L) := (eapply iso2_comp;[apply L|]); last 1 first.
Tactic Notation "irewrite'" uconstr(L) := eapply iso2_comp;[|apply iso2_sym, L].

(* parallel composition *)
Definition g2_par (F G: graph2) :=
  point (merge_seq (F ⊎ G) [::(unl input,unr input); (unl output,unr output)])
        (\pi (unl input)) (\pi (unr output)).
  (* merge2_seq (point (F ⊎ G) (inl input) (inr output)) *)
  (*            ::(inl input,inr input); (inl output,inr output). *)

(* sequential composition *)
Definition g2_dot (F G: graph2) :=
  point (merge_seq (F ⊎ G) [::(unl output,unr input)])
        (\pi (unl input)) (\pi (unr output)).
  (* merge2_seq (point (F ⊎ G) (inl input) (inr output)) *)
  (*            ::(inl output,inr input). *)

Definition g2_cnv (F: graph2) := point F output input.

Definition g2_dom (F: graph2) := point F input input.

Definition g2_one: graph2 := unit_graph2 1.

Definition g2_top: graph2 := two_graph2 1 1.

Definition g2_var a: graph2 := edge_graph2 1 a 1.

(* Note: would be nicer to prove that this is a 2p algebra (with top)
   and deduce automatically that this is a 2pdom  *)
Canonical Structure g2_ops: pttdom.ops_ :=
  {| dot := g2_dot;
     par := g2_par;
     cnv := g2_cnv;
     dom := g2_dom;
     one := g2_one;
     top := g2_top |}.

(* mostly recasting the ones proved in mgraph  *)

(* isomorphisms about unit_graph2 *)

Global Instance unit_graph2_iso: CProper (eqv ==> iso2) unit_graph2.
Proof. intros a b e. Iso2 (unit_graph_iso e). Defined.

(* isomorphisms about two_graph2 *)

Global Instance two_graph2_iso: CProper (eqv ==> eqv ==> iso2) two_graph2.
Proof. intros a b ab c d cd. Iso2 (union_iso (unit_graph_iso ab) (unit_graph_iso cd)). Defined.

(* isomorphisms about two_vertex2 *)

Global Instance add_vertex2_iso: CProper (iso2 ==> eqv ==> iso2) add_vertex2.
Proof.
  move => F G FG u v uv.
  Iso2 (union_iso FG (unit_graph_iso uv))=>/=; rewrite /unl/=; f_equal; apply FG.
Defined.

(* isomorphisms about add_edge2 *)

Lemma add_edge2_iso'' F G (h: F ≃2 G) x x' (ex: h x = x') y y' (ey: h y = y') u v (e: u ≡ v):
  F ∔ [x, u, y] ≃2 G ∔ [x', v, y'].
Proof. Iso2 (add_edge_iso'' ex ey e); apply h. Defined.

Lemma add_edge2_iso' F G (h: F ≃2 G) x u v y (e: u ≡ v): F ∔ [x, u, y] ≃2 G ∔ [h x, v, h y].
Proof. by eapply add_edge2_iso''. Defined.

Lemma add_edge2_iso F G (h: F ≃2 G) x u y: F ∔ [x, u, y] ≃2 G ∔ [h x, u, h y].
Proof. by apply add_edge2_iso'. Defined.

Lemma add_edge2_C F x u y z v t: F ∔ [x, u, y] ∔ [z, v, t] ≃2 F ∔ [z, v, t] ∔ [x, u, y].
Proof. Iso2 (add_edge_C _ _ _). Defined.

Lemma add_edge2_rev F x u v y (e: u ≡' v): F ∔ [x, u, y] ≃2 F ∔ [y, v, x].
Proof. Iso2 (add_edge_rev _ _ e). Defined.

Lemma add_edge2_vlabel F x a y u z: F [tst x <- a] ∔ [y, u, z] ≃2 F ∔ [y, u, z] [tst x <- a].
Proof. Iso2 (add_edge_vlabel _ _ _). Defined.

(* isomorphisms about edge_graph2 *)

Global Instance edge_graph2_iso: CProper (eqv ==> eqv ==> eqv ==> iso2) edge_graph2.
Proof. intros a b ab u v uv c d cd. refine (add_edge2_iso' (two_graph2_iso ab cd) _ _ uv). Defined.

(* isomorphisms about add_vlabel2 *)

Lemma add_vlabel2_iso'' F G (h: F ≃2 G) x x' (ex: h x = x') a b (e: a ≡ b): F [tst x <- a] ≃2 G [tst x' <- b].
Proof. Iso2 (add_vlabel_iso'' ex e); apply h. Defined.

Lemma add_vlabel2_iso' F G (h: F ≃2 G) x a b (e: a ≡ b): F [tst x <- a] ≃2 G [tst h x <- b].
Proof. by eapply add_vlabel2_iso''. Defined.

Lemma add_vlabel2_iso F G (h: F ≃2 G) x a: F [tst x <- a] ≃2 G [tst h x <- a].
Proof. by apply add_vlabel2_iso'. Defined.

Lemma add_vlabel2_C F x a y b: F [tst x <- a] [tst y <- b] ≃2 F [tst y <- b] [tst x <- a].
Proof. Iso2 (add_vlabel_C _ _). Defined.

Lemma add_vlabel2_unit a x b: unit_graph2 a [tst x <- b] ≃2 unit_graph2 (a⊗b).
Proof. Iso2 (add_vlabel_unit _ _). Defined.

Lemma add_vlabel2_unit' x b: unit_graph2 b ≃2 unit_graph2 1 [tst x <- b].
Proof. apply iso2_sym. irewrite add_vlabel2_unit. apply unit_graph2_iso. by rewrite monC monU. Defined.

Lemma add_vlabel2_two a b (x: unit+unit) c:
  two_graph2 a b [tst x <- c] ≃2 two_graph2 (if x then a⊗c else a) (if x then b else b⊗c).
Proof. Iso2 (add_vlabel_two _ _ _ _); by case x; case. Defined.

Lemma add_vlabel2_edge a u b (x: unit+unit) c:
  edge_graph2 a u b [tst x <- c] ≃2 edge_graph2 (if x then a⊗c else a) u (if x then b else b⊗c).
Proof. Iso2 (add_vlabel_edge _ _ _ _ _); by case x; case. Defined.

Lemma add_vlabel2_mon0 G x: G [tst x <- 1] ≃2 G.
Proof. Iso2 (add_vlabel_mon0 x). Defined.

(* isomorphisms about merge *)

Lemma merge2_iso2 F G (h: F ≃2 G) l:
  merge2_seq F l ≃2 merge2_seq G (map_pairs h l).
  (* note: h should be informative so that map_pairs can be simplified... *)
Proof. Iso2 (merge_iso h l); by rewrite h_mergeE ?iso2_input ?iso2_output. Qed.

Lemma merge_iso2 (F G : graph) (h: F ≃ G) l (i o: F):
  point (merge_seq F l) (\pi i) (\pi o) ≃2
  point (merge_seq G (map_pairs h l)) (\pi (h i)) (\pi (h o)).
Proof. Iso2 (merge_iso h l); by rewrite h_mergeE. Defined.

Lemma merge2_surj (G: graph2) (r: equiv_rel G) (H: graph2) (fv : G -> H) (fv': H -> G) (fe : bij (edge G) (edge H)):
  (forall x y, reflect (kernel fv x y) (r x y)) ->
  cancel fv' fv ->
  (forall b e, fv (endpoint b e) = endpoint b (fe e)) ->
  (forall e, elabel (fe e) ≡ elabel e) ->
  (forall y: H, vlabel y ≡ \big[mon2/mon0]_(x | fv x == y) vlabel x) ->
  fv input = input -> fv output = output ->
  merge2 G r ≃2 H.
Proof.
  intros H1 H2 H3 H4 H5 I O.
  Iso2 (merge_surj H1 H2 H3 H4 H5); by rewrite merge_surjE.
Defined.

Lemma merge_same (F : graph) (h k: equiv_rel F) (i i' o o': F):
  (h =2 k) ->
  h i i' ->
  h o o' ->
  point (merge F h) (\pi i) (\pi o) ≃2 point (merge F k) (\pi i') (\pi o').
Proof.
  intros H Hi Ho.
  Iso2 (merge_same' H);
    rewrite merge_same'E =>//;
    apply /eqquotP; by rewrite <- H.
Defined.

Lemma merge_same' (F : graph) (h k: equiv_rel F) (i o: F):
  (h =2 k) ->
  point (merge F h) (\pi i) (\pi o) ≃2 point (merge F k) (\pi i) (\pi o).
Proof. intros. by apply merge_same. Defined.

Lemma merge2_same (F : graph) (h k: equiv_rel F) (i i' o o': F):
  (h =2 k) -> h i i' -> h o o' -> merge2 (point F i o) h ≃2 merge2 (point F i' o') k.
Proof. apply merge_same. Qed.

Lemma merge2_same' (F : graph2) (h k: equiv_rel F):
  (h =2 k) -> merge2 F h ≃2 merge2 F k.
Proof. intro. by apply merge2_same. Qed.

Lemma merge_nothing (F: graph) (h: pairs F) (i o: F):
  List.Forall (fun p => p.1 = p.2) h ->
  point (merge_seq F h) (\pi i) (\pi o) ≃2 point F i o.
Proof. intros H. Iso2 (merge_nothing H); by rewrite merge_nothingE. Defined.

Lemma merge2_nothing (F: graph2) (h: pairs F):
  List.Forall (fun p => p.1 = p.2) h ->
  merge2_seq F h ≃2 F.
Proof. destruct F. apply merge_nothing. Defined.

Lemma merge_merge (G: graph) (h k: pairs G) (k': pairs (merge_seq G h)) (i o: G):
  k' = map_pairs (pi (eqv_clot h)) k ->
  point (merge_seq (merge_seq G h) k') (\pi (\pi i)) (\pi (\pi o))
≃2 point (merge_seq G (h++k)) (\pi i) (\pi o).
Proof. intro K. Iso2 (merge_merge_seq K); by rewrite /=merge_merge_seqE. Qed.

Lemma merge2_merge (G: graph2) (h k: pairs G) (k': pairs (merge_seq G h)):
  k' = map_pairs (pi (eqv_clot h)) k ->
  merge2_seq (merge2_seq G h) k' ≃2 merge2_seq G (h++k).
Proof. apply merge_merge. Qed.

Lemma merge_union_K_l (F K: graph) (i o: F+K) (h: pairs (F+K)) (k: K -> F)
      (kv: forall x: K, vlabel x = 1)
      (ke: edge K -> False)
      (kh: forall x: K, unr x = unl (k x) %[mod (eqv_clot h)]):
  point (merge_seq (F ⊎ K) h) (\pi i) (\pi o)
≃2 point (merge_seq F (union_K_pairs h k)) (\pi (sum_left k i)) (\pi (sum_left k o)).
Proof. Iso2 (merge_union_K kv kh ke)=>/=; by rewrite ?merge_union_KE. Defined.

Lemma merge2_add_edge (G: graph2) (r: equiv_rel G) x u y: merge2 (G ∔ [x, u, y]) r ≃2 merge2 G r ∔ [\pi x, u, \pi y].
Proof. Iso2 (merge_add_edge _ _ _ _); by rewrite merge_add_edgeE. Defined.

Lemma merge2_add_vlabel (G: graph2) (r: equiv_rel G) x a: merge2 (G [tst x <- a]) r ≃2 merge2 G r [tst \pi x <- a].
Proof. Iso2 (merge_add_vlabel _ _ _); by rewrite merge_add_vlabelE. Defined.

(* TODO: for now the 2p laws are all proved in Type iso2, 
   because some of them could be useful in Type in open.v and reduction.v
   (simple ones like commutativity to get symmetry reasonning, 
    but also CProper)
   we might want to downgrade some of them to Prop iso2prop
 *)

Lemma par2C (F G: graph2): F ∥ G ≃2 G ∥ F.
Proof.
  irewrite (merge_iso2 (union_C F G)) =>/=.
  apply merge_same. apply eqv_clot_eq; leqv. eqv. eqv.
Qed.

Lemma par2top (F: graph2): F ∥ top ≃2 F.
Proof.
  irewrite (merge_union_K_l (K:=g2_top) _ _ (k:=fun b => if b then input else output))=>/=; try by repeat case.
  apply merge2_nothing.
  by repeat constructor.
  repeat case; apply /eqquotP; eqv.
Qed.

Lemma par2A (F G H: graph2): F ∥ (G ∥ H) ≃2 (F ∥ G) ∥ H.
Proof.
  irewrite (merge_iso2 (union_merge_r _ _)).
  rewrite /map_pairs/map 2!union_merge_rEl 2!union_merge_rEr /=.
  irewrite (merge_merge (G:=F ⊎ (G ⊎ H))
                        (k:=[::(unl input,unr (unl input)); (unl output,unr (unr output))]))=>//.
  irewrite' (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /=.
  irewrite' (merge_merge (G:=(F ⊎ G) ⊎ H)
                              (k:=[::(unl (unl input),unr input); (unl (unr output),unr output)]))=>//.
  irewrite (merge_iso2 (union_A _ _ _)).
  apply merge_same'. rewrite /unl/unr/=.
  set a := inl _. set (b := inl _). set (c := inl _). set (d := inl _). set (e := inr _). set (f := inr _).
  apply eqv_clot_eq=>/=.
   constructor. apply eqv_clot_trans with c; eqv.
   constructor. apply eqv_clot_trans with b; eqv.
   constructor. eqv.
   constructor. apply eqv_clot_trans with b; eqv.
   leqv.

   constructor. eqv.
   constructor. apply eqv_clot_trans with f; eqv.
   constructor. apply eqv_clot_trans with a; eqv.
   leqv.
Qed.

Lemma dot2unit_r (G: graph2) a: G · unit_graph2 a ≃2 G [tst output <- a].
Proof.
  (* compositional proof *)
  (* a bit messy because merge_union_K only allows us to kill mon0-labelled vertices
     (a more general version of merge_union_K is possible, but requires updating the 
     labels of several vertices at once *)
  irewrite (merge_iso2 (union_iso iso_id (add_vlabel2_unit' output _))). simpl.
  etransitivity. refine (merge_iso2 (union_add_vlabel_r _ _ _) _ _ _). simpl.
  etransitivity. refine (iso_iso2 (merge_add_vlabel _ _ _) _ _). simpl.
  etransitivity. refine (iso_iso2 (add_vlabel_iso (merge_union_K_l (K:=g2_one) (unl input) (unl output) (k:=fun _ => output) _ _ _) _ _) _ _)=>//.
  case; apply /eqquotP; eqv. simpl.
  rewrite !merge_union_KE/=.
  etransitivity. refine (add_vlabel2_iso (merge2_nothing _) _ _).
  repeat (constructor=>//).
  destruct G=>/=. by rewrite merge_nothingE.
Qed.

Lemma dot2unit_r' (G: graph2) a: G · unit_graph2 a ≃2 G [tst output <- a].
Proof.
  (* global proof, via surjective homomorphism *)
  unshelve Iso2
   (@merge_surj _
     (G ⊎ unit_graph2 a) _
     (G [tst output <- a])
     (fun x => match x with inl y => y | inr tt => output end)
     (fun x => unl x)
     sumxU _ _ _ _ _).
  6,7: by rewrite merge_surjE.
  - apply kernel_eqv_clot.
    * by constructor.
    * case=>[x|[]]; case=>[y|[]]=>//->; eqv.
  - by [].
  - by move=>b [e|[]].
  - by case.
  - move=>x/=. rewrite (big_sum x tt) big_pred1_eq.
    case: (altP (x =P output)) => [?|xDo]; subst.
    + by rewrite (big_pred1 tt) => [|[]]; rewrite 1?monC /= ?eqxx.
    + rewrite big_pred0 ?monU // => [[]]. by rewrite eq_sym (negbTE xDo).
Qed.

Local Close Scope labels.

(* dot2one follows from dot2unit_r *)
Lemma dot2one (F: graph2): F · 1 ≃2 F.
Proof. irewrite dot2unit_r. apply add_vlabel2_mon0. Qed.

(* ... but also has a reasonable direct proof *)
Lemma dot2one' (F: graph2): F · 1 ≃2 F.
Proof.
  irewrite (merge_union_K_l (K:=g2_one) _ _ (k:=fun _ => output))=>//.
  apply merge2_nothing.
  repeat (constructor =>//).
  intros []; apply /eqquotP; eqv.
Qed.

(* half of associativity *)
Lemma dot2Aflat (F G H: graph2):
  F·(G·H) ≃2
  point (merge_seq (F ⊎ (G ⊎ H))
                   [::(unr (unl output),unr (unr input));
                      (unl output,unr (unl input))])
        (\pi unl input) (\pi unr (unr output)).
Proof.
  irewrite (merge_iso2 (union_merge_r _ _)).
  rewrite /map_pairs/map 2!union_merge_rEl 2!union_merge_rEr /fst/snd.
  irewrite (merge_merge (G:=F ⊎ (G ⊎ H))
                              (k:=[::(unl output,unr (unl input))])) =>//.
Qed.

Lemma dot2A (F G H: graph2): F · (G · H) ≃2 (F · G) · H.
Proof.
  irewrite dot2Aflat.
  irewrite' (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /fst/snd.
  irewrite' (merge_merge (G:=(F ⊎ G) ⊎ H)
                              (k:=[::(unl (unr output),unr input)])) =>//.
  irewrite (merge_iso2 (union_A _ _ _)).
  apply merge_same'=>/=.
  apply eqv_clot_eq; leqv.
Qed.

Lemma cnv2I (F: graph2): F°° ≃2 F.
Proof. by case F. Qed.

Lemma cnv2par (F G: graph2): (F ∥ G)° ≃2 F° ∥ G°.
Proof.
  apply merge_same. apply eqv_clot_eq; leqv. eqv. eqv.
Qed.

Lemma cnv2dot (F G: graph2): (F · G)° ≃2 G° · F°.
Proof.
  irewrite (merge_iso2 (union_C F G)).
  apply merge_same'=>/=. apply eqv_clot_eq; leqv.
Qed.

Lemma par2dot F G: @input F = output -> @input G = output -> F ∥ G ≃2 F · G.
Proof.
  intros HF HG. apply merge2_same; rewrite !HF !HG //.
  apply eqv_clot_eq; leqv.
Qed.

Lemma par2oneone: 1 ∥ 1 ≃2 1.
Proof. etransitivity. apply par2dot=>//. apply dot2one. Qed.

Lemma dom2E (F: graph2): dom F ≃2 1 ∥ (F · top).
Proof.
  symmetry.
  irewrite par2C.
  irewrite (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 1!union_merge_lEr /=.
  irewrite (merge_merge (G:=(F ⊎ g2_top) ⊎ g2_one)
                              (k:=[::(inl (inl input),inr tt); (inl (inr (inr tt)),inr tt)])) =>//.
  irewrite (merge_iso2 (iso_sym (union_A _ _ _))).
  irewrite (merge_union_K_l (K:=g2_top ⊎ g2_one) _ _
                            (k:=fun x => match x with inl (inl tt) => output | _ => input end))=>/=.
  apply merge_nothing.
  repeat (constructor =>//=).
  by intros [[]|].
  by intros [[]|].
  repeat case; apply /eqquotP; try eqv.
  apply eqv_clot_trans with (inr (inr tt)); eqv.
Qed.

Lemma g2_A10 (F G: graph2): 1 ∥ F·G ≃2 dom (F ∥ G°).
Proof.
  irewrite (par2C 1).
  irewrite (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 1!union_merge_lEr /fst/snd.
  irewrite (merge_merge (G:=(F ⊎ G) ⊎ g2_one)
                              (k:=[::(unl (unl input),inr tt); (unl (unr output),inr tt)])) =>//.
  irewrite (merge_union_K_l (F:=F ⊎ G) _ _ (k:=fun x => unl input))=>//=.
  2: by intros []; apply /eqquotP; simpl; eqv.
  apply merge_same; simpl.
  apply eqv_clot_eq; simpl; leqv.
  eqv.
  eqv.
Qed.

(* TOFIX: topL should be obtained from topR by duality *)
Lemma topL (F: graph2): top·F ≃2 point (F ⊎ unit_graph 1%lbl) (@unr _ F (unit_graph _) tt) (unl output).
Proof.
  irewrite (merge_iso2 (union_C _ _))=>/=.
  etransitivity. refine (merge_iso2 (union_A _ _ _) _ _ _)=>/=.
  irewrite (merge_union_K_l (F:=F ⊎ _) _ _ (k:=fun x => unl input))=>//=.
  apply merge_nothing. by constructor.
  intros []. apply /eqquotP. eqv.
Qed.

Lemma topR (F: graph2): F·top ≃2 point (F ⊎ unit_graph 1%lbl) (unl input) (@unr _ F (unit_graph _) tt).
Proof.
  irewrite (merge_iso2 (union_iso iso_id (union_C _ _))).
  irewrite (merge_iso2 (union_A _ _ _)).
  irewrite (merge_union_K_l (F:=F ⊎ _) _ _ (k:=fun x => unl output))=>//=.
  apply merge_nothing. by constructor.
  case. apply /eqquotP. eqv.
Qed.

Lemma g2_A11 (F: graph2): F·top ≃2 dom F·top.
Proof. irewrite topR. symmetry. by irewrite topR. Qed.

Lemma g2_A12' (F G: graph2): @input F = @output F -> F·G ≃2 F·top ∥ G.
Proof.
  intro H.
  irewrite' (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /=.
  irewrite' (merge_merge (G:=(F ⊎ g2_top) ⊎ G)
                              (k:=[::(inl (inl input),inr input);(inl (inr (inr tt)),inr output)])) =>//.
  irewrite' (merge_iso2 (union_C (_ ⊎ _) _)).
  irewrite' (merge_iso2 (union_A _ _ _))=>/=.
  irewrite' (merge_union_K_l (F:=G ⊎ F) (K:=g2_top) _ _
                             (k:=fun x => if x then unr input else unl output))=>//.
  2: by case. 2: by repeat case; apply /eqquotP; rewrite H; eqv.
  irewrite (merge_iso2 (union_C F G)) =>/=.
  apply merge_same'. rewrite H. apply eqv_clot_eq; leqv.
  repeat case=>//=; rewrite H; apply /eqquotP; eqv.
Qed.

Lemma g2_A12 (F G: graph2): (F ∥ 1)·G ≃2 (F ∥ 1)·top ∥ G.
Proof.
  apply g2_A12'.
  apply /eqquotP. apply eqv_clot_trans with (inr tt); eqv.
Qed.

(*

(* these two laws are skipped since we go through 2p algebra *)

Lemma g2_A13 (F G: graph2): dom(F·G) ≃2 dom(F·dom G).
Proof. reflexivity. Qed.

Lemma g2_A14' (F G H: graph2): @input F = output -> F·(G∥H) ≃2 F·G ∥ H.
Proof.
  intro E. 
  irewrite (merge_iso2 (union_merge_r _ _)).
  rewrite /map_pairs/map 2!union_merge_rEl 2!union_merge_rEr /=.
  irewrite (merge_merge (G:=F ⊎ (G ⊎ H))
                        (k:=::(unl output,unr (unl input))))=>//.
  irewrite' (merge_iso2 (union_merge_l _ _)).
  rewrite /map_pairs/map 2!union_merge_lEl 2!union_merge_lEr /=.
  irewrite' (merge_merge (G:=(F ⊎ G) ⊎ H)
                              (k:=::(unl (unl input),unr input); (unl (unr output),unr output)))=>//.
  irewrite (merge_iso2 (union_A _ _ _)).
  apply merge_same'. rewrite /unl/unr/=E.
  set a := inl _. set (b := inl _). set (c := inl _). set (e := inr _). set (f := inr _).
  apply eqv_clot_eq=>/=.  
   constructor=>/=. apply eqv_clot_trans with c; eqv.
   leqv. 
   constructor. eqv. 
   constructor=>/=. apply eqv_clot_trans with a; eqv. 
   leqv. 
Qed.

Lemma g2_A14 (F G H: graph2): dom F·(G∥H) ≃2 dom F·G ∥ H.
Proof. by apply g2_A14'. Qed.
 *)

Global Instance dot_iso2: CProper (iso2 ==> iso2 ==> iso2) g2_dot.
Proof.
  intros F F' f G G' g. rewrite /g2_dot.
  irewrite (merge_iso2 (union_iso f g))=>/=.
  apply merge_same; by rewrite /= ?iso2_input ?iso2_output.
Qed.

Global Instance par_iso2: CProper (iso2 ==> iso2 ==> iso2) g2_par.
Proof.
  intros F F' f G G' g. rewrite /g2_par.
  irewrite (merge_iso2 (union_iso f g))=>/=.
  apply merge_same; by rewrite /= ?iso2_input ?iso2_output.
Qed.

Global Instance cnv_iso2: CProper (iso2 ==> iso2) g2_cnv.
Proof. intros F F' f. eexists; apply f. Qed.

Global Instance dom_iso2: CProper (iso2 ==> iso2) g2_dom.
Proof. intros F F' f. eexists; apply f. Qed.

(* 2p-graphs form a 2pdom algebra (Proposition 5.2) *)
Definition g2_ptt: ptt.
  refine (@Build_ptt g2_ops _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
     abstract apply CProper2, dot_iso2.
     abstract apply CProper2, par_iso2.
     abstract apply CProper1, cnv_iso2.
     abstract (exists; apply dom2E).
     abstract (exists; apply par2A).
     abstract (exists; apply par2C).
     abstract (exists; apply dot2A).
     abstract (exists; apply dot2one).
     abstract (exists; apply cnv2I).
     abstract (exists; apply cnv2par).
     abstract (exists; apply cnv2dot).
     abstract (exists; apply par2oneone).
     abstract (exists; apply g2_A10).
     abstract (exists; apply g2_A11).
     abstract (exists; apply g2_A12).
Defined.
Canonical g2_ptt.

(* TODO should be inferred via ptt.pttdom_of, but required for below for applying cnv_eqv *)
(* Canonical Structure g2_pttdom: pttdom := Eval hnf in ptt.pttdom_of g2_ptt. *)
Definition g2_pttdom: pttdom.
  refine (@Build_pttdom g2_ops _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
     abstract apply dot_eqv_.
     abstract apply par_eqv_.
     abstract apply cnv_eqv_.
     abstract apply dom_eqv_.
     abstract apply parA_.
     abstract apply parC_.
     abstract apply dotA_.
     abstract apply dotx1_.
     abstract apply cnvI_.
     abstract apply cnvpar_.
     abstract apply cnvdot_.
     abstract apply par11_.
     abstract apply A10_.
     abstract apply A13_.
     abstract apply A14_.
Defined.
Canonical g2_pttdom.

(* additional lemmas needed in reduction.v *)
Local Open Scope labels.

Lemma dot2unit_l (G: graph2) a: unit_graph2 a · G ≃2 G [tst input <- a].
Proof.
  irewrite (iso2_sym (cnv2I _)).
  irewrite' (iso2_sym (cnv2I _)).
  apply cnv_iso2.
  irewrite cnv2dot.
  apply dot2unit_r.
Qed.

Lemma par2unitunit a b: unit_graph2 a ∥ unit_graph2 b ≃2 unit_graph2 (a⊗b).
Proof.
  etransitivity. apply par2dot=>//.
  etransitivity. apply dot2unit_r.
  apply add_vlabel2_unit.
Qed.

Lemma par2edgeunit a u b c: edge_graph2 a u b ∥ unit_graph2 c ≃2 unit_graph2 (a⊗(b⊗c)) ∔ [tt, u, tt].
  unshelve Iso2
   (@merge_surj _ (edge_graph2 a u b ⊎ unit_graph2 c) _ (unit_graph2 (a⊗(b⊗c)) ∔ [tt, u, tt])
     (fun _ => tt)
     (fun _ => inr tt)
     (bij_comp sumxU (option_bij sumxU)) _ _ _ _ _).
  (* 6,7: by rewrite merge_surjE. *)
  - apply kernel_eqv_clot.
    * by repeat constructor.
    * (repeat case)=>//=_; try eqv; apply eqv_clot_trans with (inr tt); eqv.
  - by case.
  - move=>d. by repeat case.
  - by repeat case.
  - repeat case=>//=. rewrite eqxx /= (big_sum (inl tt) tt) (big_sum tt tt).
    by rewrite !(big_pred1 tt) ?monA //.
Qed.

(* lemmas for term extraction *)

Lemma subgraph_for_iso (G : graph2) V1 V2 E1 E2 i1 i2 o1 o2
  (C1 : @consistent _ G V1 E1) (C2: consistent V2 E2) :
  V1 = V2 -> E1 = E2 -> val i1 = val i2 -> val o1 = val o2 ->
  point (subgraph_for C1) i1 o1 ≃2 point (subgraph_for C2) i2 o2.
Proof.
  move => eq_V eq_E eq_i eq_o. subst.
  move/val_inj : eq_i => ->. move/val_inj : eq_o => ->.
  unshelve Iso2 (@Iso _ (subgraph_for C1) (subgraph_for C2) bij_id bij_id xpred0 _).
  split=>//e b//=. by apply val_inj.
Qed.

Lemma iso2_subgraph_forT (G : graph2) (V : {set G}) (E : {set edge G}) (con : consistent V E) i o :
  (forall x, x \in V) -> (forall e, e \in E) -> val i = input -> val o = output ->
  point (subgraph_for con) i o ≃2 G.
Proof.
  move => HV HE Hi Ho.
  have ? : V = [set: G] by apply/setP => z; rewrite inE HV.
  have ? : E = [set: edge G] by apply/setP => z; rewrite inE HE.
  subst.
  transitivity (point (subgraph_for (@consistentTT _ G)) i o).
  - exact: subgraph_for_iso.
  - irewrite (iso_iso2 (iso_subgraph_forT _)). rewrite /= Ho Hi. by case G.
Qed.

End s.

(* Declare Scope graph2_scope. compat:coq-8.9*)
Bind Scope graph2_scope with graph2.
Delimit Scope graph2_scope with G2.

Arguments input {_ _}.
Arguments output {_ _}.
Arguments add_edge2 [_] _ _ _ _.
Arguments add_vertex2 [_] _ _.
Arguments add_vlabel2 [_] _ _ _.
Arguments merge2 [_] _ _.

Notation IO := [set input;output].
Notation point G i o := (@Graph2 _ G i o).

Notation "G ∔ [ x , u , y ]" :=
  (add_edge2 G x y u) (at level 20, left associativity) : graph2_scope.
Notation "G ∔ a" :=
  (add_vertex2 G a%lbl) (at level 20, left associativity) : graph2_scope.
Notation "G [tst x <- a ]" :=
  (add_vlabel2 G x a%lbl) (at level 20, left associativity) : graph2_scope.
Notation merge2_seq G l := (merge2 G (eqv_clot l)).

Arguments iso2 {_}.
Arguments iso2prop {_}.
Arguments iso2_id {_ _}.

Infix "≃2" := iso2 (at level 79).
Infix "≃2p" := iso2prop (at level 79).
Hint Resolve iso2_id : core. (* so that by gets it... *)

Tactic Notation "Iso2" uconstr(f) :=
  match goal with |- ?F ≃2 ?G => refine (@Iso2 _ F G f _ _)=>// end.

(* temporary *)
Notation add_test := add_vlabel2 (only parsing).
Notation add_test_cong := add_vlabel2_iso' (only parsing).

(* used to move from letter-labeled graphs to term-labeled graphs (Lemma 5.3) *)
(* (i.e., the g2_pttdom construction is functorial) *)
Section h.
  Variables X Y: labels.
  Variable fv: lv X -> lv Y.
  Variable fe: le X -> le Y.
  Definition relabel (G: graph X): graph Y :=
    Graph (@endpoint _ G) (fv \o (@vlabel _ G)) (fe \o (@elabel _ G)).
  Hypothesis Hfv: Proper (eqv ==> eqv) fv.
  Hypothesis Hfe: forall b, Proper (eqv_ b ==> eqv_ b) fe.
  Global Instance relabel_iso: CProper (iso ==> iso) relabel.
  Proof.
    intros G H h. Iso h h.e h.d. split.
    - apply h.
    - intro. apply Hfv, h.
    - intro. apply Hfe, h.
  Defined.
  Lemma relabel_union F G: relabel (F ⊎ G) ≃ relabel F ⊎ relabel G.
  Proof. Iso bij_id bij_id xpred0. by split=>//; case. Defined.
  Hypothesis Hfvmon2: forall a b, fv (a ⊗ b)%lbl ≡ (fv a ⊗ fv b)%lbl.
  Hypothesis Hfvmon0: fv 1%lbl ≡ 1%lbl.
  Lemma relabel_merge F r: relabel (merge F r) ≃ merge (relabel F) r.
  Proof.
    Iso bij_id bij_id xpred0.
    split=>//= v.
    elim/big_rec2 : _ => [|i y1 y2 _ ->]; by [rewrite ?Hfvmon2|symmetry].
  Defined.
  Lemma relabel_add_edge F x y u: relabel (F ∔ [x, u, y]) ≃ relabel F ∔ [x, fe u, y].
  Proof.
    Iso bij_id bij_id xpred0. by split=>//; case.
  Defined.
  Lemma relabel_unit a: relabel (unit_graph a) ≃ unit_graph (fv a).
  Proof. Iso bij_id bij_id xpred0. by split. Defined.
  Lemma relabel_two a b: relabel (two_graph a b) ≃ two_graph (fv a) (fv b).
  Proof. etransitivity. apply relabel_union. apply union_iso; apply relabel_unit. Defined.
  Lemma relabel_edge a u b: relabel (edge_graph a u b) ≃ edge_graph (fv a) (fe u) (fv b).
  Proof. etransitivity. apply relabel_add_edge. by apply (add_edge_iso'' (h:=relabel_two _ _)). Defined.

  Definition relabel2 (G: graph2 X): graph2 Y :=
    point (relabel G) input output.
  Global Instance relabel2_iso: CProper (iso2 ==> iso2) relabel2.
  Proof. intros G H h. Iso2 (relabel_iso h); apply h. Defined.
  Lemma relabel2_dot (F G: graph2 X): relabel2 (F · G) ≃2 relabel2 F · relabel2 G.
  Proof.
    etransitivity. apply (iso_iso2 (relabel_merge _)).
    refine (merge_iso2 (relabel_union F G) _ _ _).
  Qed.
  Lemma relabel2_par (F G: graph2 X): relabel2 (F ∥ G) ≃2 relabel2 F ∥ relabel2 G.
  Proof.
    etransitivity. apply (iso_iso2 (relabel_merge _)).
    refine (merge_iso2 (relabel_union F G) _ _ _).
  Qed.
  Lemma relabel2_cnv (F: graph2 X): relabel2 (F°) ≃2 (relabel2 F)°.
  Proof. reflexivity. Qed.
  Lemma relabel2_dom (F: graph2 X): relabel2 (dom F) ≃2 dom (relabel2 F).
  Proof. reflexivity. Qed.
  Lemma relabel2_one: relabel2 1 ≃2 1.
  Proof.
    transitivity (unit_graph2 (fv 1%lbl)). Iso2 (relabel_unit _).
    apply unit_graph2_iso, Hfvmon0.
  Qed.
  Lemma relabel2_top: relabel2 (g2_top X) ≃2 g2_top Y.
  Proof.
    transitivity (two_graph2 (fv 1%lbl) (fv 1%lbl)). Iso2 (relabel_two _ _).
    apply two_graph2_iso; apply Hfvmon0.
  Qed.
  Lemma relabel2_var a: relabel2 (g2_var a) ≃2 g2_var (fe a).
  Proof.
    transitivity (edge_graph2 (fv 1%lbl) (fe a) (fv 1%lbl)). Iso2 (relabel_edge _ _ _).
    apply edge_graph2_iso=>//.
  Qed.
End h.