Require Export Graphs.


Instance sum_eq_dec  {X : Type} {Y : Type} {x_eq_dec : eq_dec X} {y_eq_dec : eq_dec Y} : eq_dec (X + Y).
Proof.
  intros x y. destruct x, y.
  - decide (x = x0).
   + left. f_equal. auto.
   + right. congruence.
  - right; intros C. discriminate.
  - right; intros C; discriminate.
  - decide (y0 = y). 
   + left; f_equal; auto.
   + right; congruence.
Qed.


Section Children. 
Variable g : Graph.


Definition subgraph(x : g) := G (edgeRel (g:=g)) (dom g)  x.

Definition child_nodes := filter (fun x => E (root g) x = true) (dom g).

Lemma in_child_nodes_iff : forall x, x el child_nodes <-> E (root g) x = true.
Proof.
  unfold child_nodes. 
  intros; split; intros; [apply in_filter_iff in H | apply in_filter_iff]; intuition.
  destruct (E_in_dom H); auto.
Qed.

Definition children := map subgraph child_nodes.

Lemma in_children_iff g1 : g1 el children <-> exists x, x el child_nodes /\ g1 = subgraph x.
Proof.
  split; intros.
  - unfold children in H. assert (exists u, subgraph u = g1 /\ u el child_nodes).
    { apply in_map_iff. auto. } destruct H0 as [u [A B]]. exists u. split; auto.
  - unfold children. apply in_map_iff. destruct H as [u [A B]]. exists u; split; auto.
Qed.


End Children.

Instance subgraph_eq_dec {g: Graph} (x : g)  : eq_dec (subgraph x).
Proof.
  auto.
Qed.

Definition elem (g1 g2 : Graph) := 
     exists g3, g3 el children g2 /\ bisim g1 g3.

Lemma children_elem g1 g2 : g1 el children g2 -> elem g1 g2.
Proof.
  intros. exists g1. split; auto. reflexivity.
Qed.

Instance elem_dec (g1 g2 : Graph) : dec (elem g1 g2).
Proof.
  auto.
Qed.

Definition g_incl (g1 g2 : Graph) := forall g3, elem g3 g1 -> elem g3 g2.

Lemma g_incl_dec' (g1 g2 : Graph) : dec (forall g, g el children g1 -> elem g g2).
Proof. 
  auto.
Qed.

Lemma elem_bisim_inv_l g1 g2 g3 : elem g1 g2 -> bisim g1 g3 -> elem g3 g2.
Proof.
   intros. unfold elem in *. destruct H as [g [A B]]. exists g; split; auto.
   symmetry in H0. etransitivity; eauto.
Qed. 

Lemma g_incl_on_children g1 g2 : (forall g, g el children g1 -> elem g g2) <-> g_incl g1 g2.
Proof.
  split; intros.
  - unfold g_incl. intros. unfold elem in H0. destruct H0 as [g [A B]]. 
    specialize (H _ A). apply elem_bisim_inv_l with (g1 := g); [|symmetry]; eauto.
  - unfold g_incl in H. apply H. apply children_elem; auto.
Qed.

