Require Export GraphNat.

Section Reach.

Variable g : Graph. 

Lemma path_endpoints_dom x y (A : path_ex x y) : x el dom g /\ y el dom g.
Proof.
  destruct A as [l A]; induction A.
  - split; auto.
  - split; intuition. apply E_in_dom in H; intuition.
Qed.

Fixpoint reach_in (x y : g) n :=
 match n with
    |O => if (decision (x el dom g /\ x = y)) then true else false
    |S n => if reach_in x y n then true 
            else if (decision (exists x', x' el dom g /\ E x x' = true /\ reach_in x' y n = true)) then true else false
  end.

Lemma reach_refl (x : g) : x el dom g -> reach_in x x 0 = true.
Proof.
  simpl. intros; decide(x el dom g /\ x = x); try congruence. contradict n; split; auto. 
Qed.

Lemma reach_child_nodes (x y : g) : E x y = true -> reach_in x y 1 = true.
Proof.
  intros. simpl. decide (x el dom g /\ x = y); try congruence.
  rewrite decision_done; auto. assert (y el dom g) by (apply E_in_dom in H; intuition).
  exists y; repeat split; auto. apply decision_done; auto. 
Qed.

Lemma reach_in_char x y n : 
      reach_in x y (S n) = true -> x = y \/ exists z, E x z = true /\ reach_in z y n = true.
