Require Export TreeOrder.

Definition tree_elem s t := tree_step_equiv t (s .: t).

Lemma sort_idem s : sort(sort s) = sort s.
Proof.
  apply tree_step_equiv_equal. symmetry. apply sort_equiv.
Qed.

Lemma elem_char s t : tree_elem s t -> exists t', In t' (tree_to_list t) /\ tree_step_equiv s t'.
Proof with eauto using sort_equiv. 
  intros A. destruct (tree_step_equiv_list A). unfold tree_sim in H0.
  destruct (H0 s) as [x [B C]]... simpl...
Qed.

Lemma list_elem_tree_elem s t : s el tree_to_list t -> tree_elem s t.
Proof.
  revert s; induction t; intros s A; simpl in *; [tauto|]. destruct A.
  - subst. unfold tree_elem. symmetry. apply TreeEquiv; constructor.
  - specialize (IHt2 _ H). unfold tree_elem in *. rewrite IHt2 at 1. 
    apply TreeEquiv. constructor.
Qed.

Lemma elem_char_backw s t : ( exists t', In t' (tree_to_list t ) /\ tree_step_equiv s t') -> tree_elem s t.
Proof.
  intros [t' [A B]]. induction B.
  - apply (list_elem_tree_elem A).
  - specialize (IHB A). unfold tree_elem in *. apply step_equiv in H. 
    rewrite IHB at 1. now rewrite H.
  - specialize (IHB A). unfold tree_elem in *. apply step_equiv in H.
    rewrite IHB at 1. now rewrite H.
Qed.


Definition tree_subset s t := tree_step_equiv t (tree_append s t).

Lemma subs_char s t : tree_subset s t -> forall s', tree_elem s' s -> tree_elem s' t.
Proof with eauto using sort_equiv.
  intros A s' B. unfold tree_subset in A.
  destruct (tree_step_equiv_list A). destruct (elem_char B).
  apply elem_char_backw. destruct (H0 x). 
  - rewrite tree_append_list. intuition. 
  - exists x0. split; try tauto. intuition. now rewrite H4.
Qed.


Lemma subs_char_backw s t : (forall s', tree_elem s' s -> tree_elem s' t ) -> tree_subset s t.
Proof with eauto using tree_step_equiv, tree_step, tree_equiv.
  revert t; induction s; intros t A; unfold tree_subset; simpl...
  assert (tree_subset s2 t). { apply IHs2. intros s' B. apply A. 
     apply elem_char_backw. destruct (elem_char B). exists x; split; firstorder. } 
  unfold tree_subset in H. rewrite <- H.
  assert (tree_elem s1 t). 
  {apply A. apply  elem_char_backw. exists s1; split; simpl; try tauto. constructor. }
  unfold tree_elem in H0. auto.
Qed.

Theorem tree_elem_char s t : tree_elem s t <-> exists t', In t' (tree_to_list t) /\ tree_step_equiv s t'.
Proof with eauto using elem_char, elem_char_backw.
  split; intros...
Qed.

Theorem tree_subset_char s t : tree_subset s t <-> forall s', tree_elem s' s -> tree_elem s' t.
Proof with eauto using subs_char, subs_char_backw.
  split; intros...
Qed.

Lemma elem_rew_left s t u :
  tree_elem s t -> tree_step_equiv s u -> tree_elem u t.
Proof.
  intros A B. apply tree_elem_char in A as [x [C D]].
  apply tree_elem_char. exists x; split; try tauto.
  rewrite <- D. symmetry; auto.
Qed.

Lemma elem_rew_right s t u :
  tree_elem s t -> tree_step_equiv t u -> tree_elem s u.
Proof with eauto using tree_step_equiv_trans.
  intros A B.
  apply tree_elem_char. apply tree_elem_char in A as [x [C D]]. 
  destruct (tree_step_equiv_list B) as [B1 B2].
  destruct (B1 x C) as [v [E F]]. exists v; split...
Qed.


Lemma subs_rew_left s t u :
  tree_subset s t -> tree_step_equiv s u -> tree_subset u t.
Proof with eauto using tree_step_equiv_sym, tree_step_equiv, tree_step_equiv_trans.
  intros A B. apply tree_subset_char. intros u' C.
  destruct (tree_step_equiv_list B) as [B1 B2].
  apply tree_elem_char. apply tree_elem_char in C as [x [D E]].
  destruct (B2 x D) as [s' [F G]]. rewrite tree_subset_char in A.
  apply list_elem_tree_elem in F. apply A in F. apply tree_elem_char in F as [y [I J]]...
Qed.

Lemma subs_rew_right s t u:
  tree_subset s t -> tree_step_equiv t u -> tree_subset s u.
Proof with eauto using tree_step_equiv_trans, tree_step_equiv_sym.
  intros A B.  apply tree_subset_char. intros s' C. 
  rewrite tree_subset_char in A.
  apply A in C. apply tree_elem_char in C as [t' [D E]].
  apply tree_step_equiv_list in B as [B1 B2]. 
  destruct (B1 t' D) as [x [F G]]. apply elem_char_backw...
Qed.


Lemma append_equiv s t : tree_step_equiv (tree_append s t) (tree_append t s).
Proof with eauto using tree_step_equiv, tree_step_equiv_trans, tree_step_equiv_sym, tree_step_equiv_comp.
  revert t; induction s; intros t; induction t; simpl in *...
  rewrite IHs2. rewrite <- IHt2. rewrite IHs2. rewrite <- IHs2.
  apply tree_step_equiv_trans with (t := s1 .: t1 .: tree_append t2 s2)...
  apply TreeEquiv. econstructor; eauto.
Qed.


Lemma double_incl s t : tree_subset s t -> tree_subset t s -> tree_step_equiv s t.
Proof.
  intros. unfold tree_subset in *. rewrite H. rewrite H0 at 1. apply append_equiv.
Qed.

Lemma tree_sim_subs s t : tree_sim tree_step_equiv s t -> tree_subset s t.
Proof with eauto using tree_step_equiv_trans, tree_step_equiv_sym.
  intros A. apply tree_subset_char. intros s' B.
  apply tree_elem_char in B as [x [C D]].
  apply tree_elem_char. destruct (A _ C) as [y [E F]]...
Qed.

Theorem tree_sim_step_equiv s t :
tree_sim tree_step_equiv s t -> tree_sim tree_step_equiv t s -> tree_step_equiv s t.
Proof with eauto using double_incl, tree_sim_subs.
  intros A B...
Qed.
 

