Require Export GraphAxioms.

Definition reorder (g : Graph) := 
   G (edgeRel (g := g)) (root g :: (rem (undup (dom g)) (root g))) (root g).


Lemma reorder_dom_equi_root_contained g ( A: root g el dom g) : dom g === dom (reorder g).
Proof. 
  unfold reorder; simpl.
  split; intros x B; simpl in *.
   - decide (x = root g); [left; auto|].
     right. apply in_rem_iff. split; auto. apply undup_id_equi. auto.
   - decide (x = root g); [subst; auto|]. 
     destruct B; [congruence|]. apply in_rem_iff in H as [B C].
     apply undup_id_equi in B; auto.
Qed.

Lemma no_root_bisim_empty (g : Graph) :  (~ (root g el dom g)) -> bisim g empty.
Proof.
  intros. exists (fun x y => if (decision (x = root g /\ y = root empty)) then true else false ).
    split.
    + constructor; split; intros. 
      * decide (x = root g /\ y = root empty); try congruence. unfold E in H0.  
        apply E_in_dom in H1. destruct a; subst x. destruct H1; exfalso; congruence.
      * exfalso; unfold empty in H1. unfold E in H1; simpl in H1. apply trivial_dec in H1; discriminate.
    + decide (root g = root g /\ root empty = root empty); try congruence. contradict n; split; congruence.
Qed.
 

Lemma with_root_bisim_reorder (g : Graph) : (root g el dom g) -> bisim g (reorder g).
Proof.
  intros A; eapply bisimIsom.
    { unfold iso. exists (fun x => x). split; intros; reflexivity. }
    unfold mutated. split; [| split]; intros.
    - simpl. split; intros x B; simpl in *.
       + decide (x = root g); [subst; left; auto|]. right. apply in_rem_iff; split; auto.
          apply undup_id_equi. apply in_map_iff in B as [y [C D]]. subst; auto.
       + destruct B as [B|B].
         * subst. apply in_map_iff; exists (root g); auto.
         * apply in_rem_iff in B as [B C]. apply in_map_iff; exists x; split; auto.
           eapply undup_id_equi; auto.
   - reflexivity.
   - split; intros; simpl in *.
     + unfold reorder. unfold E in *. simpl in *.
       decide  ((root g = x \/ x el rem (undup (dom g)) (root g)) /\
       (root g = y \/ y el rem (undup (dom g)) (root g))).
       *  decide (x el dom g /\ y el dom g); congruence.
       * contradict n. decide (x el dom g /\ y el dom g); try congruence.
         destruct a; split.
         { decide (x = root g); [subst; left; auto|]. right. 
           apply in_rem_iff; split; auto. apply undup_id_equi; auto. }
         { decide (y = root g); [subst; left; auto|]. right. 
           apply in_rem_iff; split; auto. apply undup_id_equi; auto. }
     + unfold reorder in *; unfold E in *; simpl in *. 
       decide  ((root g = x \/ x el rem (undup (dom g)) (root g)) /\
           (root g = y \/ y el rem (undup (dom g)) (root g))); try congruence.
       decide (x el dom g /\ y el dom g); try congruence. contradict n. 
       destruct a as [[B|B][C|C]]; split; subst; try congruence.
        * apply in_rem_iff in C as [C D]. eapply undup_id_equi; auto.
        * apply in_rem_iff in B as [B C]; eapply undup_id_equi; auto.
        * apply in_rem_iff in B as [B D]. eapply undup_id_equi; auto.
        * apply in_rem_iff in C as [C D]. eapply undup_id_equi; auto.
Qed.

Lemma empty_or_reorder : forall (g : Graph), {bisim g empty} + {bisim g (reorder g)}.
Proof.
  intros g. decide (root g el dom g).
  - right. eapply with_root_bisim_reorder. auto.
  - left. eapply no_root_bisim_empty; auto.
Qed.

(*
Definition degree (g : Graph) := length (dom (reorder g)).
 
Goal degree empty = 1.
Proof.
  unfold degree, empty. simpl. decide (tt <> tt); simpl; congruence. 
Qed.
*)

Section Indices.

Context {X : Type} {x_eq_dec : eq_dec X}. 

Definition nth : list X -> nat -> option X := 
   fix nth xs n := 
   match xs, n with
   |[], _ => None
   |(x :: xs), 0 => Some x
   |(x :: xs), S n => nth xs n
   end.

Lemma nth_elem (xs : list X) (n : nat) (x : X) : nth xs n = Some x -> x el xs.
Proof.
  revert n; induction xs; intros; simpl in *; try discriminate.
  destruct n.
  - left; injection H; intros; auto.
  - right; eapply IHxs; eauto.
Qed.

Lemma nth_in_range (xs : list X) (n : nat) : n < |xs| -> exists x, nth xs n = Some x.
Proof.
  revert n; induction xs; simpl in *; intros. omega. destruct n.
  - exists a; auto.
  - apply IHxs. omega.  
Qed.

Lemma nth_found_in_range (xs : list X) (x : X) n : nth xs n = Some x -> n < |xs|.
Proof.
  revert n. induction xs; simpl in *; intros; [discriminate|].
  destruct n; [omega|]. cut (n < |xs|); [omega|]. apply IHxs; auto.
Qed.

Lemma nth_contained (xs : list X) (x : X) : x el xs -> exists n, nth xs n = Some x.
Proof.
  induction xs; simpl; intros; [tauto|].
  destruct H.
  - exists 0; subst; auto.
  - destruct (IHxs H) as [m A]. exists (S m); auto.