Instance g_incl_dec g1 g2 : dec (g_incl g1 g2).
Proof.
  destruct (g_incl_dec' g1 g2).
  - left. apply g_incl_on_children; auto.
  - right. intros C. apply n. apply g_incl_on_children. auto.
Qed.

Definition g_equiv g1 g2 := g_incl g1 g2 /\ g_incl g2 g1.

Lemma g_equiv_dec g1 g2 : dec (g_equiv g1 g2).
Proof.
  unfold g_equiv. auto. 
Qed.

Lemma bisim_incl g1 g2 : bisim g1 g2 -> g_incl g1 g2.
Proof.
  intros. apply g_incl_on_children. intros.
  unfold bisim in H. unfold elem. apply in_children_iff in H0.
  destruct H0 as [x [A B]]. apply in_child_nodes_iff in A. 
  destruct H as [p [C D]].  induction C. 
  pose (H0 := H).
  specialize (H0 _ _ D). destruct H0 as [I J]. specialize (I _ A). destruct I as [u [C1 C2]].
  exists (subgraph u). split.
  - apply in_children_iff.  exists u; split; auto. apply in_child_nodes_iff; auto.
  - subst g. exists p. split; auto.
    constructor. simpl. intros; split; intros; clear C1 C2 J A D.
    + specialize (H _ _ H0). destruct H as [A B]. specialize (A _ H1). 
      destruct A as [y' [C D]]. exists y'; auto. 
    + specialize (H _ _ H0). destruct H as [A B]. specialize (B _ H1). destruct B as [x' [C D]]. 
      exists x'; auto.
Qed.

Lemma bisim_equiv g1 g2 : bisim g1 g2 -> g_equiv g1 g2.
Proof.
  intros. split; apply bisim_incl; eauto using bisimSym.
Qed. 

Lemma subgraph_elem_E (g : Graph) (x x' : g) : E x x' = true -> elem (subgraph x') (subgraph x).
Proof.
  intros. apply children_elem. apply in_children_iff. 
  exists x'; split; auto. apply in_child_nodes_iff; simpl. auto. 
Qed.


Lemma trivial_dec (A : Prop) (A_dec : dec (A)) (s : bool) : 
    ((if decision (A) then s else false) = true) -> (s = true).
Proof.
  intros; decide A; congruence.
Qed.

Section Extensionality.

Variable g1 g2 : Graph.
Variable g1_g2_equiv : g_equiv g1 g2.

Lemma Ext : bisim g1 g2.
Proof.
  unfold bisim. exists (fun a b => if (decision (g_equiv (subgraph a) (subgraph b))) then true else false).
  split.
  - constructor. intros; split; intros. 
    + decide (g_equiv (subgraph (g:=g1) x) (subgraph (g:=g2) y)); try congruence.
      clear H. unfold g_equiv in g. destruct g as [A B].
      assert (elem (subgraph x') (subgraph x)). { 
        apply subgraph_elem_E. auto.
      } pose (C := A). unfold g_incl in C. specialize (C _ H). unfold elem in C.
        destruct C as [g3 [D1 D2]]. apply in_children_iff in D1. destruct D1 as [y' [E1 E2]]. subst g3.
        exists y'. split; auto.
         * apply in_child_nodes_iff in E1. auto.
         * decide (g_equiv (subgraph (g:=g1) x') (subgraph (g:=g2) y')); try congruence.
           contradict n. apply bisim_equiv. auto.
    + decide (g_equiv (subgraph (g:=g1) x) (subgraph (g:=g2) y)); try congruence.
      clear H. unfold g_equiv in g. destruct g as [A B].
      assert (elem (subgraph y') (subgraph y)). { 
        apply subgraph_elem_E. auto.
      } pose (C := B). unfold g_incl in C. specialize (C _ H). unfold elem in C.
        destruct C as [g3 [D1 D2]]. apply in_children_iff in D1. destruct D1 as [x' [E1 E2]]. subst g3.
        exists x'. split; auto.
         * apply in_child_nodes_iff in E1. auto.
         * decide (g_equiv (subgraph (g:=g1) x') (subgraph (g:=g2) y')); try congruence.
           contradict n. apply bisim_equiv. symmetry; auto. 
  - apply decision_done. auto.
Qed.

End Extensionality.


Lemma elem_bisim_inv_r g1 g2 g3 : elem g1 g2 -> bisim g2 g3 -> elem g1 g3.
Proof.
  intros. apply bisim_equiv in H0. unfold g_equiv in H0; unfold g_incl in *.
  destruct H0 as [A B]. apply A. auto.
Qed.

Lemma g_incl_bisim_inv_r g1 g2 g3 : g_incl g1 g2 -> bisim g2 g3 -> g_incl g1 g3.
Proof.
   intros; apply bisim_equiv in H0. unfold g_equiv in H0; unfold g_incl in *. destruct H0 as [A B].
   intros.  apply A. apply H. auto.
Qed. 


Inductive Unit := tt.
Instance Unit_eq_dec : eq_dec Unit.
Proof.
  intros. destruct x, y. left; reflexivity.
Qed.


Section Empty.

Definition empty : Graph :=  G (fun x y => false) [tt] tt.

Variable g : Graph.

Lemma not_E_empty x : not (E (root empty) x = true).
Proof.
  unfold E. intros C. apply trivial_dec in C. discriminate.
Qed.

Lemma Empty : not (elem g empty).
Proof.
  unfold elem; intros [x [A B]]. apply in_children_iff in A. 
  destruct A as [u [C D]]. apply in_child_nodes_iff in C.
  apply not_E_empty in C; auto.
Qed.

Lemma children_empty : children empty = [].
Proof.
  destruct (children empty) eqn:E; try reflexivity.
  assert (g0 el children empty). { rewrite E; auto. }
  apply in_children_iff in H. destruct H as [x [A B]]. apply in_child_nodes_iff in A.
  apply not_E_empty in A; tauto.
Qed.

End Empty.


Lemma bisim_empty_iff g: bisim g empty <-> (forall g', ~ (elem g' g)).
Proof.
  split; intros H.
  - apply bisim_equiv in H as [A B]. unfold g_incl in *. intros g' C.
    specialize (A _ C). now apply Empty in A.
  - apply Ext. split; intros h A.
    + contradict A; auto.
    + now apply Empty in A.
Qed.


Instance option_eq_dec {X : Type} {x_eq_dec : eq_dec X} : eq_dec (option X).
Proof.
 intros. destruct x, y; try (right; discriminate).
 - decide (x = x0); [left| right]; congruence.
 - left; auto.
Qed.


Section Adjunction.

Variable g1 g2 : Graph.
 

Definition adj := 
      G
      (fun a b => match a, b with 
        |None, Some d =>
           match d with
             |inl x => eqb x (root g1)
             |inr y => E (root g2) y
           end
        |Some c, Some d => 
           match c, d with
             |inl x, inl y => E x y
             |inr x, inr y => E x y
             |_, _ => false
           end
        
        |_, _ => false
      end) 
      (None :: (Some (inl (root g1))) :: (map (@Some (g1 + g2)) (map inl (dom g1) ++  map inr (dom g2))))
      None.


Lemma adj_edge_left (x x' : g1) : E x x' = true-> E (g:=adj) (Some (inl x)) (Some (inl x')) = true.
Proof.
   intros A. unfold E. 
   decide (and
         (@In (t adj) (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) x))
            (dom adj))
         (@In (t adj) (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) x'))
            (dom adj))); try congruence.
   - unfold adj; simpl; auto.
   - destruct n. apply E_in_dom in A. split; unfold adj; simpl.
     + right; right. apply in_map_iff. exists (inl x); split; try congruence. apply in_append.
       left; apply in_map_iff; exists x; intuition.
     + right; right; apply in_map_iff. exists (inl x'); split; try congruence. apply in_append.
       left; apply in_map_iff; exists x'; intuition.
Qed.

Lemma left_edge_adj (x x' : g1) : E (g:=adj) (Some (inl x)) (Some (inl x')) = true -> E x x' = true.
Proof.
  intros. unfold E in H. unfold adj in H; simpl in H; apply trivial_dec in H. auto.
Qed.

Lemma no_edge_left_right (x : g1) (y : g2) : ~ (E(g:=adj) (Some (inl x)) (Some (inr y)) = true).
Proof.
  intros A. unfold E in A. unfold adj in A; simpl in A; apply trivial_dec in A. discriminate.
Qed.

Lemma no_edge_right_left (x : g1) (y : g2) : ~ (E(g:=adj) (Some (inr y)) (Some (inl x)) = true).
Proof.
  intros A. unfold E in A; unfold adj in A; simpl in A; apply trivial_dec in A. discriminate.
Qed.

Lemma no_edge_to_root (x : option (g1 + g2)) : ~ (E(g:=adj) x None = true).
Proof.
  intros A. unfold E in A; unfold adj in A; simpl in A.
  apply trivial_dec in A. destruct x; discriminate. 
Qed.

Lemma edge_right (y y' : g2) : E (g:=adj) (Some (inr y)) (Some (inr y')) = true -> E y y' = true.
Proof.
  intros A. unfold E in A; unfold adj in A; simpl in A. apply trivial_dec in A. auto.
Qed.

Lemma edge_right_adj (y y' : g2) :   E y y' = true ->  E (g:=adj) (Some (inr y)) (Some (inr y')) = true.
Proof. 
  intros A; unfold E; unfold adj; simpl. decide  ((@None (g1 + g2) = @Some (g1 + g2) (@inr g1 g2 y) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) =
        @Some (g1 + g2) (@inr g1 g2 y) \/
        @Some (g1 + g2) (@inr g1 g2 y)
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2))) /\
       (@None (g1 + g2) = @Some (g1 + g2) (@inr g1 g2 y') \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) =
        @Some (g1 + g2) (@inr g1 g2 y') \/
        @Some (g1 + g2) (@inr g1 g2 y')
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2)))); try congruence. exfalso; apply n. split; right; right.
               - apply in_map_iff. exists  (inr y). split; auto. apply in_append. 
                 right; apply in_map_iff. exists y; split; auto. destruct (E_in_dom A); auto.
               - apply in_map_iff.  exists (inr y'). split; auto. apply in_append; right; apply in_map_iff.
                 exists y'; split; try congruence. destruct (E_in_dom A); auto.
Qed.


Lemma edge_root_right (y : g2) : E (g:=adj) None (Some (inr y)) = true -> E (root g2) y = true.
Proof.
  intros A; unfold E in A; unfold adj in A; simpl in A. apply trivial_dec in A. auto.
Qed.

Lemma edge_root_left_root : E (root adj) (Some (inl (root g1))) = true.
Proof.
  unfold E; unfold adj; simpl. decide  ((@None (g1 + g2) = @None (g1 + g2) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) = @None (g1 + g2) \/
        @None (g1 + g2)
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2))) /\
       (@None (g1 + g2) = @Some (g1 + g2) (@inl g1 g2 (root g1)) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) =
        @Some (g1 + g2) (@inl g1 g2 (root g1)) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1))
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2)))); try congruence.
               - apply eqb_iff; auto.
               - exfalso; apply n. split.
                 + left; auto.
                 + right. left. auto. 
Qed. 

Lemma edge_root_right_child y :  E (root g2) y = true -> E (root adj) (Some (inr y)) = true.
Proof.
  intros. unfold E; unfold adj; simpl. decide  ((@None (g1 + g2) = @None (g1 + g2) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) = @None (g1 + g2) \/
        @None (g1 + g2)
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2))) /\
       (@None (g1 + g2) = @Some (g1 + g2) (@inr g1 g2 y) \/
        @Some (g1 + g2) (@inl g1 g2 (root g1)) =
        @Some (g1 + g2) (@inr g1 g2 y) \/
        @Some (g1 + g2) (@inr g1 g2 y)
        el @map (g1 + g2) (option (g1 + g2)) (@Some (g1 + g2))
             (@map g1 (g1 + g2) (@inl g1 g2) (dom g1) ++
              @map g2 (g1 + g2) (@inr g1 g2) (dom g2)))); try congruence. exfalso; apply n.
              split.
              - left; auto.
              - right; right; apply in_map_iff. exists (inr y); split; auto. apply in_append.
                right; apply in_map_iff. exists y; split; auto. destruct (E_in_dom H); auto.
              
