Require Export Base.
Require Export Omega.
(* Set Printing Projections. *)

Structure Graph := G {
t :> Type;
t_eq_dec : eq_dec t;
edgeRel : t -> t -> bool;
dom : list t;
root : t
}.

Arguments G {t} {t_eq_dec} (edgeRel) (dom) (root).

Instance graph_eq_dec (g : Graph) : eq_dec g.
Proof.
  apply t_eq_dec.
Defined.

Section GraphIntro.

Context {g : Graph}.

 
Definition E (x y : g) := 
   if (decision (x el g.(dom) /\
       y el g.(dom)))
   then (edgeRel x y) else false.


Inductive path : list g -> g -> g -> Prop :=
   |Path_O x : x el dom g -> path [x] x x
   |Path_S (x y z : g) (A : list g) : path A y z -> E x y = true -> path (x :: A) x z.

Definition path_ex x y := exists A, path A x y.

Lemma E_in_dom (x y : g) : E x y = true -> x el dom g /\ y el dom g.
Proof.
  unfold E. decide (x el dom g /\ y el dom g); congruence.
Qed.

Lemma E_edgeRel (x y : g) : E x y = true -> edgeRel x y = true.
Proof.
  unfold E; decide (x el dom g /\ y el dom g); congruence.
Qed.

End GraphIntro.


Definition dom' g := root g :: dom g.
Section Bisim.


Variable g1 g2 : Graph.

Inductive isBisim (p : g1 -> g2 -> bool) : Prop :=
|isB : 
       (forall x y,  p x y = true -> 
          (forall x', E x x' = true -> exists y', E y y' = true /\ p x' y' = true) /\
          (forall y', E y y' = true -> exists x', E x x' = true /\ p x' y' = true)) 
          -> isBisim p.

Definition bisim :=  exists p, isBisim p /\ p (root g1) (root g2) = true.

End Bisim.


Definition eqb {X : Type} {x_eq_dec : eq_dec X} := fun x y => if (decision (x = y)) then true else false.

Lemma eqb_iff {X : Type} {x_eqdec : eq_dec X} : forall x y, eqb x y = true <-> x = y.
Proof.
  unfold eqb; split; intros; decide (x = y); congruence. 
Qed.


Lemma decision_done (A : Prop) (A_dec : dec (A)) (X : Type) : forall s t : X,
     A -> (if (decision (A)) then s else t) = s.
Proof.
  intros; decide (A); congruence.
Qed.

Lemma decision_done' (A : Prop) (A_dec : dec (A)) (X : Type) : forall s t : X,
    (not A) -> (if (decision (A)) then s else t) = t.
Proof.
  intros; decide (A); congruence.
Qed.
Section Reflexivity.

Variable g1 : Graph.



Lemma bisimRefl : bisim g1 g1.
Proof.
  exists (eqb).
  split; [constructor|].
  - intros. split; intros.
    + exists x'. split.
      * rewrite eqb_iff in H; subst; auto.
      * apply eqb_iff; auto.
    + exists y'; split. 
      * rewrite eqb_iff in H; subst; auto.
      * apply eqb_iff; auto. 
 - apply eqb_iff; auto.
Qed.

End Reflexivity.

Section Transitivity.

Variable g1 g2 g3 : Graph.