Qed.

Definition index (y : X) := fix f xs :=
  match xs with
   |[] => None
   |(x :: xs)=> if eqb x y then Some 0 else
     match f xs 
     with |Some m => Some (S m)
          |None => None
      end
   end. 


Lemma index_of_elem (xs : list X) (x : X)  : x el xs -> exists n, index x xs = Some n.
Proof.
  induction xs; intros; simpl in *; try tauto.
  destruct (eqb a x)eqn:E; try congruence. 
  - exists 0; auto.
  - destruct H; [apply eqb_iff in H; exfalso; congruence|]. specialize (IHxs H). destruct IHxs as [n A].
    destruct (index x xs); try discriminate.
    exists (S n0); auto.
Qed.

Lemma index_elem (xs : list X) (x : X) (n : nat) : index x xs = Some n -> x el xs.
Proof.
  revert n; induction xs; intros; simpl in *.
  - discriminate.
  - destruct (eqb a x) eqn:E. 
    + left; apply eqb_iff; auto.
    + right.  destruct (index x xs) eqn:F; try congruence. eapply IHxs; eauto.
Qed.  

Lemma index_in_range (xs : list X) (x : X) (n : nat) : index x xs = Some n -> n < |xs|.
Proof. 
  revert n; induction xs; intros; simpl in *; try discriminate.
  destruct (eqb a x).
  - injection H; intros; subst. omega.
  - destruct (index x xs) eqn:E; try discriminate.
    injection H; intros; subst. specialize (IHxs n0 eq_refl). omega.
Qed.

Lemma index_nth' (xs : list X) :
                   forall x, x el xs -> 
                   (match (index x xs) with 
                     |Some n => nth xs n
                     |None => Some x
                    end )= Some  x.
Proof.
  induction xs; intros; simpl in *; try tauto.
  destruct (eqb a x) eqn:E.
   - apply -> eqb_iff in E; subst; auto.
   - destruct H; [apply eqb_iff in H; exfalso; congruence|]. 
     destruct (index_of_elem H) as [n A]. specialize (IHxs _ H). 
     destruct (index x xs) eqn:F; congruence. 
Qed.

Lemma index_nth (xs : list X) (x : X) (A : x el xs) (n : nat) :
      index x xs = Some n -> nth xs n = Some x.
Proof.
  revert n; induction xs; intros; simpl in *; try tauto.
  destruct (eqb a x) eqn:E.
   - apply -> eqb_iff in E; subst; auto. destruct n; congruence.
   - destruct A as [A|A]; [apply eqb_iff in A; exfalso; congruence|].  
     specialize (IHxs A). 
     destruct (index x xs) eqn:F; try congruence. injection H; intros; subst.
     apply IHxs. auto.
Qed.

Lemma nth_index (xs : list X) (x : X) (A : x el xs) (n : nat) : 
      dupfree xs -> nth xs n = Some x -> index x xs = Some n.
Proof.
  intros B. revert n. induction xs; intros; simpl in *; try tauto.
  destruct (eqb a x) eqn:E.
  - clear A. destruct n; try congruence. apply -> eqb_iff in E.
    subst a. apply nth_elem in H. exfalso. 
    apply dupfree_cons in B. destruct B as [B C]. apply B; auto. 
  - destruct A as [A|A]; [apply eqb_iff in A; exfalso; congruence|].
    apply dupfree_cons in B. destruct B as [B1 B2]. specialize (IHxs A B2).
    apply index_of_elem in A. destruct A as [m A]. rewrite A. destruct n.
    + injection H; intros. apply eqb_iff in H0. congruence. 
    + specialize (IHxs _ H). congruence.
Qed.

Fixpoint range n := 
  match n with
  |O => []
  |S n => range n ++ [n]
  end.

Lemma range_elems n : forall m, m < n -> m el range n.
Proof.
  induction n; simpl; intros; [omega|]. 
  decide (n = m); apply in_append.
  - right. subst; auto.
  - assert (m < n) by omega; left; apply IHn; auto.
Qed.

Lemma in_range n m : m el range n -> m < n.
Proof.
  induction n; simpl; intros ; [omega|].
  decide (m = n); [omega|]. 
  apply in_append in H. destruct H; [| apply in_sing in H; omega].
  cut (m < n); try omega. apply IHn; auto.
Qed.

Lemma in_range_iff n m : m el range n <-> m < n.
Proof.
  split; intros; eauto using range_elems, in_range.
Qed.

Lemma dupfree_range n : dupfree (range n).
Proof.
  induction n; unfold range; simpl in *; [constructor|].
  apply dupfree_app.
  - change (disjoint (range n) [n]). intros [x [A B]].
    apply in_range_iff in A; apply in_sing in B. omega.
  - auto.
  - constructor; auto. constructor.
Qed.
  

End Indices.



Lemma dupfree_only_one_index (X : Type) (n m : nat) (xs : list X) (x : X) :
          dupfree xs ->
          nth xs n = Some x ->
          nth xs m = Some x -> n = m.
Proof.
  intros A; revert n m x. induction A; intros; simpl in *; [discriminate|].
  destruct n, m; try congruence.
  - injection H0; intros; subst. apply nth_elem in H1. congruence.
  - injection H1; intros; subst. apply nth_elem in H0; congruence.
  - f_equal. eapply IHA; eauto.