Proof.
   revert x. induction n; intros; simpl in *. 
   - decide (x = y); [left; auto|].
     decide (x el dom g /\ x = y).
     + exfalso; intuition.
     + decide (exists x' : g, x' el dom g /\ E x x' = true /\
             (if decision (x' el dom g /\ x' = y) then true else false) = true); try congruence. 
       destruct e as [x' [A B]]. right; exists x'. auto.
   - decide (x = y); [left; congruence|]. right. 
     destruct (reach_in x y n) eqn:E; try congruence.
      + destruct (IHn x) as [A | [z [A B]]]; try congruence.  {rewrite E. auto. }
        exists z.  split; auto. rewrite B. auto.
      + decide  (exists x' : g,
                x' el dom g /\ Graphs.E x x' = true /\ reach_in x' y n = true); try congruence.
         { destruct e as [x' [A [B C]]]. exists x'. split; auto. rewrite C. auto. }
     decide (exists x' : g,
             x' el dom g /\
             Graphs.E x x' = true /\
             (if reach_in x' y n
              then true
              else
               if decision
                    (exists x'0 : g,
                       x'0 el dom g /\
                       Graphs.E x' x'0 = true /\ reach_in x'0 y n = true)
               then true
               else false) = true). 
               * destruct e as [x' [A [B C]]]; exists x'; split; auto.
               * discriminate.
Qed.

Lemma reach_in_char_O x y : reach_in x y 0 = true -> x el dom g /\ x = y.
Proof.
  intros. simpl in *. decide (x el dom g /\ x = y); congruence.
Qed.

Lemma path_ex_step (x y z : g) : path_ex y z -> E x y = true -> path_ex x z.
Proof.
   intros [A B]; revert x; induction B; intros; simpl in *; unfold path_ex.
   - exists [x0; x]. eapply Path_S; eauto. constructor; auto.
   - destruct (IHB _ H) as [l C]. exists (x0 :: l). eapply Path_S; eauto.
Qed.
    
Lemma reach_in_el_dom (x y : g) n : reach_in x y n = true -> y el dom g.
Proof.
  revert x y; induction n; intros; simpl in *.
  - decide (x el dom g /\ x = y); intuition; congruence. 
  - destruct (reach_in x y n) eqn:E; eauto.
    decide  (exists x' : g,
             x' el dom g /\ Graphs.E x x' = true /\ reach_in x' y n = true); try congruence.
    destruct e as [x' [A [B C]]]. eauto.
Qed.

Lemma reach_path x y n : reach_in x y n = true -> path_ex x y.
Proof.
  revert x; induction n; intros x A.
  - apply reach_in_char_O in A as [A B]; subst. exists [y]; apply Path_O; auto.
  - assert (y el dom g) by (apply (reach_in_el_dom A)).
    apply reach_in_char in A; auto. simpl in *. decide (x = y); subst.
    + exists [y]; apply Path_O; auto.
    + destruct A; [congruence|]. destruct H0 as [z [A B]].
      eapply path_ex_step; eauto.
Qed.

Lemma reach_one_more_step x y n : reach_in x y n = true -> reach_in x y (S n) = true.
Proof.
  revert x y; induction n; intros; simpl in *.
  - decide  (x el dom g /\ x = y); congruence.
  - destruct (reach_in x y n) eqn:F; try congruence. 
    decide (exists x' : g, x' el dom g /\ E x x' = true /\ reach_in x' y n = true); congruence.
Qed.

Lemma reach_more_steps x y n m : reach_in x y n = true -> m > n -> reach_in x y m = true.
Proof.
  revert x y n; induction m; intros; simpl in *.
  - omega.
  - decide (m = n).
    + subst; rewrite H. auto.
    + assert (m > n) by omega. specialize (IHm _ _ _ H H1). rewrite IHm. auto.
Qed.

Lemma reach_refl_n x n : x el dom g -> reach_in x x n = true.
Proof.
  intros; destruct n.
  - apply reach_refl. auto.
  - eapply reach_more_steps. eapply reach_refl; eauto. omega.
Qed.

Lemma reach_step_begin x y z n : reach_in y z n = true -> E x y = true -> reach_in x z (S n) = true.
Proof.
  intros; simpl. destruct (reach_in x z n) eqn:F; try congruence.
  rewrite decision_done; auto. exists y; repeat split; auto. apply E_in_dom in H0; intuition.
Qed.

Lemma path_step A (x y z : g) : path A x y -> E y z = true -> path (A ++ [z]) x z.
Proof.
  intros B; revert z. induction B; intros u C; simpl in *.
  - apply Path_S with (y := u); eauto using path; [apply Path_O|]; auto. destruct (E_in_dom C); auto. 
  - eapply Path_S.
   + apply IHB. auto.
   + destruct B; now firstorder.
Qed. 

Lemma path_reach_in_n x y A: path A x y -> reach_in x y (length A) = true.
Proof.
  induction 1.
  - apply reach_refl_n. auto.
  - eapply reach_step_begin; eauto.
Qed.

Lemma path_begin (x y z : g) A : path (x ::  A) y z -> x = y.
Proof.
  intros B. remember (x :: A) as l.  induction B; simpl in *.
  - injection Heql; subst; auto.
  - injection Heql; firstorder.
Qed.

Definition remove_until (x : g) := 
   fix f A := match A with
    |[] => []
    |(y :: rs) => if (decision (x = y)) then y :: rs else f rs
   end.

Lemma remove_until_starts_with x A : x el A -> exists B, remove_until x A = x :: B.
Proof.
  revert x. induction A; intros x C; simpl in *; try tauto. 
  decide (x = a); destruct C; try congruence.
  - subst a. clear e. exists A; auto.
  - subst a. exists A; auto.
  - apply IHA. auto.
Qed. 

Lemma remove_until_path A x y z :
  path A y z -> x el A -> path (remove_until x A) x z.
Proof.
  induction 1; intros; simpl in *.
  - decide (x = x0); subst; destruct H0; try congruence; try tauto. 
    apply Path_O; auto.
  - decide (x = x0).
    + subst. eapply Path_S; eauto.
    + destruct H1; try congruence. apply IHpath; auto.
Qed.


Lemma remove_until_smaller d A : |remove_until d A| <= |A|.
Proof.
  induction A; simpl in *; try omega. 
  decide (d = a).
  - subst a. simpl. omega.
  - firstorder.
Qed. 

Fixpoint norm_path xs :=
   match xs with
   | [] => []
   | (x :: xs) => 
     let ys := norm_path xs in 
       if (decision (x el ys)) then remove_until x ys else x :: ys
   end.

Lemma norm_path_corr xs x y : path xs x y -> path (norm_path xs) x y.
Proof with eauto.
  induction 1; simpl. constructor. auto. decide (x el norm_path A)... eapply remove_until_path...
  eapply Path_S...
Qed.

Lemma dupfree_incl_size (X : Type) {x_eq_dec : eq_dec X} (xs ys : list X) : 
            dupfree xs -> xs <<= ys -> |xs| <= |ys|.
Proof.
  intros A; revert ys; induction A; intros; simpl in *; [omega|].
  assert (x el ys). { apply H0. auto. }
  assert (|A| <= |(rem ys x)|). { apply IHA. intros y B. apply in_rem_iff. split; auto. congruence. }
  assert (|(x :: (rem ys x))| <= |ys|). { simpl. cut (|rem ys x| < |ys|); try omega. apply len_rem. auto. }
  assert (|(x :: A)| <= |(x :: rem ys x)|). {simpl; omega. }
  simpl in *; omega.
Qed.

Lemma remove_until_dupfree x xs : dupfree xs -> dupfree (remove_until x xs).
Proof.
  intros A; revert x; induction A; intros; simpl in *; [constructor|].
  decide (x0 = x).
  - subst. constructor; auto.
  - auto. 
Qed.

Lemma dupfree_norm_path xs : dupfree (norm_path xs).
Proof.
  induction xs; simpl in *.
  - constructor.
  - decide (a el norm_path xs). 
    + apply remove_until_dupfree. auto.
    + constructor; auto.
Qed.

Lemma remove_until_incl x xs : remove_until x xs <<= xs.
Proof.
  revert x; induction xs; intros; simpl; [|decide (x = a)]; auto.
Qed.

Lemma norm_path_incl xs : norm_path xs <<= xs.
Proof with eauto using remove_until_incl.
  induction xs; simpl; auto.
  decide (a el norm_path xs)... etransitivity...
Qed.


Lemma norm_path_len xs ys : xs <<= ys -> |norm_path xs| <= |ys|.
Proof.
  revert ys; induction xs; simpl; intros; [omega|]. decide (a el norm_path xs); simpl.
  - etransitivity. apply remove_until_smaller. apply IHxs. intros x elxs. apply H. simpl. tauto.
  - replace (S (|norm_path xs |)) with (|(a :: norm_path xs)|) by (simpl; omega).
    apply dupfree_incl_size; auto. 
    + constructor; auto. apply dupfree_norm_path.
    + etransitivity; try eapply H. cut (norm_path xs <<= xs); try auto. 
      apply norm_path_incl.
Qed.

Lemma path_dom_incl A x y : path A x y -> A <<= dom g.
Proof.
  induction 1.
  - auto.
  - intros u [B|B]; auto. subst. apply E_in_dom in H0; intuition.
Qed. 

Lemma path_reach_dom x y : path_ex x y <-> reach_in x y (|dom g|) = true.
Proof.
  split; intros.
  - destruct H as [A B]. assert (path (norm_path A) x y). { apply norm_path_corr. auto. }
    assert (|norm_path A| <= |dom g|). { apply norm_path_len. eapply path_dom_incl; eauto. }
    decide (|norm_path A| = |dom g|). 
    + rewrite <- e. apply path_reach_in_n. auto.
    + assert (|dom g| > |norm_path A|) by omega. eapply reach_more_steps. 
      eapply path_reach_in_n. eauto. auto.
  - eapply reach_path; eauto.
Qed.


End Reach.


Instance path_ex_dec {g : Graph} (x y : g) : dec (path_ex x y).
Proof.
  destruct (reach_in x y (|dom g|)) eqn:E.
  - left; apply path_reach_dom; auto.
  - right; intros C. apply path_reach_dom in C; congruence. 
Qed.