Qed.


Lemma subgraph_edgeRel (g : Graph) (x : g) : edgeRel (g := g) = edgeRel (g := subgraph x).
Proof.
  auto.
Qed.

Lemma E_subgraph_impl x y: @E adj (@Some (g1 + g2) (@inl g1 g2 x))
       (@Some (g1 + g2) (@inl g1 g2 y)) = true ->
@E (@subgraph adj (@Some (g1 + g2) (@inl g1 g2 (root g1))))
  (@Some (g1 + g2) (@inl g1 g2 x)) (@Some (g1 + g2) (@inl g1 g2 y)) = true.
Proof.
  intros. unfold E in H. destruct (decision
          (and
             (@In (t adj) (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) x))
                (dom adj))
             (@In (t adj) (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) y))
                (dom adj)))); try congruence.
   unfold E. destruct (decision  (and
         (@In
            (t
               (@subgraph adj
                  (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) (root g1)))))
            (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) x))
            (dom
               (@subgraph adj
                  (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) (root g1))))))
         (@In
            (t
               (@subgraph adj
                  (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) (root g1)))))
            (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) y))
            (dom
               (@subgraph adj
                  (@Some (sum (t g1) (t g2)) (@inl (t g1) (t g2) (root g1))))))) ); try congruence; auto.