Qed.


Definition well_formed (g : Graph) := dupfree (dom g) /\ exists xs, dom g = (root g) :: xs.

Lemma empty_well_formed : well_formed (empty).
Proof.
  split.
  - simpl. constructor; auto. constructor.
  - exists []; auto.
Qed.


Lemma reorder_well_formed g : root g el dom g -> well_formed (reorder g).
Proof.
  intros; split.
  - unfold reorder. simpl. constructor.
    + intros C; apply in_rem_iff in C; intuition.
    + apply dupfree_filter. apply dupfree_undup.
  - simpl. exists (rem (undup (dom g)) (root g)); auto. 
Qed.

Section bisimNat.



Variable g : Graph.
Variable g_well_formed : well_formed g.

Definition graph_to_nat := 
       G 
       (fun n m => 
          match (nth (dom g) n), (nth (dom g) m) with
          |Some x, Some y => E x y
          |_, _ => false
         end) 
       (range (|dom g|)) 
       0.


Lemma dom_g_nat (x : g) : x el dom g -> {n| Some x = nth (dom g) n}.
Proof.
  intros A; destruct (index x (dom g)) eqn:E.
  - exists n. symmetry; apply index_nth; auto.
  - apply index_of_elem in A. exfalso; destruct A; congruence.
Qed.
 
Lemma E_g_nat (x y : g) (n m : nat) : E x y = true -> 
              index x (dom g) = Some n -> index y (dom g) = Some m ->  (@E graph_to_nat n m) = true.
Proof.
  intros. unfold E; simpl. decide (n el range (|dom g |) /\ m el range (|dom g |)); try congruence.
  - destruct a as [A B]. apply in_range_iff in A; apply in_range_iff in B. 
    apply nth_in_range in A; apply nth_in_range in B.
    destruct A as [a A], B as [b B]. rewrite A, B.
    cut (a = x /\ b = y). intros; intuition; subst; auto.
    assert (nth (dom g) n = Some x). { apply index_nth; auto. apply E_in_dom in H. intuition. }
    assert (nth (dom g) m = Some y). { apply index_nth; auto; apply E_in_dom in H; intuition. } 
    split; congruence.
  - contradict n0. split; apply in_range_iff; eapply index_in_range; eauto. 
Qed.

Lemma E_nat_g (m n : nat) (x y : g) :
              (@E graph_to_nat n m) = true -> 
              nth (dom g) n = Some x -> nth (dom g) m = Some y ->
              E x y = true.
Proof.
  intros. unfold E in H. destruct (@decision
          (and (@In (t graph_to_nat) n (dom graph_to_nat))
             (@In (t graph_to_nat) m (dom graph_to_nat)))); try congruence.
  destruct a as [A B]. unfold graph_to_nat in A, B. simpl in *. apply in_range_iff in A.
  apply in_range_iff in B. apply nth_in_range in A. apply nth_in_range in B.
  destruct A as [u A], B as [v B]. rewrite A, B in H.
  congruence.
Qed.
    

Definition convert_to_index (x : g) :=
   match (index x (dom g)) with |Some n => n |None => |dom g| end.


Lemma convert_index_found (x : g) : (convert_to_index x) el dom graph_to_nat ->
                      exists n, index x (dom g) = Some n.
Proof.
  intros. simpl in *. apply in_range_iff in H. pose (I := H). apply nth_in_range in I as [y A].
  exists (convert_to_index x). apply nth_index. 
  - unfold convert_to_index in A. destruct (index x (dom g)) eqn:E; try congruence.
    + eapply index_elem; eauto.
    + unfold convert_to_index in H. rewrite E in H. omega.  
  - destruct g_well_formed; auto.
  - cut (x = y); intros; subst; auto. unfold convert_to_index in A.
    destruct (index x (dom g)) eqn:E.
    + apply index_nth in E. congruence. unfold convert_to_index in H. rewrite E in H. 
      apply index_elem in E. auto.
    + unfold convert_to_index in H; rewrite E in H; omega.
Qed.

Lemma E_nat_g_equiv (x y : g) :
      E x y = true <-> @E graph_to_nat (convert_to_index x) (convert_to_index y) = true.
Proof.
   split; intros.
   - assert (x el dom g) by (apply E_in_dom in H; intuition).
     assert (y el dom g) by (apply E_in_dom in H; intuition). 
     eapply E_g_nat in H; eauto.
     + destruct (index_of_elem H0). 
       unfold convert_to_index. simpl. rewrite H2. auto.
     + destruct (index_of_elem H1).
       unfold convert_to_index; simpl. rewrite H2; auto.
   - pose (I := H). apply E_in_dom in I; destruct I as [A B]. 
     simpl in *. apply in_range_iff in A. apply in_range_iff in B.
     apply nth_in_range in A. apply nth_in_range in B. destruct A as [n A], B as [m B].
     pose (I := H); apply E_in_dom in I.
     unfold convert_to_index in A, B. destruct I as [C D]. 
     apply convert_index_found in C as [u C].
     apply convert_index_found in D as [v D]. rewrite C in A; rewrite D in B.
     assert (x el dom g). { apply index_elem in C. auto. }
     assert (y el dom g) by (apply index_elem in D; auto). 
     unfold convert_to_index in H; apply trivial_dec in H.
     rewrite C, D in H. 
     apply index_nth in C; auto. apply index_nth in D; auto.
     assert (x = n) by congruence; assert (y = m) by congruence.
     subst. unfold graph_to_nat in H. simpl in H. rewrite A, B in H. auto.
