Require Import TreeSim.

Lemma TreeInduction (P : Tree -> Prop) :
  (forall s , (forall t, In t (tree_to_list s) -> P t) -> P s) -> forall s, P s.
Proof.
  intros A s.
  assert (G : forall v u, In u (tree_to_list v) -> P u).
  { clear s. intros v. induction v.
   - intros u B. contradiction.
   - intros u B. simpl in B; destruct B as [B|B].
     + subst. apply A; assumption.
     + firstorder. }
  apply G with (v := s.:s). simpl; auto.
Qed.


CoInductive TreeBisim : Tree -> Tree -> Prop :=
  |CoBisim s t :
    (forall s', In s' (tree_to_list s) -> exists2 t', In t' (tree_to_list t) & TreeBisim s' t') -> 
    (forall t', In t' (tree_to_list t) -> exists2 s', In s' (tree_to_list s) & TreeBisim t' s') -> 
    TreeBisim s t.

Lemma TreeCoInd (R : Tree -> Tree -> Prop) : 
  (forall s t, R s t ->
    (forall s', In s' (tree_to_list s) -> exists2 t', In t' (tree_to_list t) & R s' t') /\
    (forall t', In t' (tree_to_list t) -> exists2 s', In s' (tree_to_list s) & R t' s') ) ->
   forall s t, R s t -> TreeBisim s t.
Proof.
  cofix. intros A s t B. constructor.
   - intros s' C. destruct (A s t B). destruct (H s' C). exists x. assumption. apply TreeCoInd; assumption.
   - intros s' C. destruct (A s t B). destruct (H0 s' C). exists x. assumption. apply TreeCoInd; assumption.
Qed.

Lemma BisimInList s s' : In s' (tree_to_list s) -> TreeBisim s' s'.
Proof.
  revert s'; induction s.
  - intros s' A; contradiction A.
  - intros s' A. simpl in A; destruct A.
    + subst. constructor; intros x B; exists x;  try tauto; apply (IHs1 x B).
    + apply (IHs2 _ H).
Qed.


Lemma BisimRefl s : TreeBisim s s.
Proof.
  constructor; intros x A; exists x; try tauto; apply (@BisimInList s x ); assumption.
Qed.

Lemma BisimSym s t : TreeBisim s t -> TreeBisim t s.
Proof.
  intros A; inv A; constructor; assumption.
Qed.

Lemma BisimDel s t : TreeBisim (s .: s .: t) (s .: t).
Proof.
  constructor; intros x B.
   - simpl in B; destruct B as [B | [B | B]].
    + subst. exists x; simpl; eauto using BisimRefl.
    + subst. exists x; simpl; eauto using BisimRefl.
    + exists x; simpl; eauto using BisimRefl.
   - simpl in B; destruct B as [B | B].
    + subst; exists x; simpl; eauto using BisimRefl.
    + exists x; simpl; eauto using BisimRefl. 
Qed.

Lemma BisimSwap s t u : TreeBisim (s .: t .: u) (t .: s .: u).
Proof.
  constructor; intros x B; simpl in B; repeat destruct B; exists x; simpl; eauto using BisimRefl; try tauto.
Qed.

Lemma BisimComp s s' t t' : TreeBisim s s' -> TreeBisim t t' -> TreeBisim (s .: t) (s' .: t').
Proof.
  constructor; intros x B. simpl in B; destruct B as [B|B].
   - subst. exists s'; try tauto. simpl; auto.
   - inv H0. destruct (H1 x B). exists x0; simpl; try tauto.
   - simpl in B; destruct B as [B|B].
    + subst; exists s; simpl; try tauto. apply (BisimSym H).
    + inv H0. destruct (H2 _ B). exists x0; simpl; try tauto.
Qed.

(*
Lemma BisimStep s t : tree_step s t -> TreeBisim s t.
Proof with eauto using BisimRefl, BisimComp.
  intros A.
  induction A...
  - apply BisimDel.
  - apply BisimSwap.
Qed.
*)

Lemma BisimTrans s t u : TreeBisim s t -> TreeBisim t u -> TreeBisim s u.
Proof.
  intros A B.
  apply TreeCoInd with (R := fun s u => exists2 v, TreeBisim s v & TreeBisim v u).
  - clear s t u A B. intros s t [v A B]. split; intros x C.
   + destruct A, B. destruct (H _ C) as [y D E]. destruct (H1 _ D). eauto 10.
   + destruct A, B. destruct (H2 _ C) as [y D E]. destruct (H0 _ D). eauto 10.
  - eauto.
Qed.


Lemma EquivBisim s t : tree_equiv s t -> TreeBisim s t.
Proof with eauto using BisimRefl, BisimSwap, BisimDel, BisimSym, BisimComp, BisimTrans.
  intros A; induction A...
Qed.

Lemma BisimDoubleIncl : forall s t, TreeBisim s t -> tree_subset s t /\ tree_subset t s.
Proof.
  refine (TreeInduction _). intros. inv H0. split.
  - apply tree_subset_char. intros s' A. apply tree_elem_char in A. destruct A as [x [B C]].
    specialize (H1 x B). destruct H1 as [y D E]. apply tree_elem_char. 
    destruct (H x B y E) as [subs1 subs2]. exists y. split; auto.
    rewrite C. now apply double_incl.
  - apply tree_subset_char. intros s' A. apply tree_elem_char in A. destruct A as [y [D E]].
    specialize (H2 y D). destruct H2 as [x B C]. apply tree_elem_char. apply BisimSym in C.
    destruct (H x B y C) as [subs1 subs2]. exists x. split; auto. rewrite E.
    now apply double_incl.
Qed.

Lemma BisimEquiv s t : TreeBisim s t -> tree_equiv s t.
Proof.
  intros H; apply BisimDoubleIncl in H; apply TreeEquiv, double_incl; intuition.
Qed.