Require Import Omega.
Require Export Base.

Inductive Tree :=
|empty : Tree
|comp : Tree -> Tree -> Tree.

Implicit Types s t : Tree.

Notation "s .: t" := (comp s t) (at level 60, right associativity) .

Instance tree_eq_dec s t : dec (s = t).
Proof.
  unfold dec. repeat decide equality.
Qed.

(* General tree functions and lemmas *)

Fixpoint size t :=
  match t with
   |empty => 0
   |(s1 .: s2) => size s1 + size s2 + 1
  end.


Fixpoint tree_append s t :=
  match s with 
   |empty => t
   |(s1 .: s2) => (s1 .: (tree_append s2 t)) 
  end.


Definition tree_to_list : Tree -> list Tree :=
  fix f s := match s with 
   | empty => nil
   | (comp s' t) => s' :: (f t)
  end.

Lemma tree_append_list s t :
   tree_to_list (tree_append s t) = (tree_to_list s) ++ (tree_to_list t).
Proof.
   revert t. induction s; intros; simpl; congruence.
Qed.

Fixpoint list_to_tree l :=
  match l with 
   | nil => empty
   | (cons a  l') => a .: (list_to_tree l')
  end.

Lemma tree_list_id s : s = (list_to_tree (tree_to_list s)).
Proof.
  induction s; simpl; congruence.
Qed.

Lemma list_tree_id l : l = (list_to_tree (tree_to_list l)).
Proof.
  induction l; simpl; congruence.
Qed.

Lemma tree_list_append ss ts :
   list_to_tree (ss ++ ts) = tree_append (list_to_tree ss) (list_to_tree ts).
Proof.
  induction ss; simpl in *; [|rewrite IHss]; auto.
Qed.


(* Original tree_equiv *)

Inductive tree_equiv : Tree -> Tree -> Prop :=
  |equivEmpty : tree_equiv empty empty
  |equivDel s t : tree_equiv (s .: s .: t) (s .: t)
  |equivSwap s t u : tree_equiv (s .: t .: u) (t .: s .: u)
  |equivSym s t : s <> empty -> t <> empty -> tree_equiv s t -> tree_equiv t s
  |equivComp s s' t t' : tree_equiv s s' -> tree_equiv t t' -> tree_equiv (s .: t) (s' .: t')
  |equivTrans s t u : tree_equiv s t -> tree_equiv t u -> tree_equiv s u.


Definition elem s t : Prop := tree_equiv t (comp s t).


Lemma tree_equiv_id s : tree_equiv s s.
Proof with eauto using tree_equiv.
  induction s...
Qed.


Lemma tree_equiv_empty s : tree_equiv s empty -> s = empty.
Proof.
  intros A. remember empty as t. induction A; try congruence.
  rewrite IHA1; rewrite IHA2; congruence.
Qed.

Lemma tree_equiv_empty' s : tree_equiv empty s -> s = empty.
Proof.
  intros A. remember empty as t. induction A; try congruence.
  rewrite IHA2; rewrite IHA1; congruence.
Qed.

Lemma tree_equiv_sym s t : tree_equiv s t -> tree_equiv t s.
Proof with eauto using tree_equiv.
  induction 1; simpl... constructor; try congruence...
Qed.


Lemma tree_equiv_trans s t u : tree_equiv s t -> tree_equiv t u -> tree_equiv s u.
Proof.
  apply equivTrans; assumption.
Qed.


Instance tree_equiv_Equivalence : 
  Equivalence tree_equiv.
Proof. 
  constructor; hnf.
  - apply tree_equiv_id.
  - apply tree_equiv_sym.
  - apply tree_equiv_trans.
Qed.


Instance comp_tree_equiv_proper : 
  Proper (tree_equiv ==> tree_equiv ==> tree_equiv) comp.
Proof. 
  cbv. eauto using tree_equiv.
Qed.


Definition tree_sim (R : Tree -> Tree -> Prop) s t : Prop :=
   forall s', s' el (tree_to_list s) -> exists t', t' el tree_to_list t /\ R s' t'.

Theorem tree_equiv_list s t :
tree_equiv s t -> tree_sim tree_equiv s t /\ tree_sim tree_equiv t s.
Proof with eauto using tree_equiv.
  intros A. induction A.
  - split; intros s B; simpl in *; contradiction.
  - split; intros s' A; exists s'; split; firstorder. 
  - split; intros s' A; exists s'; split; simpl; firstorder.
  - split; intros [B|B]; intuition. 
  - split.
   { intros x [B|B]. 
    - subst. exists s'. split; simpl; auto.
    - apply IHA2 in B as [u [B C]]. exists u; firstorder. }
   intros x [B|B].
   + subst. exists s. split; simpl; intuition...
   + destruct IHA2 as [C D]. destruct IHA1 as [E F].
     destruct (D x B) as [y [G1 G2]].
     exists y. split; simpl...
  - split.
   + intros s' B. destruct IHA1 as [C1 C2]. destruct IHA2 as [D1 D2]. 
     destruct (C1 s' B) as [y [E1 E2]]. destruct (D1 y E1) as [z [F1 F2]].
     exists z. split... 
   + intros t' B. destruct IHA1 as [C1 C2]. destruct IHA2 as [D1 D2].
     destruct (D2 t' B) as [y [E1 E2]]. destruct (C2 y E1) as [z [F1 F2]].
     exists z. split...
Qed.


Lemma tree_equiv_append s s' t t' :
   tree_equiv s s' -> tree_equiv t t' -> tree_equiv (tree_append s t) (tree_append s' t').
Proof with eauto using tree_equiv; try reflexivity.
  intros A. revert t t'. induction A; simpl...
  - intros u v B. rewrite equivDel. 
    apply equivComp; [reflexivity|]. induction t; simpl... apply equivComp...
  - intros x y A. rewrite equivSwap.
    repeat apply equivComp; try reflexivity.
    induction u; simpl... apply equivComp... 
  - intros x y B. symmetry. apply IHA. symmetry; auto.
  - intros x y B. rewrite IHA1; try reflexivity.
    rewrite IHA2...
Qed.

(* step equiv *)

Inductive tree_step : Tree -> Tree -> Prop :=
  |stepDel : forall s t, tree_step (s .: s .: t) (s .: t)
  |stepSwap : forall s t u, tree_step (s .: t .: u) (t .: s .: u)
  |stepCompL : forall s s' t, tree_step s s' -> tree_step (s .: t) (s' .: t)
  |stepCompR : forall s t t', tree_step t t' -> tree_step (s .: t) (s .: t').

Inductive tree_step_equiv : Tree -> Tree -> Prop :=
  |equivRefl s : tree_step_equiv s s
  |equivLeft s t u: tree_step s t -> tree_step_equiv t u ->  tree_step_equiv s u
  |equivRight s t u : tree_step t s -> tree_step_equiv t u -> tree_step_equiv s u.


Lemma step_equiv s t :tree_step s t -> tree_step_equiv s t.
Proof.
   intros A. apply equivLeft with (t := t); firstorder; constructor.
Qed.


Lemma equivStepCompL s t u : tree_step_equiv t u -> tree_step_equiv (s .: t) (s .: u).
Proof with eauto using tree_step, tree_step_equiv.
  intros A; revert s; induction A; intros; simpl...
Qed.

Lemma equivStepCompR s t u : tree_step_equiv s t -> tree_step_equiv (s .: u) (t .: u).
Proof with eauto using tree_step, tree_step_equiv.
  intros A; revert u; induction A; intros; simpl...
Qed.


Lemma tree_step_equiv_comp s s' t t' :
   tree_step_equiv s s' -> tree_step_equiv t t' -> tree_step_equiv (s .: t) (s' .: t').
Proof with eauto using tree_step, tree_step_equiv. 
  intros A B. induction A; simpl... 
  apply equivStepCompL. assumption.
Qed.

Lemma tree_step_equiv_trans s t u : tree_step_equiv s t -> tree_step_equiv t u -> tree_step_equiv s u.
Proof with eauto using tree_step_equiv, tree_step.
  intros A B; induction A; simpl... 
Qed.

Lemma tree_step_equiv_empty_backw s : tree_step_equiv empty s -> s = empty.
Proof with eauto using tree_step_equiv, tree_step.
  intros A. remember empty as t. induction A; simpl...
  - destruct H; discriminate.
  - destruct H; discriminate.
Qed.

Lemma step_equiv_backw s t: tree_step s t -> tree_step_equiv t s.
Proof with eauto using tree_step, tree_step_equiv.
  intros A...
Qed.

Lemma tree_step_equiv_sym s t : tree_step_equiv s t -> tree_step_equiv t s.
Proof with eauto using tree_step, tree_step_equiv, tree_step_equiv_trans, step_equiv_backw.
  intros A; induction A; simpl...
Qed.

Instance tree_step_equiv_Equivalence : 
  Equivalence tree_step_equiv.
Proof with eauto using tree_step_equiv. 
  constructor; hnf.
  - intros; constructor.
  - apply tree_step_equiv_sym.
  - apply tree_step_equiv_trans.
Qed.


Instance comp_tree_step_equiv_proper : 
  Proper (tree_step_equiv ==> tree_step_equiv ==> tree_step_equiv) comp.
Proof. 
  cbv. intros. apply tree_step_equiv_comp; auto. 
Qed.

Instance comp_tree_step_tree_step_equiv_proper : 
  Proper (tree_step ==> tree_step_equiv ==> tree_step_equiv) comp.
Proof with eauto using tree_step_equiv, tree_step.
  cbv; intros. eapply equivRight... rewrite H0...
Qed.

Instance comp_tree_step_equiv_tree_step_proper : 
  Proper (tree_step_equiv ==> tree_step ==> tree_step_equiv) comp.
Proof with eauto using tree_step_equiv, tree_step.
  cbv; intros. eapply equivRight... rewrite H...
Qed.

Lemma tree_step_equiv_empty s : tree_step_equiv s empty -> s = empty.
Proof with eauto using tree_step, tree_step_equiv.
  intros A. remember empty as t. induction A; subst; simpl...
  - specialize (IHA eq_refl). destruct H; discriminate.
  - specialize (IHA eq_refl). destruct H; discriminate.
Qed.



(*Equivalence of tree_equiv and tree_step_equiv *)

Lemma tree_step_tree_equiv s t : tree_step s t -> tree_equiv s t.
Proof with eauto using tree_step, tree_equiv.
  intros A; induction A...
  - rewrite IHA. reflexivity.
  - rewrite IHA; reflexivity. 
Qed.

Theorem TreeEquiv s t: tree_equiv s t <-> tree_step_equiv s t.
Proof with eauto using tree_equiv, tree_step, tree_step_equiv; try firstorder.
  split; intros A; induction A...
  - rewrite IHA1, IHA2. reflexivity.
  - rewrite IHA1; apply IHA2.
  - apply tree_step_tree_equiv in H. rewrite H; auto.
  - apply tree_step_tree_equiv in H. rewrite <- IHA; symmetry; auto. 
Qed.

Lemma tree_step_equiv_list s t : tree_step_equiv s t -> tree_sim tree_step_equiv s t /\ tree_sim tree_step_equiv t s.
Proof with eauto using tree_step_equiv, tree_equiv, TreeEquiv.
  intros A. apply TreeEquiv, tree_equiv_list in A as [A B].
  split; intros s' H.
  - destruct (A s' H) as [x [D E]]. exists x. split; [|apply TreeEquiv]...
  - destruct (B s' H) as [x [D E]]. exists x. split; [|apply TreeEquiv]...
Qed.

Lemma tree_step_equiv_sim s t : tree_step_equiv s t -> tree_sim tree_step_equiv s t.
Proof.
  intros A; destruct (tree_step_equiv_list A); firstorder; tauto.
Qed.



Lemma tree_step_equiv_append s s' t t' :
  tree_step_equiv s s' -> tree_step_equiv t t' -> tree_step_equiv (tree_append s t) (tree_append s' t').
Proof.
  intros A B. apply TreeEquiv, tree_equiv_append; now apply TreeEquiv.
Qed.