Qed.


Lemma bisimGraphNat : bisim g graph_to_nat.
Proof.
  apply bisimIsom with (f := convert_to_index).
  - unfold iso. exists (fun n => match (nth (dom g) n) with |Some x => x |None => root g end).
    split; intros.
     + destruct (nth (dom g) (convert_to_index x)) eqn:E.
       * unfold convert_to_index in E. destruct (index x (dom g)) eqn:F; simpl in *.
         { cut (nth (dom g) n = Some x). { intros. congruence. }
            apply index_nth; auto.
         }
         apply index_of_elem in H. destruct H; congruence. 
       * unfold convert_to_index in E. destruct (index x (dom g)) eqn:F; simpl in *.
         {  apply index_in_range in F. apply nth_in_range in F.
            destruct F; congruence. } 
         apply index_of_elem in H; destruct H; congruence.
     +  destruct (nth (dom g) y) eqn:E.
       * unfold convert_to_index. simpl. destruct (index t (dom g)) eqn:F; simpl in *.
         { apply index_nth in F. 
           - destruct g_well_formed; eapply dupfree_only_one_index; eauto.
           - apply nth_elem in E. auto. 
         } apply in_range_iff in H. apply nth_index in E; try congruence.
           { eapply nth_elem. eauto. } firstorder.
       * unfold convert_to_index. unfold graph_to_nat in H. simpl in H. 
         apply in_range_iff in H. apply nth_in_range in H. destruct H; congruence.
  - split; [|split]; intros.
    + split; intros u A.
      * apply in_map_iff in A. destruct A as [x [A B]]. unfold convert_to_index in A. 
        destruct (index x (dom g)) eqn:E.
        { subst u. apply in_range_iff. apply index_in_range in E. auto. }
        subst u. apply index_of_elem in B. destruct B; congruence. 
      * apply in_map_iff. unfold convert_to_index. simpl in *. apply in_range_iff in A.
        apply nth_in_range in A. destruct A as [x A]. exists x.
        { apply nth_index in A.
          - rewrite A.  split; auto. eapply index_elem. eauto.
          - eapply nth_elem. eauto.
          - firstorder.
        }
    + unfold convert_to_index; simpl. destruct g_well_formed as [A [l B]].
      assert (root g el dom g). { rewrite B. auto. }
      apply index_of_elem in H. destruct H as [n C]; rewrite C.
      rewrite B in C. simpl in C. assert (eqb (root g) (root g) = true).
      apply eqb_iff; auto. rewrite H in C. injection C; intros; auto.
    + split; intros; apply E_nat_g_equiv; auto.
Qed.

Lemma graph_to_nat_well_formed : well_formed graph_to_nat.
Proof.
   split.
   - simpl. apply dupfree_range.
   - simpl. remember (dom g) as l. assert (l <> []).
     { destruct g_well_formed as [A [xs B]]. intros C. subst. congruence. }
     clear Heql. induction l; simpl in *.
     + congruence.  
     + destruct l; simpl in *.
       * exists []; auto.
       * destruct IHl as [xs A]. congruence. unfold range in *. simpl. 
         change (exists xs0 : list nat,
          range (S (|l|)) ++ [S (|l |)] = 0 :: xs0).
          change (range (S (|l|)) = 0 :: xs) in A. rewrite A. 
          exists (xs ++ [S (|l|)]). auto.
Qed.

End bisimNat.


Definition graph_on (g : Graph) (X : Type) := t g = X.


Definition make_well_formed (g : Graph) := if decision (root g el dom g) then reorder g else empty.

Lemma make_well_formed_corr (g : Graph) : well_formed (make_well_formed g).
Proof.
  intros; unfold make_well_formed; decide (root g el dom g);
  eauto using empty_well_formed, reorder_well_formed.
Qed.

Lemma make_well_formed_bisim (g : Graph) : bisim g (make_well_formed g).
Proof.
  intros; unfold make_well_formed; decide (root g el dom g);
  eauto using no_root_bisim_empty, with_root_bisim_reorder.
Qed.

Lemma make_well_formed_id (g : Graph) : well_formed g -> g = make_well_formed g.
Proof.
  intros [A [xs B]]. unfold make_well_formed.
  decide (root g el dom g) as [H|H]; [|contradict H; rewrite B; auto]. 
  cut (dom g = dom (reorder g)). { unfold reorder; intros; destruct g; simpl; f_equal; auto. }
  unfold reorder. simpl. assert (~ root g el xs). { rewrite B in A. apply dupfree_cons in A. intuition. }
  eapply undup_id in A. rewrite A. rewrite B. simpl.
  decide (root g <> root g); [congruence|]. f_equal. symmetry; apply rem_id. auto.
Qed.

Definition proj_nat (g : Graph) := graph_to_nat (make_well_formed g).

Lemma proj_nat_well_formed (g : Graph) : well_formed (proj_nat g).
Proof.
   apply graph_to_nat_well_formed; apply make_well_formed_corr.
Qed.

Theorem bisimNat (g : Graph) : bisim g (proj_nat g).
Proof.
  eapply bisimTrans. eapply make_well_formed_bisim.
  apply bisimGraphNat. apply make_well_formed_corr.
Qed.

Section MapCat.

Variable (X : Type) (Y : Type) (f : X -> list Y) (xs : list X).