Lemma bisimTrans : bisim g1 g2 -> bisim g2 g3 -> bisim g1 g3.
Proof.
  intros [P [[A1] A2]] [R [[B1] B2]].
  exists (fun x z => if (decision (exists y, y el dom' g2 /\ P x y = true /\ R y z = true)) then true else false).
  split; [constructor|]; intros.
  - split; intros.
   + decide (exists y0 : g2, y0 el dom' g2 /\ P x y0 = true /\ R y0 y = true); try congruence.
     clear H. destruct e as [u [C [D E]]]. specialize (A1 _ _ D). destruct A1 as [A1 A3]. 
     specialize (A1 _ H0). destruct A1 as [y' [F G]]. specialize (B1 _ _  E). destruct B1 as [B1 B3].
     specialize (B1 _ F). destruct B1 as [u' [I J]]. 
     exists u'; split; try congruence. apply decision_done; try reflexivity. exists y'; split; auto.
     destruct (E_in_dom F); right; auto.
   + decide (exists y0 : g2,
             y0 el dom' g2 /\ P x y0 = true /\ R y0 y = true); try discriminate.
     destruct e as [u [C [D E]]]. specialize (A1 _ _   D). destruct A1 as [A1 A3]. 
     specialize (B1 _ _  E). destruct B1 as [B1 B3].
     specialize (B3 _ H0). destruct B3 as [x' [F G]]. 
     specialize (A3 _ F). destruct A3 as [u' [I J]]. specialize (A1 _ I). destruct A1 as [z [K L]]. 
     exists u'; split; try congruence. apply decision_done. exists x'; split; auto.
     destruct (E_in_dom F); right; auto. 
  - apply decision_done. exists (root g2). split.
    + left; auto.
    + firstorder.
Qed. 


End Transitivity.

Section Symmetry.

Variable g1 g2 : Graph.


Lemma bisimSym : bisim g1 g2 -> bisim g2 g1.
Proof.
  intros [p [[A] B]]. exists (fun y x => p x y). split.
  - constructor. intros; split; intros.
    + specialize (A _ _ H). destruct A as [A1 A2]. specialize (A2 _ H0). destruct A2 as [y' [B1 B2]].
      exists y'. split; auto.
    + specialize (A _ _ H). destruct A as [A1 A2]. specialize (A1 _ H0). destruct A1 as [x' [B1 B2]].
      exists x'; split; auto.
  - auto.
Qed.

End Symmetry.


Definition allPairs (X Y : Type) (xs : list X) (ys : list Y) := power (list_prod xs ys).


Instance pair_eq_dec (X Y : Type) (A : forall x y : X, dec (x = y)) (B : forall x y : Y, dec (x = y)): 
   forall x y : (X * Y), dec (x = y).
Proof.
  intros [a b] [c d]. decide (a = c); decide (b = d); try (right; congruence).
  left; congruence.
Qed.

Lemma in_append (X : Type) (a : X) xs ys : a el xs \/ a el ys <-> a el xs ++ ys.
Proof.
  revert ys; induction xs; intros [|y ys]; split; intros; simpl in *; auto; try tauto.
  - destruct H; try tauto. destruct H; [left|right]; auto.
  - left. destruct H; [left|right]; firstorder. 
  - repeat destruct H; firstorder.
  - repeat destruct H.
    + auto.
    + apply IHxs in H. firstorder.
Qed.
  

Lemma power_incl' (X : Type) (xs ys : list X) (x_eq_dec : forall x y : X, dec (x = y)) : ys <<= xs -> exists zs, zs el power xs /\ zs === ys.
Proof.
  revert ys; induction xs; intros [| y ys] A; simpl in *.
  - exists []; auto.
  - unfold incl in A. exfalso; apply A with (a := y); auto.
  - exists []. split; try now auto. cut (exists zs, zs el power xs /\ zs === []).
    + intros [zs [B C]]. destruct zs; try now auto. hnf in C. unfold incl in C. destruct C as [C1 C2]. 
      specialize (C1 x). exfalso; firstorder.
    + apply IHxs. firstorder. 
  - assert (rem (y :: ys) a <<= xs). {
       intros v B. apply in_rem_iff in B. destruct B as [B1 B2]. destruct (A v B1); try congruence.
     } destruct (IHxs _ H) as [u [B1 B2]].  destruct (decision (a el y::ys)).
     +  exists (a :: u). split. 
       * apply in_append. right. apply in_map_iff. exists u; auto.
       * split; intros v C. 
         { destruct (decision (v = a)). 
           - subst v. auto.
           - simpl in B2. decide (y <> a); try congruence.
             + destruct C; try congruence. assert (v el (y :: rem ys  a)).  { apply B2. auto. }
               destruct (decision (v = y)). left; auto. simpl; right. simpl in H1; destruct H1; try congruence.
               apply in_rem_iff in H1. tauto.
             + simpl in C, i. destruct C; try congruence. assert (y = a). { destruct (decision (y = a)); tauto. }
               right. assert (v el rem ys a). { apply B2; auto. }  apply in_rem_iff in H2; tauto.
         }
         { destruct (decision (v = a)).
           - left; auto.
           - right. apply B2. apply in_rem_iff; tauto.
          }
      + exists u. split; try eauto using in_append. cut (y :: ys === rem (y :: ys) a). 
        { intros. rewrite H0. auto. } split; intros v C.
        * apply in_rem_iff. split; try auto. destruct (decision (v = a)); try congruence. 
        * apply in_rem_iff in C. tauto.
Qed.



Lemma list_prod_nil (X : Type) (xs : list X) : list_prod xs (@nil X) = (@nil (X * X)).
Proof. 
   induction xs; simpl; try congruence.
Qed.

Lemma incl_nil (X : Type) (xs : list X) : xs <<= [] -> xs = [].
Proof.
  destruct xs; simpl in *; try congruence. intros. unfold incl in H. specialize (H x); exfalso; firstorder.
Qed.

  
Lemma inclProd (X : Type) (Y : Type) (x_eq_dec : forall x y : X, dec (x = y)) 
               (y_eq_dec : forall x y : Y, dec ( x= y)) (xs cs : list X) (ys ds : list Y) :
       cs <<= xs -> ds <<= ys -> list_prod cs ds <<= list_prod xs ys.
Proof.
   intros A B [x y] C. apply in_prod_iff. apply in_prod_iff in C. firstorder.
Qed. 
 

Lemma allPairsCorr (X Y : Type) (A : forall x y : X, dec (x = y)) (B : forall x y : Y, dec (x = y)) : 
   forall (xs : list X) (ys : list Y), forall lxs, lxs <<= xs -> forall lys, lys <<= ys ->
  exists (u : list (X * Y)), u el allPairs xs ys /\ u === list_prod lxs lys.
Proof.
  intros. unfold allPairs. apply power_incl'. 
  - auto.
  - apply inclProd; auto.
Qed.


Definition allFuns (X Y: Type) (xs : list X) (ys : list Y) {A : forall x y : X, dec (x = y)} {B : forall x y : Y, dec (x = y)} := 
      map (fun l => fun x y => if (decision ((x,y) el l)) then true else false) (allPairs xs ys).


Axiom FunExt : forall (X  Y: Type), forall (f g : X -> Y), f = g <-> forall x, f x = g x.
Axiom PropExt : forall (X : Type), forall (P Q : X ->  X -> Prop), P = Q <-> forall x y, P x y <-> Q x y.

Lemma all_funs_contained (X  Y: Type) (x_eq_dec : forall x y : X, dec (x = y)) (y_eq_dec : forall x y : Y, dec (x = y)) (xs : list X) (ys : list Y) : 
forall (f : X -> Y -> bool), (forall x y, f x y = true -> x el xs /\ y el ys) -> f el allFuns xs ys.
Proof.
  intros f A.
  assert (exists l,  (exists ks, ks el allPairs xs ys /\ ks === l) /\ forall x y, (x, y) el l <-> f x y = true).
  { assert (forall x : X * Y, dec ((fun u : X * Y => let (a, b) := u in f a b = true) x)). 
    { intros. destruct x as [a b]. destruct (f a b); firstorder. }
    exists (filter (fun u : X * Y => match u with pair a b => f a b = true end) (list_prod xs ys)) .
    intros. repeat split.
    - unfold allPairs. apply power_incl'. auto. intros x B. apply in_filter_iff in B. tauto.
    - intros B; apply in_filter_iff in B. tauto.
    - intros B; apply in_filter_iff. split; try now auto. apply in_prod_iff; firstorder. }
  unfold allFuns. apply in_map_iff. destruct H as [l  [[ks [B C]] D]B]. exists ks. split; simpl in *.
  - apply FunExt. intros. apply FunExt. intros. specialize (D x x0). unfold equi in C.  unfold incl in C.
    decide ((x, x0) el ks); destruct (f x x0); firstorder; congruence.
  - auto.
Qed.


Lemma allPairsIncl (X  Y: Type) {x_eq_dec : forall x y : X, dec (x = y)} 
           {y_eq_dec : forall x y : Y, dec (x = y)} (xs : list X) (ys : list Y) l: 
      l el allPairs xs ys -> forall x y, (x,y) el l -> x el xs /\ y el ys.
Proof.
  intros A x y B. unfold allPairs in A. apply power_incl in A. unfold incl in A. specialize (A _ B).
  apply in_prod_iff in A; easy.  
Qed.



Lemma list_exists_dec' (X : Type) (x : X) xs P : (forall x : X, x el xs -> dec (P x)) -> dec (exists x , x el xs /\ P x).
Proof.
   induction xs; intros A.
   - simpl. right; firstorder. 
   - assert (H : dec (P a)). { apply A; auto. } destruct H. 
     + left; exists a; auto.
     + cut (dec (exists x, x el xs /\ P x)).
       { intros [B|B].
         - left; firstorder. 
         - right; intros C; firstorder; congruence. }
       apply IHxs; eauto.
Qed.


Lemma dom_dom'_incl g : dom g <<= dom' g.
Proof.
  intros x A. right; auto.
Qed.

Hint Resolve dom_dom'_incl. 

Section bisimDec.

Variable g1 g2 : Graph.

Lemma bisimDecElmem (P : g1 -> g2 -> bool) :
      dec (forall x, x el dom' g1 -> forall y, y el dom' g2 ->  P x y = true ->
       (forall x', x' el dom' g1 -> E x x' = true -> exists y', y' el dom' g2 /\ E y y' = true /\ P x' y' = true) /\
       (forall y', y' el dom' g2 -> E y y' = true -> exists x', x' el dom' g1 /\ E x x' = true /\ P x' y' = true)).
Proof.
  intros. auto. 
Qed.


Lemma lt_corr (P : g1 -> g2 -> bool) :
    (forall x y, P x y = true -> x el dom' g1 /\ y el dom' g2) ->
    ((forall x, x el dom' g1 -> forall y, y el dom' g2 ->  P x y = true ->
       (forall x', x' el dom' g1 -> E x x' = true -> exists y', y' el dom' g2 /\ E y y' = true /\ P x' y' = true) /\
       (forall y', y' el dom' g2 -> E y y' = true -> exists x', x' el dom' g1 /\ E x x' = true /\ P x' y' = true))
    <-> (forall x y, P x y = true -> 
          (forall x', E x x' = true -> exists y', E y y' = true /\ P x' y' = true) /\
          (forall y', E y y' = true -> exists x', E x x' = true /\ P x' y' = true))).
Proof.
  intros; split; intros.
  - split; intros.
    + assert (x el dom' g1 /\ y el dom' g2). { apply H. auto. } destruct H3 as [A B]. specialize (H0 _ A _ B H1).
      destruct H0 as [C D]. assert (x' el dom' g1). { destruct (E_in_dom H2). apply dom_dom'_incl; auto. }
      specialize (C _ H0 H2).  destruct C as [y' [I [J K]]]. exists y'. split; auto.
    + assert (x el dom' g1 /\ y el dom' g2). { apply H. auto. } destruct H3 as [A B]. specialize (H0 _ A _ B H1).
      destruct H0 as [C D]. assert (y' el dom' g2). { destruct (E_in_dom H2). apply dom_dom'_incl. auto. } specialize (D _ H0 H2).
      destruct D as [x' [I [J K]]]. exists x'. split; auto.
  - split; intros.
    + specialize (H0 _ _ H3). destruct H0 as [A B]. specialize (A _ H5). destruct A as [y' [C D]]; exists y'; split; auto.
      destruct (E_in_dom C); apply dom_dom'_incl; auto.
    + specialize (H0 _ _ H3). destruct H0 as [A B]. specialize (B _ H5). destruct B as [x' [C D]]; exists x'; split; auto.
      destruct (E_in_dom C); apply dom_dom'_incl; auto.
Qed.


Lemma is_P_bisim_dec (P : g1 -> g2 -> bool) : 
    (forall x y, P x y = true -> x el dom' g1 /\ y el dom' g2) -> dec (isBisim P).
Proof.
  intros A.
  cut ( dec (forall x y, P x y = true -> 
          (forall x', E x x' = true -> exists y', E y y' = true /\ P x' y' = true) /\
          (forall y', E y y' = true -> exists x', E x x' = true /\ P x' y' = true))).
  - intros [E|E]. 
    + left. constructor; intros; eauto. 
    + right; intros F. destruct F; tauto.
 - cut (dec (forall x, x el dom' g1 -> forall y, y el dom' g2 ->  P x y = true ->
       (forall x', x' el dom' g1 -> E x x' = true -> exists y', y' el dom' g2 /\ E y y' = true /\ P x' y' = true) /\
       (forall y', y' el dom' g2 -> E y y' = true -> exists x', x' el dom' g1 /\ E x x' = true /\ P x' y' = true))).
    + intros [E|E]. 
     * left. apply (lt_corr A). firstorder.
     * right. intros F. apply E. apply (lt_corr A). auto.
    + auto.
Qed.



Definition p_on_dom' P := (fun x y => if (decision (x el dom' g1 /\ y el dom' g2)) then P x y else false).

Lemma bisim_on_dom' : forall (P : g1 -> g2 -> bool), isBisim P -> isBisim (p_on_dom' P).
Proof.
  intros.  unfold p_on_dom'.  constructor. intros; split; intros.
   - decide (x el dom' g1 /\ y el dom' g2).
     + destruct a as [A B]. destruct H. specialize (H _ _ H0).
         destruct H as [C D]. specialize (C _ H1). destruct C as [y' [E F]]; exists y'; split; auto.
         rewrite decision_done. auto. unfold dom'. split; right; eapply E_in_dom; eauto.
     + destruct n. discriminate.
  - decide (x el dom' g1 /\ y el dom' g2). 
    + destruct a as [A B]. destruct H. specialize (H _ _ H0).
         destruct H as [C D]. specialize (D _ H1). destruct D as [x' [E F]]; exists x'; split; auto.
         rewrite decision_done. auto. split; right; eapply E_in_dom; eauto.
    + destruct n. discriminate.
Qed.

Lemma p_on_dom'_limited P : (forall x y, (p_on_dom' P) x y = true -> x el dom' g1 /\ y el dom' g2).
Proof.
  intros. unfold p_on_dom' in H. decide (x el dom' g1 /\ y el dom' g2); congruence.
Qed.

Definition all_bisims := (allFuns (dom' g1) (dom' g2)).

Lemma finitely_many_bisim :
   forall (P : g1 -> g2 -> bool), isBisim P -> (p_on_dom' P) el all_bisims /\ isBisim (p_on_dom' P).
Proof. 
 intros.  assert (isBisim (p_on_dom' P)). { apply (bisim_on_dom' H). } split; auto.
 apply all_funs_contained. apply p_on_dom'_limited.
Qed.


Lemma all_bisims_limited_dom P : P el all_bisims -> forall x y, P x y = true -> x el dom' g1 /\ y el dom' g2.
Proof. 
  unfold all_bisims. unfold allFuns. intros. apply in_map_iff in H. 
  destruct H as [l [C D]]. subst P. apply allPairsIncl with (l := l); auto.
  decide ((x,y) el l); congruence.
Qed.


End bisimDec.



Instance tree_equiv_Equivalence : 
  Equivalence bisim.
Proof. 
  constructor; hnf.
  - apply bisimRefl.
  - apply bisimSym.
  - apply bisimTrans.
Qed.


Instance graph_bisim_dec (g1 g2 : Graph) : dec (bisim g1 g2).
Proof.
  pose (l := all_bisims g1 g2). 
  assert (D : forall (P : g1 -> g2 -> bool), isBisim P ->  
       (p_on_dom' P) el (all_bisims g1 g2) /\ isBisim (p_on_dom' P)).
  { apply finitely_many_bisim. }
  assert (E : forall P, P el (all_bisims g1 g2) -> forall x y, P x y = true -> x el dom' g1 /\ y el dom' g2).
  { intros P. apply all_bisims_limited_dom. }
  unfold bisim.
    cut (dec (exists P, P el l /\ isBisim P /\ P (root g1) (root g2) = true)).
   { intros [A|A].
     - left. firstorder. 
     - right. intros C. apply A. destruct C as [P [I J]]. specialize (D P I). destruct D as [D1 D2].
       specialize (E _ D1).  exists (p_on_dom' P). split; auto. split; auto.
       unfold p_on_dom'. rewrite decision_done; auto. split; left; auto. 
   }
   apply list_exists_dec'. firstorder. intros P A. apply and_dec. 
   - subst l.  specialize (E _ A). apply (is_P_bisim_dec E).
   - auto. 
Qed.


Section Isom.
Variable X Y : Type.
Variable f : X -> Y.

Definition iso := exists f', (forall x, f' (f x) = x) /\ (forall y, f (f' y) = y).

Variable xs : list X.
Variable ys : list Y.
Definition iso_on := exists f', (forall x, x el xs -> f' (f x) = x) /\ (forall y, y el ys -> f (f' y) = y).

Lemma iso_general_on : iso -> iso_on.
Proof.
  firstorder.
Qed.

End Isom.

Section BisimIsom.

Variable g1 g2 : Graph.
Variable f : g1 -> g2.

Definition mutated := 
    map f (dom g1) === dom g2 /\ 
    f (root g1) = root g2 /\
    forall (x y : g1), E x y = true <-> E (f x) (f y) = true. 

Lemma bisimIsom : iso_on f (dom g1) (dom g2) -> mutated -> bisim g1 g2.
Proof.
  intros [f' [A B]] [C1 [C2 C3]]. exists (fun x y => eqb (f x) y). split; [constructor|].
  - intros; split; intros.
    + exists (f x'). rewrite eqb_iff in H. subst y. split. 
      * apply C3. auto.
      * apply eqb_iff; auto.
    + exists (f' y'). rewrite eqb_iff in H. subst y. rewrite B. split.
      * apply <- C3. rewrite B; auto. eapply E_in_dom; eauto.
      * apply eqb_iff; auto.
      * eapply E_in_dom; eauto.
 - apply eqb_iff; auto.
Qed.

End BisimIsom.

