Require Export GraphReach.

Definition path_ex_plus (g : Graph) (x y : g) := exists x', E x x' = true /\ path_ex x' y.

Instance path_ex_plus_dec (g : Graph) (x y : g) : dec (path_ex_plus x y).
Proof.
  decide (exists x', x' el dom g /\ E x x' = true /\ path_ex x' y).
  - left; firstorder.
  - right; intros [x' [A B]]. apply n. exists x'; repeat split; auto. apply E_in_dom in A; intuition.   
Qed.

Lemma path_ex_plus_len (g : Graph) (x y : g) : path_ex_plus x y <-> exists xs, path xs x y /\ |xs| > 1.
Proof.
  split; intros.
  - destruct H as [x' [A [l B]]]. exists (x :: l). split; [econstructor; eauto|].
    destruct l; simpl in *; [|omega]. inv B.
  - destruct H as [[|u xs] [A B]]; inv A; simpl in *; [omega|].
    exists y0; split; auto. exists xs; auto.
Qed.


Lemma path_ex_plus_step (g : Graph) (x y z: g) : path_ex_plus x y -> E y z = true -> path_ex_plus x z.
Proof.
  intros [x' [A [xs B]]] C. exists x'; split; auto.
  exists (xs ++ [z]). eapply path_step; eauto.
Qed.

Definition g_trans (g : Graph) := forall g', elem g' g -> g_incl g' g.

Section TC.

Lemma subgraph_root_id (g: Graph) : subgraph (root g) = g.
Proof.
  unfold subgraph; destruct g; simpl; f_equal; auto. 
Qed.

Definition tc (g: Graph) := 
   G 
   (fun a b =>
     match a, b with
      |Some x, Some y => edgeRel x y
      |None, Some y => if (decision (path_ex_plus (root g) y)) then true else false
      |_, _ => false
    end) 
   (None :: (map (Some (A := g)) (dom g))) 
   (None).

Inductive elem_n : Graph -> Graph -> nat -> Prop :=
  |elem_O (g1 g2 : Graph) : bisim g1 g2 -> elem_n g1 g2 0
  |elem_S (g1 g2 g3 : Graph) n : elem g1 g2 -> elem_n g2 g3 n -> elem_n g1 g3 (S n).


Lemma elem_step (g1 g2 : Graph) (x y : g2) (n : nat): 
   elem_n g1 (subgraph y) n -> E x y = true -> elem_n g1 (subgraph x) (S n).
Proof.
   intros A. revert x. remember (subgraph y) as g_y. induction A; intros.
   - subst. apply elem_S with (g2 := subgraph x).
     + unfold elem. exists (subgraph y). split; auto. 
       apply in_children_iff. exists y; split. apply in_child_nodes_iff; auto. unfold subgraph; simpl; auto. 
     + constructor. apply bisimRefl.
   - subst. specialize (IHA eq_refl _ H0). econstructor. eauto. destruct H as [g' [B C]]. 
     apply in_children_iff in B as [u [B D]]. subst. auto.
Qed.

Lemma path_elem_n (g1 g2 : Graph) (r x : g2) :
    path_ex r x -> bisim g1 (subgraph x) -> exists n, elem_n g1 (subgraph r) n.
Proof.
  intros [l A]; revert g1. induction A; intros; simpl in *.
  - exists 0; constructor; auto.
  - specialize (IHA _ H0). destruct IHA as [n B]. exists (S n).
    eapply elem_step; eauto.
Qed.

Lemma path_plus_elem_n (g1 g2 : Graph) (r x : g2) : 
    path_ex_plus r x -> bisim g1 (subgraph x) -> exists n, n > 0 /\ elem_n g1 (subgraph r) n.
Proof.
  intros [x' [A [l B]]] C. assert (path_ex x' x). { exists l; auto. }
  destruct (path_elem_n H C) as [n D]. exists (S n); split; [omega|].
  eapply elem_step. eauto. auto.
Qed. 


Lemma E_subgraph (g : Graph) (v x y: g) : (@E (subgraph v) x y) = E x y.
Proof.
  unfold E; unfold subgraph; simpl. congruence.
Qed.


Lemma elem_n_path_ex_plus (g1 g2 : Graph) (n : nat) : 
         n > 0 -> elem_n g1 g2 n -> exists x : g2, path_ex_plus (root g2) x /\ bisim g1 (subgraph x).
Proof.
  revert g1 g2; induction n; intros; simpl in *; [omega|].
  decide (n = 0).
  - subst. inv H0. inv H5. apply bisim_equiv in H0. destruct H0 as [A1 A2].
    specialize (A1 _ H2). destruct A1 as [g' [A B]]. apply in_children_iff in A as [x [A C]].
    subst g'. exists x; split; auto.
    apply in_child_nodes_iff in A. exists x; split; auto. exists [x]; constructor. 
    apply E_in_dom in A; intuition.
  - assert (n > 0) by omega. inv H0. specialize (IHn _ _ H1 H6). destruct IHn as [x' [A B]].
    clear n0 H. apply bisim_equiv in B as [B C]. specialize (B _ H3). 
    destruct B as [g' [B1 B2]]. apply in_children_iff in B1 as [y [D1 D2]].
    apply in_child_nodes_iff in D1. subst g'. exists y; split; auto. simpl in D1.
    eapply path_ex_plus_step; eauto.
Qed.

Lemma elem_n_path(g1 g2 : Graph) (g2_root_cont : root g2 el dom g2) : 
      (exists n, elem_n g1 g2 n) <-> (exists x : g2, path_ex (root g2) x /\ bisim g1 (subgraph x)).
Proof.
  split; intros.
  - destruct H as [n A]. revert g2_root_cont A. revert g1 g2. induction n; intros; simpl in *.
     + inv A. exists (root g2); split. 
       * exists [root g2]. constructor. auto. 
       * rewrite subgraph_root_id. auto.
     + inv A. specialize (IHn _ _ g2_root_cont H3). destruct IHn as [x [A B]].
       apply bisim_equiv in B. destruct B as [B1 B2]. unfold g_incl in *. specialize (B1 _ H0).
       destruct B1 as [g' [C D]]. apply in_children_iff in C. destruct C as [y [C1 C2]].
       exists y. split.
       * apply in_child_nodes_iff in C1. destruct A as [l A]. exists (l ++ [y]). 
         unfold subgraph in *; simpl in *; eapply path_step; eauto.
       * subst g'. auto.
  - destruct H as [x [[l A] B]]. 
    cut (exists n, elem_n g1 (subgraph (root g2)) n).
    { intros. rewrite subgraph_root_id in H; auto. } apply path_elem_n with (r := root g2) in B; auto.
    exists l; auto.
Qed.

Lemma elem_n_bisim_inv (g1 g2 g3 : Graph) n : bisim g2 g3 -> elem_n g1 g2 n -> elem_n g1 g3 n.
Proof.
  revert g1 g2 g3. induction n; intros; simpl in *.
  - inv H0. constructor. eauto using bisimTrans.
  - assert (g_equiv g2 g3) by (apply bisim_equiv; auto). destruct H1 as [A B].
    inv H0. econstructor. eauto. eapply IHn; eauto.
Qed.

Lemma elem_n_r_el_dom (g1 g2 : Graph) n : 
   n > 0 -> elem_n g1 g2 n -> root g2 el dom g2.
Proof.
  revert g1 g2. induction n; intros; simpl in *.
  - omega.
  - inv H0. decide (n = 0).
    + subst.  inv H5. assert (elem g1 g2).
      { apply bisim_equiv in H0. destruct H0 as [A B]. apply A. auto. }
      unfold elem in H1. destruct H1 as [g' [A B]]. apply in_children_iff in A as [u [A C]].
      apply in_child_nodes_iff in A. apply E_in_dom in A; intuition.
    + assert (n > 0) by omega. eauto.       
Qed.

Lemma E_tc (g : Graph) (x : g) : E (root (tc g)) (Some x) = true <-> path_ex_plus (root g) x.
Proof.
  simpl; split; intros.
  - unfold tc in H; unfold E in H; simpl in H.
    decide ((@None g = @None g \/
            @None g el @map g (option g) (@Some g) (dom g)) /\
           (@None g = @Some g x \/
            @Some g x el @map g (option g) (@Some g) (dom g))); try congruence.
    decide (path_ex_plus (root g) x); congruence.
 - unfold tc; unfold E; simpl. 
   decide  ((@None g = @None g \/ @None g el @map g (option g) (@Some g) (dom g)) /\
       (@None g = @Some g x \/
        @Some g x el @map g (option g) (@Some g) (dom g))).
   + decide (path_ex_plus (root g) x); congruence. 
   + contradict n. split; [left; auto|right]. destruct H as [x' [A B]]. 
     apply in_map_iff. exists x; split; auto. apply path_reach_dom in B.
     apply reach_in_el_dom in B; auto.
Qed.

Lemma E_tc_Some (g : Graph) (x y : g) : E x y = (@E (tc g) (Some x) (Some y)).
Proof.
  unfold E; simpl. decide (x el dom g /\ y el dom g).
  - decide ((@None g = @Some g x \/
        @Some g x el @map g (option g) (@Some g) (dom g)) /\
       (@None g = @Some g y \/
        @Some g y el @map g (option g) (@Some g) (dom g))); try congruence.
    contradict n. split; right.
    + apply in_map_iff; exists x; intuition.
    + apply in_map_iff; exists y; intuition.
  - decide  ((None = Some x \/ Some x el map (Some (A:=g)) (dom g)) /\
      (None = Some y \/ Some y el map (Some (A:=g)) (dom g))); try congruence.
    destruct a as [[A|A][B|B]]; try congruence. 
    apply in_map_iff in A as [x' [A1 A2]]. injection A1; intros; subst.
    apply in_map_iff in B as [y' [B1 B2]]. injection B1; intros; subst.
    contradict n. split; auto.
Qed.

Lemma not_E_tc_None g a :  ~ (@E (tc g) a None) = true. 
Proof.
  intros C; unfold E in C; simpl in C. destruct a.
  - decide ((@None g = @Some g t \/
            @Some g t el @map g (option g) (@Some g) (dom g)) /\
           (@None g = @None g \/
            @None g el @map g (option g) (@Some g) (dom g))); congruence.
  - decide ((@None g = @None g \/
            @None g el @map g (option g) (@Some g) (dom g)) /\
           (@None g = @None g \/
            @None g el @map g (option g) (@Some g) (dom g))); congruence.
Qed.



Lemma tc_subgraph_bisim (g : Graph) (x : g) : bisim (subgraph (g:=g) x) (subgraph (g:=tc g) (Some x)).
Proof.
  exists (fun x b => 
     match b with 
     |Some y => eqb x y
     |None => false 
  end). split.
  - constructor; intros; split; intros.
    + destruct y; try congruence. rewrite eqb_iff in H; subst t.
      exists (Some x'); split. 
      * rewrite E_tc_Some in H0; auto.
      * rewrite eqb_iff; auto.
    + destruct y as [y|]; try congruence. rewrite eqb_iff in H; subst x0.
      destruct y' as [y'|]. 
      * exists (y'). split; [eauto using E_tc_Some|]. rewrite eqb_iff; auto.
      * contradict H0; intros C. rewrite E_subgraph in C. apply not_E_tc_None in C; tauto.
  - simpl. rewrite eqb_iff; auto. 
Qed.

Lemma tc_corr g1 g2 n : n > 0 -> elem_n g1 g2 n -> elem g1 (tc g2).
Proof.
  intros.
  assert (exists x : g2, path_ex_plus (root g2) x /\ bisim g1 (subgraph x)).
  { eapply elem_n_path_ex_plus; eauto. } 
  destruct H1 as [x [A B]]. unfold elem. exists (subgraph (g := tc g2) (Some x)); split; auto.
  - apply in_children_iff. exists (Some x). split.
    + apply E_tc in A; apply in_child_nodes_iff; auto.
    + auto.
  - rewrite B. apply tc_subgraph_bisim.
Qed.


Lemma tc_corr' g1 g2 : elem g1 (tc g2) -> exists n, n > 0 /\ elem_n g1 g2 n.
Proof.
  intros.
  assert (A : exists x : g2, path_ex_plus (root g2) x /\ bisim g1 (subgraph x)).
  { destruct H as [g [A B]]. apply in_children_iff in A as [x [C D]]. 
    apply in_child_nodes_iff in C. simpl in C. destruct x as [x|]. 
    - apply E_tc in C. subst; exists x; split; auto. rewrite B. 
      symmetry; apply tc_subgraph_bisim.  
    - apply not_E_tc_None in C; tauto. } 
  destruct A as [x [A B]]. cut (exists n, n > 0 /\ elem_n g1 (subgraph (root g2)) n).
  { intros. rewrite subgraph_root_id in H0. auto. } eapply path_plus_elem_n; eauto.
Qed.

Lemma tc_trans g : g_trans (tc g).
Proof.
  intros g1 A g2 B. apply tc_corr' in A as [n [A1 A2]]. 
  apply (tc_corr (n := S n)); [omega|]. 
  econstructor; eauto.
Qed.

Lemma tc_super_g g : g_incl g (tc g).
Proof.
  intros g' A. apply (tc_corr(n := 1)); [omega|]. 
  econstructor; eauto. econstructor; apply bisimRefl.
Qed.

Lemma tc_least_trans_super_g g : forall g', g_trans g' -> g_incl g g' -> g_incl (tc g) g'.
Proof.
  intros g' g'_trans g'_super_g h A. apply tc_corr' in A as [n [A1 A2]].
  revert h A1 A2. 
  induction n; intros; simpl in *; [omega|].
  destruct n; simpl in  *.
  - inv A2. inv H3. apply g'_super_g. eapply elem_bisim_inv_r; eauto.
  - inv A2. apply IHn in H3; [|omega]. apply g'_trans in H3. now apply H3.
Qed.

End TC.