Definition mapcat := flatten (map f xs).

Lemma in_mapcat_iff y : y el mapcat <-> exists x, x el xs /\ y el f x.
Proof.
  split; intros.
  - apply in_flatten_iff in H as [ys [A B]].
    apply in_map_iff in A as [x [C D]]; exists x; subst; auto.
  - apply in_flatten_iff. destruct H as [x [A B]]. exists (f x); split; auto.
    apply in_map_iff; firstorder.
Qed.

End MapCat.


Lemma mapcat_app (X Y : Type) (f : X -> list Y) (xs ys : list X) : mapcat f (xs ++ ys) = mapcat f xs ++ mapcat f ys.
Proof.
  induction xs; simpl in *; [auto|].
  unfold mapcat in *. simpl. rewrite IHxs.
  rewrite app_assoc. auto.
Qed.

Definition prefix (X : Type) (xs ys : list X) := exists zs, ys = xs ++ zs. 

Lemma prefix_trans (X : Type) (xs ys zs : list X) : prefix xs ys -> prefix ys zs -> prefix xs zs.
Proof.
  intros [ls A] [rs B]; unfold prefix.
  - exists (ls ++ rs); rewrite app_assoc. subst; auto.
Qed.

Section FirstInList.
 
Variable (X : Type) (p : X -> Prop).
Context {p_dec : forall x, dec (p x)}.

Fixpoint find_first_index xs :=
    match xs with
      | [] => None
      | (x :: xs) => if (decision (p x)) then Some 0 else 
        match find_first_index xs with
         |None => None
         |Some n => Some (n + 1)
        end
    end.


Lemma find_first_index_char xs n : find_first_index xs = Some n -> {x | nth xs n = Some x /\ p x}.
Proof.
  revert n; induction xs; simpl in *; intros n A; [discriminate|]. decide (p a); simpl in *.
  - injection A; intros; subst. exists a; auto.
  - destruct (find_first_index xs) eqn:E; [|congruence].
    injection A; intros; subst. replace (n1 + 1) with (S n1) by omega. apply IHxs. auto.
Qed.

Lemma find_first_index_char' xs x : x el xs -> p x -> {n | find_first_index xs = Some n}.
Proof.
  revert x; induction xs; simpl in *; intros x A B; [tauto|].
  decide (p a); try congruence.
  - exists 0; auto. 
  - assert (C : x el xs). {destruct A; congruence. } destruct (IHxs _ C B) as [m D].
    exists (S m). destruct (find_first_index xs); try congruence. f_equal; injection D; intros; omega.
Qed.


Lemma find_first_corr xs : (exists x, x el xs /\ p x) <-> (exists n, find_first_index xs = Some n).
Proof.
  split; intros; firstorder using find_first_index_char, find_first_index_char'.
  destruct (find_first_index_char H) as [y [A B]]. exists y; split; auto. apply nth_elem in A. auto.
Qed.


Lemma prefix_nth (xs ys : list X) n (x : X) : prefix xs ys -> nth xs n = Some x -> nth ys n = Some x.
Proof.
  revert ys n x. induction xs; intros; simpl in *; [discriminate|].
  destruct n.
  - destruct H as [zs B]; subst ys. simpl. auto.
  - destruct H as [zs B]; subst ys; simpl. apply IHxs. exists zs; auto. auto.
Qed.

(*
Lemma find_first_p xs x : find_first xs = Some x -> p x.
Proof.
  induction xs; simpl in *; intros A; [discriminate|]. 
  decide (p a); auto. injection A; intros; subst; auto.
Qed.

Lemma find_first_elem xs x : find_first xs = Some x -> x el xs.
Proof.
  induction xs; simpl in *; intros A; [discriminate|].
  decide (p a); auto. injection A; intros; subst; auto.
Qed.
*)

Lemma incl_first_same_elem (xs ys : list X) (n : nat) :
    prefix xs ys -> find_first_index xs = Some n -> find_first_index ys = Some n.
Proof.
   revert ys n; induction xs; intros; simpl in *; [discriminate|].
   unfold prefix in *.  destruct H as [zs C]. subst ys.
   simpl in *. decide (p a).
   - injection H0; intros; auto.
   - destruct (find_first_index xs); try congruence.
     destruct n. { injection H0; intros. exfalso; omega. }
     assert (find_first_index (xs++zs) = Some n).
     { apply IHxs. eauto. f_equal. injection H0; subst; omega. }
     rewrite H. f_equal; injection H0; intros; omega.
Qed.


End FirstInList.

Arguments find_first_index {X} (p) {p_dec} (xs).

Lemma find_first_equiv (X : Type) (p q : X -> Prop) {p_dec : forall x, dec (p x)} 
                       {q_dec : forall x, dec (q x)} xs :
                       (forall x, p x <-> q x) -> find_first_index p xs = find_first_index q xs.
Proof. 
   intros; induction xs; simpl in *; [congruence|].
   decide (p a).
   - assert (q a) by firstorder. decide (q a); congruence.
   - assert (~ q a) by firstorder. decide (q a); try congruence.
     rewrite IHxs. auto.
Qed.


Section FirstInMapcat.

Variable (X : Type) (xs : list X) (f : X -> list X).
Variable (p : X -> Prop).
Context {p_dec : forall x, dec (p x)}.


Lemma first_in_mapcat n : find_first_index p (mapcat f xs) = Some n -> 
                         exists x, x el xs /\ exists z, z el f x /\ p z.