Qed.

Lemma E_subgraph_impl' x t : @E (@subgraph adj (@Some (g1 + g2) (@inl g1 g2 (root g1))))
       (@Some (g1 + g2) (@inl g1 g2 x)) (@Some (g1 + g2) (@inl g1 g2 t)) =  true 
     -> @E adj (@Some (g1 + g2) (@inl g1 g2 x)) (@Some (g1 + g2) (@inl g1 g2 t)) = true.
Proof.
   intros. unfold E in H. destruct (decision  (and
             (@In
                (Graphs.t
                   (@subgraph adj
                      (@Some (sum (Graphs.t g1) (Graphs.t g2))
                         (@inl (Graphs.t g1) (Graphs.t g2) (root g1)))))
                (@Some (sum (Graphs.t g1) (Graphs.t g2))
                   (@inl (Graphs.t g1) (Graphs.t g2) x))
                (dom
                   (@subgraph adj
                      (@Some (sum (Graphs.t g1) (Graphs.t g2))
                         (@inl (Graphs.t g1) (Graphs.t g2) (root g1))))))
             (@In
                (Graphs.t
                   (@subgraph adj
                      (@Some (sum (Graphs.t g1) (Graphs.t g2))
                         (@inl (Graphs.t g1) (Graphs.t g2) (root g1)))))
                (@Some (sum (Graphs.t g1) (Graphs.t g2))
                   (@inl (Graphs.t g1) (Graphs.t g2) t))
                (dom
                   (@subgraph adj
                      (@Some (sum (Graphs.t g1) (Graphs.t g2))
                         (@inl (Graphs.t g1) (Graphs.t g2) (root g1)))))))); try congruence.
        unfold E. destruct (decision  (and
         (@In (Graphs.t adj)
            (@Some (sum (Graphs.t g1) (Graphs.t g2))
               (@inl (Graphs.t g1) (Graphs.t g2) x)) (dom adj))
         (@In (Graphs.t adj)
            (@Some (sum (Graphs.t g1) (Graphs.t g2))
               (@inl (Graphs.t g1) (Graphs.t g2) t)) (dom adj)))); try congruence; auto.