Proof.
  intros A. apply find_first_index_char in A as [u [A B]].
  assert (u el mapcat f xs). { apply nth_elem in A. auto. } 
  apply in_mapcat_iff in H as [v [C D]].
  exists v; split; auto. exists u; split; auto.
Qed.

Lemma first_in_mapcat' x z : x el xs -> z el f x -> p z -> exists n, find_first_index p (mapcat f xs) = Some n.
Proof.
  intros. apply find_first_corr. exists z. split; auto. apply in_mapcat_iff.
  exists x; split; auto.
Qed.

End FirstInMapcat.


Definition one_to_n (n : nat) := map S (range n).

Lemma in_one_to_n_iff (n :nat) m : m el one_to_n n <-> 1 <= m <= n.
Proof.
  split; intros.
  - unfold one_to_n in H. apply in_map_iff in H as [x [A B]].
    apply in_range_iff in B. omega.
  - unfold one_to_n; apply in_map_iff. destruct m; [omega|].
    exists m; split; auto. apply in_range_iff; omega.
Qed.

Section MapcatPrefix.


Lemma app_nil (X : Type) (xs : list X) : xs ++ [] = xs.
Proof.
  induction xs; simpl in *; congruence.
Qed. 
  

Lemma flatten_app (X : Type) (xs ys : list (list X)) : flatten (xs ++ ys) = flatten xs ++ flatten ys.
Proof.
  revert ys; induction xs; intros; simpl in *.
  - auto.
  - rewrite <- app_assoc. rewrite IHxs. auto.
Qed.

Lemma l_n_prefix_l_S_n n : prefix (one_to_n n) (one_to_n (S n)).
Proof.
  unfold one_to_n; induction n; simpl in *.
  - exists [1]. auto.
  - rewrite !map_app. exists [S (S n)]. simpl. auto.
Qed.

Lemma n_le_m_pref n m : n <= m -> prefix (one_to_n n) (one_to_n m).
Proof.
  unfold one_to_n.
  revert n; induction m; intros; simpl in *.
  - destruct n; [|omega]. exists []; auto. 
  - decide (n = S m).
    { subst. simpl.  exists []. rewrite app_nil; auto. }
    assert (S n <= S m) by omega. assert (n <= m) by omega.
    destruct (IHm _ H1) as [zs A].
    rewrite !map_app. rewrite A. exists (zs ++ [S m]). rewrite app_assoc. auto.
Qed.

Variable (X : Type) (xs : list X) (ys : list X).
Variable (Y : Type) (f : X -> list Y).
Variable xs_pref_ys : prefix xs ys.

Lemma mapcat_preserves_pref : prefix (mapcat f xs) (mapcat f ys).
Proof.
  revert ys xs_pref_ys. induction xs; intros; simpl in *.
  - exists (mapcat f ys); auto.
  - destruct xs_pref_ys as [zs A]. rewrite A.
    exists (mapcat f zs). simpl. 
    unfold mapcat in *; simpl in *. rewrite <- app_assoc. 
    rewrite map_app. rewrite flatten_app; auto.
Qed.

End MapcatPrefix.

Lemma len_map (X Y : Type) (xs : list X) (f : X -> Y) : |map f xs| = |xs|.
Proof.
  induction xs; simpl in *; omega.
Qed.

Lemma len_app (X : Type) (xs ys : list X) : |xs ++ ys| = |xs| + |ys|.
Proof.
  revert ys; induction xs; intros; simpl in *; [|f_equal]; auto.
Qed.

Lemma len_power_gt_one (X : Type) (xs : list X) : |power xs| >= 1.
Proof.
  induction xs; simpl in *; [|rewrite len_app]; omega.
Qed.


Lemma mapcat_len (X Y : Type) (xs : list X) (f : X -> list Y) : (forall x, |f x| >= 1) -> |mapcat f xs| >= |xs|.
Proof.
  induction xs; intros; simpl in *; [omega|].
  unfold mapcat in *; simpl in *. rewrite len_app. unfold id. specialize (IHxs H). specialize (H a). omega.
Qed.

Section DomSizeFixed.

Variable n : nat.

Definition all_graphs_size_n := map (fun f => G f (range n) 0 ) (allFuns (range n) (range n)).
Lemma at_least_one_graph : |all_graphs_size_n| >= 1.
Proof.
  unfold all_graphs_size_n. rewrite len_map. unfold allFuns. rewrite len_map.
  unfold allPairs. apply len_power_gt_one.
Qed.

Variable n_gt_0 : n > 0.

Lemma in_all_graphs_size_n_iff (g : Graph) : g el all_graphs_size_n -> graph_on g nat /\ well_formed g.
Proof.
  unfold all_graphs_size_n; intros; split; simpl in *; apply in_map_iff in H as [x [A B]]. 
  - subst. unfold graph_on. simpl. auto.
  - split. 
    + subst g; simpl. apply dupfree_range.
    + subst g; simpl. clear x B. induction n; simpl in *; [omega|]. destruct n0; unfold range; simpl in *.
      * exists []; auto.
      * destruct IHn0 as [xs A]. omega. exists (xs ++ [S n0]). simpl. 
        change ((range (S n0)) ++ [S n0] = 0 :: xs ++ [S n0]). simpl. rewrite A. auto.
Qed.

Lemma well_formed_bisim_size_dom (g : Graph) : well_formed g -> |dom g| = n -> 
                            (graph_to_nat g) el all_graphs_size_n.
Proof.
   intros. unfold all_graphs_size_n; apply in_map_iff. 
   simpl. exists (edgeRel (g := graph_to_nat g)). split.
   - unfold graph_to_nat; f_equal. congruence. 
   - apply all_funs_contained. intros. split.
     + unfold graph_to_nat in H1; simpl in H1. destruct (nth (dom g) x) eqn:E; try congruence.
       apply in_range_iff. apply nth_found_in_range in E. congruence.
     + unfold graph_to_nat in H1; simpl in H1. destruct (nth (dom g) x) eqn:E; try congruence.
       destruct (nth (dom g) y) eqn:F; try congruence.
       apply in_range_iff. apply nth_found_in_range in F. congruence.
Qed.

End DomSizeFixed.

Lemma range_size n : |range n| = n.
Proof.
  induction n; simpl in *; [omega|].
  unfold range. simpl; rewrite len_app; simpl. change ((|range n |) + 1 = S n). rewrite IHn. 
  omega.
Qed.

Lemma proj_nat_same_dom_size g : |dom (graph_to_nat g)| = |dom g|.
Proof.
  simpl. rewrite range_size. auto. 
Qed.

Lemma filter_len (X : Type)  (p : X -> Prop) {p_dec : forall x, dec (p x)} (xs : list X) : |filter p xs| <= |xs|.
Proof.
  induction xs; intros; simpl in *; [omega|].
  decide (p a); simpl in *; omega.
Qed.

Lemma undup_len (X : Type) {x_eq_dec : eq_dec X} (xs : list X) : |undup xs| <= |xs|.
Proof.
  induction xs; simpl in *; [auto|].
  decide (a el xs); simpl; omega.
Qed.

Lemma len_rem (X : Type) {x_eq_dec : eq_dec X} (xs : list X) : forall x, x el xs -> |(rem xs x)| < |xs|.
Proof.
  induction xs; intros; simpl in *; [tauto|].
  decide (a <> x); destruct H; simpl in *; try congruence.
  - cut (|rem xs x | < |xs |); [intros; omega| auto].
  - assert (|rem xs x| <= |xs|). {apply filter_len. } omega.
  - assert (|rem xs x| <= |xs|) by (apply filter_len). omega.
Qed. 

Lemma wf_reorder_dom_size g : root g el dom g -> |dom (reorder g)| <= |dom g|.
Proof.
  intros; unfold reorder; decide (root g el dom g); [|congruence]; simpl.
  cut (|rem (undup (dom g)) (root g) | < |dom g |); [intros; omega|].
  cut (|rem (undup (dom g)) (root g) | < |undup (dom g)|).
  { assert (|undup (dom g)| <= |dom g|) by (apply undup_len). omega. }
  apply len_rem. apply undup_id_equi. auto.
Qed.

Lemma reorder_dom_size g : root g el dom g -> |(dom (proj_nat g))| <= |dom g|.
Proof.
  unfold proj_nat. unfold make_well_formed. intros A; decide (root g el dom g); [|congruence].
  rewrite proj_nat_same_dom_size. apply wf_reorder_dom_size; auto.
Qed.

Lemma empty_dom_size g : ~ root g el dom g -> |(dom (proj_nat g))| <= S (|dom g|).
Proof.
  intros A; unfold proj_nat; unfold make_well_formed; simpl.
  decide (root g el dom g); [congruence|]. 
  simpl. omega.
Qed.

Lemma dom_size_limit_for_graph_nat g : |dom (proj_nat g)| <= S (|dom g|).
Proof.
  decide (root g el dom g).
  - rewrite reorder_dom_size; auto.
  - rewrite empty_dom_size; auto.
Qed.

Lemma nat_graph_dom_size_min g : |dom (proj_nat g)| >= 1.
Proof.
  assert (well_formed (proj_nat g)) as [A [xs B]]. { apply proj_nat_well_formed. }
  rewrite B. simpl. omega.
Qed.

Section EnoughGraphs.

Variable g : Graph.

Definition graphs_of_size_lt_n n := mapcat all_graphs_size_n (one_to_n n).

Definition nat_graphs_for_g := graphs_of_size_lt_n (S (|dom g|)).

Lemma nat_graphs_for_g_contains_proj : (proj_nat g) el nat_graphs_for_g.
Proof.
  apply in_mapcat_iff. exists (|dom (proj_nat g)|). split.
  - apply in_one_to_n_iff. split; [| apply dom_size_limit_for_graph_nat].
    cut (|dom (proj_nat g)| >= 1); [omega|]. apply nat_graph_dom_size_min.
  - apply well_formed_bisim_size_dom. 
    + apply make_well_formed_corr.
    + unfold proj_nat. symmetry. apply proj_nat_same_dom_size.
Qed.

End EnoughGraphs.


Section Enumerate.