Qed.

Lemma E_subgraph_x_y (x y u : adj) : @E (@subgraph adj u) x y =  true 
     -> @E adj x y = true.
Proof.
  intros.  unfold E in H. destruct (decision 
          (and (@In (t (@subgraph adj u)) x (dom (@subgraph adj u)))
             (@In (t (@subgraph adj u)) y (dom (@subgraph adj u))))); try congruence.
           unfold E. destruct (decision (and (@In (t adj) x (dom adj)) (@In (t adj) y (dom adj))));
           try congruence; auto.
Qed.

Lemma E_subgraph_x_y_adj (x y u : adj) : @E adj x y =  true 
     -> @E (@subgraph adj u)  x y = true.
Proof.
  intros. unfold E in H. destruct (@decision (and (@In (t adj) x (dom adj)) (@In (t adj) y (dom adj)))); try congruence.
  unfold E. destruct (  @decision
      (and (@In (t (@subgraph adj u)) x (dom (@subgraph adj u)))
         (@In (t (@subgraph adj u)) y (dom (@subgraph adj u))))); try congruence; auto.
Qed.

Lemma bisim_left_root : bisim g1 (subgraph (g:=adj) (Some (inl (root g1)))).
Proof. 
   exists (fun x y => eqb (Some (inl x)) y). split; [constructor|]; intros.
   -split; intros.
    + rewrite eqb_iff in H. subst y. exists (Some (inl x')); split; [|apply eqb_iff; auto].
      apply adj_edge_left in H0. auto.
    + rewrite eqb_iff in H. subst y. 
     {destruct y'.
       - destruct s. 
         + exists t. split; [| apply eqb_iff; auto]. apply left_edge_adj. auto.
         + exfalso. apply E_subgraph_x_y in H0. apply (no_edge_left_right H0). 
       - exfalso. apply E_subgraph_x_y in H0. apply (no_edge_to_root H0). }
  - rewrite eqb_iff. auto.
Qed.


Lemma bisim_right_child b :  bisim (subgraph (g:=g2) b) (subgraph (g:=adj) (Some (inr b))).
Proof.
  exists (fun x y => eqb (Some (inr x)) y ). split; [constructor|]; intros.
   - split; intros.
      + rewrite eqb_iff in H. subst y. exists (Some (inr x')). split; [|apply eqb_iff; auto].
        apply E_subgraph_x_y_adj.
        apply edge_right_adj. auto.
      + rewrite eqb_iff in H. subst y. destruct y'.
        * {destruct s.
          - exfalso. apply (no_edge_right_left H0).
          - apply edge_right in H0. exists t. split; auto. apply eqb_iff; auto.
          }
        * contradict H0. intros C. apply (no_edge_to_root C). 
  - apply eqb_iff. auto. 
Qed.




Variable g : Graph.
Lemma Adj : elem g  adj <-> bisim g g1 \/ elem g g2.
Proof.
  split; intros.
  - destruct H as [x [A B]]. apply in_children_iff in A. destruct A as [u [A A2]].  apply in_child_nodes_iff in A. 
    assert ((exists a, u = Some (inl a)) \/ (exists b, u = Some (inr b))).
    { unfold adj in A. simpl in A. destruct x.
      - unfold E in A. simpl in A. apply trivial_dec in A. 
        destruct u. { destruct s.  
        - left; exists t0; auto. 
        - right. exists t0; auto. 
        } discriminate. }
    destruct H as [[a C]|[b C]]; subst x. 
    + unfold E in A. unfold adj in A. simpl in A. apply trivial_dec in A. destruct u; try discriminate.
      destruct s. 
      * rewrite eqb_iff in A. subst t. left. 
        rewrite B. symmetry; apply bisim_left_root.
      * discriminate.
   + right. exists (subgraph b). split; auto. { apply in_children_iff. exists b. split; auto. 
      apply in_child_nodes_iff. subst u. apply edge_root_right in A. auto. } subst u. 
      rewrite B. symmetry; apply bisim_right_child.
  - destruct H.
    + exists (subgraph (g:=adj) (Some (inl (root g1)))). split.
      * apply in_children_iff. exists (Some (inl (root g1))). split; auto.
        apply in_child_nodes_iff. apply edge_root_left_root.
      * etransitivity; eauto. apply bisim_left_root.
    + destruct H as [y [A B]]. 
      unfold elem. apply in_children_iff in A. destruct A as [n [A C]]. exists (subgraph (g := adj) (Some (inr n))).
      split.
      * apply in_children_iff. exists (Some (inr n)). split; auto. apply in_child_nodes_iff in A. 
        apply in_child_nodes_iff. apply edge_root_right_child. auto.
      * rewrite B; subst; apply bisim_right_child.
Qed.


End Adjunction.

Fixpoint list_to_graph (xs : list Graph) :=
  match xs with
  |[] => empty
  |(x :: xs) => adj x (list_to_graph xs)
  end.

Lemma elem_list_to_graph xs g : elem g (list_to_graph xs) <-> exists x, x el xs /\ bisim g x.
Proof.
  revert g; induction xs; intros g; split; intros H; simpl in *.
  - apply Empty in H. tauto.
  - exfalso. destruct H; tauto.
  - apply Adj in H. destruct H.
    + exists a; auto.
    + specialize (IHxs g). destruct IHxs as [A B]. specialize (A H). destruct A as [x [C D]].
      exists x; auto.
  - apply Adj. destruct H as [x [[A|A] B]].
    + subst a. left. auto.
    + right. apply IHxs. exists x. split; auto.
Qed.


Lemma elem_list_graph_bisim g : bisim g (list_to_graph (children g)).
Proof.
  apply Ext. split.
  - intros g0 A. apply elem_list_to_graph. unfold elem in A. destruct A as [g2 [B C]]. exists g2.
    split; auto. 
  - intros g0 A. apply -> elem_list_to_graph in A. destruct A as [x [A B]]. exists x; split; auto.
Qed.


Definition list_g_incl xs ys := forall g, g el xs -> exists g', g' el ys /\ bisim g g'.
Definition list_g_equiv xs ys := list_g_incl xs ys /\ list_g_incl ys xs.

Lemma list_graph_equiv xs : list_g_equiv (children (list_to_graph xs)) xs.
Proof.
  induction xs; split; intros; simpl in *.
  - intros x A. rewrite children_empty in A. simpl in A; tauto.
  - intros x A. simpl in A; tauto.
  - intros x A; simpl in A. assert (elem x (adj a (list_to_graph xs))).
    { apply children_elem. auto. } apply Adj in H. destruct H.
     + exists a; split; auto.
     + destruct IHxs as [B C]. unfold elem in H.
       destruct H as [g [D E]]. specialize (B _ D). destruct B as [g' [B1 B2]].
       exists g'; split; auto. rewrite <- B2; auto.
  - intros x [A|A]; simpl in *. 
    + subst a. exists (subgraph (g:=adj x (list_to_graph xs)) (Some (inl (root x)))); split.
      * apply in_children_iff. exists (Some (inl (root x))); split; auto. apply in_child_nodes_iff.
        apply edge_root_left_root. 
      * apply bisim_left_root.
    + destruct IHxs as [B1 B2]. specialize (B2 _ A). destruct B2 as [g' [C D]]. 
      apply in_children_iff in C.  destruct C as [u [C1 C2]]. 
      apply in_child_nodes_iff in C1. exists (subgraph (g := adj a (list_to_graph xs)) (Some (inr u))).
      split.
      * apply in_children_iff. exists (Some (inr u)); split; auto. apply in_child_nodes_iff.
        apply edge_root_right_child . auto. 
      * rewrite D; subst. apply bisim_right_child.       
Qed.


Section UPair.

Variable g1 g2 : Graph.

Definition upair := list_to_graph [g1; g2].

Lemma UPair : forall g, elem g upair <-> bisim g g1 \/ bisim g g2.
Proof.
  unfold upair; intros; split; intros.
  - apply -> elem_list_to_graph in H. destruct H as [x [[A|[A|A]] B]]; simpl in *; try tauto; subst; auto.
  - apply elem_list_to_graph. destruct H; [exists g1|exists g2]; intuition.
Qed.

End UPair.

Section Sing.

Variable g1 : Graph.

Definition sing := upair g1 g1.

Lemma Sing : forall g, elem g sing <-> bisim g g1.
Proof.
  unfold sing; intros; split; intros.
  - apply UPair in H; intuition.
  - apply UPair; auto.
Qed.

End Sing.

Definition flatten (X : Type) (xs : list (list X)) := flat_map id xs.

Lemma in_flatten_iff (X : Type) (xs : list (list X)) : 
   forall x, x el flatten xs <-> exists ys, ys el xs /\ x el ys.
Proof.
  unfold flatten. intros. apply in_flat_map.
Qed.

Section Union.

Variable g1 : Graph.

Definition union := list_to_graph (flatten (map children (children g1))).

Lemma Union : forall g, elem g union <-> exists g', elem g' g1 /\ elem g g'.
Proof.
   intros; unfold union; split; intros.
    - apply -> elem_list_to_graph in H. destruct H as [x [A B]].
      apply in_flatten_iff in A. destruct A as [l [A1 A2]]. apply in_map_iff in A1.
      destruct A1 as [y [C D]]. exists y. split.
      + apply children_elem in D; auto.
      + exists x. split; auto. subst l. auto.
   - apply elem_list_to_graph. destruct H as [g' [A B]]. 
     unfold elem in A, B. destruct A as [x [A1 A2]], B as [y [B1 B2]]. 
     assert (g_equiv g' x). { apply bisim_equiv. auto. } unfold g_equiv in H.
     destruct H as [D1 D2]. assert (elem y x). { apply D1.  apply children_elem in B1; auto. }
     destruct H as [u [C1 C2]]. exists u. split; eauto using bisimTrans.
     apply in_flatten_iff. exists (children x); split; auto. apply in_map_iff. exists x; split; auto.
Qed.

End Union.

Definition ext_bisim P := forall (g1 g2 : Graph), bisim g1 g2 -> (P g1 <-> P g2).

Section Separation.

Variable M : Graph.

Variable P : Graph -> Prop.
Context {p_dec : forall M, dec (P M)}.
Variable p_ext : ext_bisim P.

Definition sep := list_to_graph (filter P (children M)).

Lemma Sep : forall N, elem N sep <-> exists M', elem M' M /\ P M' /\ bisim N M'.
Proof.
  intros; unfold sep; split; intros.
  - apply -> elem_list_to_graph in H. destruct H as [M' [A B]].
    apply in_filter_iff in A; destruct A as [A C].
    exists M'; split; [|split]; eauto using children_elem. 
  - apply elem_list_to_graph. destruct H as [M' [A1 [A2 A3]]].
    unfold elem in A1. destruct A1 as [x [B1 B2]]. exists x; split; eauto using bisimTrans.
    apply in_filter_iff. split; auto. eapply p_ext. symmetry; eauto. auto.
Qed.


End Separation.

Arguments sep M P {p_dec}.

Section Rep.

Variable M : Graph.
Variable f : Graph -> Graph.

Definition rep := list_to_graph (map f (children M)).

Variable f_ext : forall N M, bisim N M -> bisim (f N) (f M).

Lemma Rep : forall N, elem N rep <-> exists M', elem M' M /\ bisim N (f M').
Proof.
  unfold rep; intros; split; intros.
  - apply -> elem_list_to_graph in H. destruct H as [x [A B]].
    apply in_map_iff in A. destruct A as [M' [C D]].
    exists M'; split.
    + apply children_elem; auto. 
    + subst. auto.
  - apply elem_list_to_graph. destruct H as [M' [A B]].
    destruct A as [x [C D]]. exists (f x). split.
    + apply in_map_iff. exists x; split; auto.
    + eauto using bisimTrans.
Qed.

End Rep.

Lemma filter_in_power (X : Type) (xs : list X) (p : X -> Prop) {p_dec : forall x, dec (p x)} : 
      filter p xs el power xs.
Proof.
  induction xs; simpl in *; auto.
  decide (p a).
  - apply in_append. right. apply in_map_iff. exists (filter p xs). split; auto.
  - apply in_append; left. auto. 
Qed.

Section Power.

Variable M : Graph.

Definition pow := list_to_graph (map list_to_graph (power (children M))).

Lemma Pow : forall N, elem N pow <-> g_incl N M.
Proof.
  intros; unfold pow; split; intros.
  - apply -> elem_list_to_graph in H. destruct H as [x [A B]].
    apply in_map_iff in A. destruct A as [l [A C]].
    apply power_incl in C. apply g_incl_on_children. 
    intros. subst. unfold elem. apply bisim_equiv in B. destruct B as [B1 B2].
    assert (elem g N) by (eauto using children_elem).
    specialize (B1 _ H0). apply -> elem_list_to_graph in B1.
    destruct B1 as [y [D E]]. specialize (C _ D). exists y; split; auto.
  - apply elem_list_to_graph. unfold g_incl in H. 
     pose (l := filter (fun M' : Graph => elem M' N) (children M)).
     assert (l el power (children M)). { apply filter_in_power. }
     exists (list_to_graph l). split.
     + apply in_map_iff. exists l; split; auto.
     + apply Ext. split.
       * intros g A. assert (elem g M). { apply H; auto. } subst l. 
         apply elem_list_to_graph. destruct H1 as [x [B C]]. exists x; split; auto.
         apply in_filter_iff. split; auto. eapply elem_bisim_inv_l; eauto.
       * intros g A. subst l. apply -> elem_list_to_graph in A. destruct A as [x [A B]].
         apply in_filter_iff in A. destruct A as [A C]. eapply elem_bisim_inv_l; eauto using bisimSym.
Qed.

End Power.