Definition graph_num g := 
  let (g', A) := find_first_index_char' (p := bisim g) (nat_graphs_for_g_contains_proj g) (bisimNat g)
  in g'.

Lemma representant_some g : find_first_index (bisim g) (nat_graphs_for_g g) = Some (graph_num g).
Proof.
  unfold graph_num.
  destruct (find_first_index_char' (p:=bisim g) (xs:=nat_graphs_for_g g) (x:=proj_nat g)
    (nat_graphs_for_g_contains_proj g) (bisimNat g)).
  auto.
Qed.

Lemma graph_num_bisim g g' : nth (nat_graphs_for_g g) (graph_num g) = Some g' -> bisim g g'.
Proof.
  intros. assert (find_first_index (bisim g) (nat_graphs_for_g g) = Some (graph_num g)). 
  {apply representant_some. } unfold nat_graphs_for_g in *.
  apply find_first_index_char in H0. destruct H0 as [g0 [A B]]. congruence. 
Qed.

Definition graph_index n := match nth (graphs_of_size_lt_n (S n)) n with
   |Some g => g
   |None => empty
   end.

Lemma prefix_graphs_of_size_le n m: n <= m -> prefix (graphs_of_size_lt_n n) (graphs_of_size_lt_n m).
Proof.
  intros. unfold graphs_of_size_lt_n. apply mapcat_preserves_pref. apply n_le_m_pref. omega.
Qed.

Lemma graph_index_corr : forall g,  bisim g (graph_index (graph_num g)) .
Proof.
  intros. unfold graph_index. destruct (nth (graphs_of_size_lt_n (S (graph_num g))) (graph_num g)) eqn:E.
  - decide (graph_num g <= |dom g|). 
    + assert (prefix (graphs_of_size_lt_n (S (graph_num g))) (nat_graphs_for_g g)). { 
      unfold nat_graphs_for_g. apply prefix_graphs_of_size_le. omega. }
      apply (prefix_nth H) in E. apply graph_num_bisim; auto.
    + assert (|dom g| <= graph_num g) by omega.
      assert (prefix (nat_graphs_for_g g) (graphs_of_size_lt_n (S (graph_num g)))). { 
         unfold nat_graphs_for_g. apply prefix_graphs_of_size_le. omega.
        } assert (find_first_index (bisim g) (nat_graphs_for_g g) = Some (graph_num g)). 
        { apply representant_some. } apply find_first_index_char in H1 as [g' [A B]].
            apply (prefix_nth H0) in A. congruence.  
  - exfalso. remember (graph_num g) as n. assert (n < |graphs_of_size_lt_n (S n)|).
    { unfold graphs_of_size_lt_n. 
      assert (|mapcat all_graphs_size_n (one_to_n (S n))| >= |(one_to_n (S n))|).
      { apply mapcat_len. apply at_least_one_graph. }
      assert (|one_to_n (S n)| = S n).
      { unfold one_to_n. rewrite len_map. rewrite range_size. auto. } omega. }
    apply nth_in_range in H as [x C]. congruence.
Qed.

Lemma representative_elem_le (g : Graph) : 
     forall g', bisim g' g -> |dom g| <= |dom g'| -> graph_num g' = graph_num g.
Proof.
  intros. unfold graph_num.
  cut (find_first_index (bisim g) (nat_graphs_for_g g) = find_first_index (bisim g') (nat_graphs_for_g g')).
  { intros. repeat rewrite representant_some in H1. injection H1; auto. }
  assert (find_first_index (bisim g) (nat_graphs_for_g g) = Some (graph_num g)). { apply representant_some. }
  assert (find_first_index (bisim g) (nat_graphs_for_g g) =
       find_first_index (bisim g') (nat_graphs_for_g g)). {
          apply find_first_equiv. intros; split; intros; eauto using bisimTrans, bisimSym. 
       }
  assert (find_first_index (bisim g') (nat_graphs_for_g g) = 
          find_first_index (bisim g') (nat_graphs_for_g g')). {
          rewrite <- H2, H1. symmetry. 
          apply incl_first_same_elem with (xs := nat_graphs_for_g g).
          - unfold nat_graphs_for_g. apply mapcat_preserves_pref.
            apply n_le_m_pref. omega.
          - rewrite <- H2. auto. }
  rewrite H2. rewrite H3. auto.
Qed.
          

Theorem representative_elem (g : Graph) : 
     forall g', bisim g' g <-> graph_num g' = graph_num g.
Proof.
  intros; split; intros. 
  - decide (|dom g| <= |dom g'|).
    { apply representative_elem_le; auto. }
    assert (|dom g'| <= |dom g|) by omega.
    symmetry; apply representative_elem_le; auto. now symmetry.
  - assert (find_first_index (bisim g) (nat_graphs_for_g g) = Some (graph_num g)) by (apply representant_some). 
    assert (find_first_index (bisim g') (nat_graphs_for_g g') = Some (graph_num g')) by (apply representant_some). 
    apply find_first_index_char in H0. apply find_first_index_char in H1. rewrite H in H1. 
    destruct H0 as [x [A B]], H1 as [y [C D]]. 
    cut (Some x = Some y). {intros E; injection E; intros; subst; eauto using bisimTrans, bisimSym. }
    decide (|dom g| <= |dom g'|).
    + assert (E : S (|dom g|) <= S (|dom g'|)) by omega.
      unfold nat_graphs_for_g in *. apply prefix_graphs_of_size_le in E. 
      rewrite (prefix_nth E A) in C. auto.
    + assert (E : S (|dom g'|) <= S (|dom g|)) by omega.
      unfold nat_graphs_for_g in *. apply prefix_graphs_of_size_le in E. 
      rewrite (prefix_nth E C) in A. auto.
Qed.

Lemma graph_num_corr g g' : bisim g g' -> graph_num g = graph_num g'.
Proof. 
  intros; now apply representative_elem.
Qed.

End Enumerate.


