Require Export Tree.

(* Order and sorting *) 

Inductive Order := LT | EQ | GT.

Fixpoint tree_cmp s t :=
  match s,t with 
  |empty, empty => EQ
  |empty, _ => LT
  |_, empty => GT
  |(s1 .: s2) , (t1 .: t2) => 
     match (tree_cmp s1 t1) with
     | EQ => tree_cmp s2 t2
     | x => x end 
  end.

Lemma tree_cmp_eq_equal s t : tree_cmp s t = EQ -> s = t.
Proof.
  revert t; induction s; intros t A; destruct t; simpl in *; try congruence.
  destruct (tree_cmp s1 t1) eqn:E; try congruence. f_equal; eauto.
Qed.

Lemma tree_cmp_equal_eq s : tree_cmp s s = EQ.
Proof.
  induction s; simpl; [congruence|]. now rewrite IHs1.
Qed.
 
Lemma not_lt_empty s : not (tree_cmp s empty = LT).
Proof.
  induction s; intros A; inv A.
Qed.

Lemma cmp_lt_rev s t : tree_cmp s t = LT -> tree_cmp t s = GT.
Proof with try congruence.
  revert s; induction t; intros [|s1 s2] A; simpl in *...
  destruct (tree_cmp t1 s1) eqn:E...
  - destruct (tree_cmp s1 t1) eqn:F...
    + specialize (IHt1 _ F)...
    + rewrite (tree_cmp_eq_equal F) in E, F...
  - apply tree_cmp_eq_equal in E. subst. rewrite tree_cmp_equal_eq in A. auto.

Qed.

Lemma cmp_gt_rev s t : tree_cmp s t = GT -> tree_cmp t s = LT.
Proof.
  revert t; induction s; intros [|t1 t2] A; simpl in *; try congruence.
  destruct (tree_cmp t1 s1) eqn:E; try congruence. 
  - apply tree_cmp_eq_equal in E; subst. rewrite tree_cmp_equal_eq in A. auto.
  - destruct (tree_cmp s1 t1) eqn:F; try congruence.
    + apply tree_cmp_eq_equal in F. subst. rewrite IHs1 in E; eauto.
    + apply IHs1 in F. congruence.
Qed.

Lemma cmp_trans s t u : tree_cmp s t = LT -> tree_cmp t u = LT -> tree_cmp s u = LT.
Proof with try congruence.
  revert t u. induction s; intros [|t1 t2] [|u1 u2] A B; simpl in *...
  destruct (tree_cmp s1 t1) eqn:E...
  - destruct (tree_cmp t1 u1) eqn:F... 
    + erewrite IHs1; eauto.
    + apply tree_cmp_eq_equal in F; subst. rewrite E; auto.
  - apply tree_cmp_eq_equal in E; subst. destruct (tree_cmp t1 u1) eqn:F...
    apply tree_cmp_eq_equal in F; subst. firstorder.
Qed.


Fixpoint insert s t : Tree := match t with
  |empty => s .: empty
  |(t1 .: t2) => match (tree_cmp s t1) with
    | EQ => t1 .: t2
    | LT => s .: t1 .: t2
    | GT => t1 .: insert s t2 end 
  end.


Fixpoint sort s: Tree :=
  match s with 
   |empty => empty
   |(s1 .: s2) => insert (sort s1) (sort s2) 
  end.


Lemma insert_equiv s t : tree_step_equiv (s .: t) (insert s t).
Proof with eauto using tree_step, tree_step_equiv.
  revert s. induction t; intros s; simpl...
  destruct (tree_cmp s t1) eqn:E...
  - apply tree_cmp_eq_equal in E; subst...
  - apply tree_step_equiv_trans with (t := t1 .: s .: t2)... rewrite IHt2...
Qed.

Theorem sort_equiv s: tree_step_equiv s (sort s).
Proof with eauto using tree_step, tree_step_equiv, tree_step_equiv_comp, insert_equiv. 
  induction s; simpl...
  apply tree_step_equiv_trans with (t := (sort s1) .: (sort s2))...
Qed.
 
Lemma del_sort_equal s t : sort (s .: s .: t) = sort ( s .: t).
Proof with try congruence; eauto. 
  simpl. remember (sort s ) as x; remember (sort t) as y. 
  clear Heqx Heqy. revert x. clear s t. induction y; intros x; [simpl|]...
  - now rewrite tree_cmp_equal_eq.
  - simpl. destruct (tree_cmp x y1) eqn:E; simpl. (* [|rewrite E|rewrite E]... *)
    now rewrite tree_cmp_equal_eq. + now rewrite E. +rewrite E. now rewrite IHy2.  
Qed.

Lemma swap_sort_equal s t u: sort (s .: t .: u) = sort (t .: s .: u).
Proof with try congruence; eauto using cmp_trans.
  simpl. remember (sort s) as x; remember (sort t) as y; remember (sort u) as z.
  clear Heqx Heqy Heqz s t u. 
  revert x y. 
 induction z; intros x y; simpl.
  - destruct (tree_cmp x y) eqn:E.
   + now rewrite (cmp_lt_rev E). 
   + rewrite (tree_cmp_eq_equal E). now rewrite (tree_cmp_equal_eq).
   + now rewrite (cmp_gt_rev E).
  - destruct (tree_cmp y z1) eqn:E.
   + { destruct (tree_cmp x z1) eqn:F; simpl; rewrite E.
       - destruct (tree_cmp x y) eqn:G.
         + now rewrite (cmp_lt_rev G).
         + now rewrite (tree_cmp_eq_equal G); rewrite tree_cmp_equal_eq. 
         + rewrite (cmp_gt_rev G). now rewrite F.
       - destruct (tree_cmp x y) eqn:G; try rewrite F...
         apply tree_cmp_eq_equal in F; subst. apply cmp_lt_rev in E...
       - rewrite F; destruct (tree_cmp x y) eqn:G...
         + assert (tree_cmp x z1 = LT)...
         + apply tree_cmp_eq_equal in G; subst...
      } 
   + destruct (tree_cmp x z1) eqn:F; simpl; rewrite E, F...
     apply tree_cmp_eq_equal in E; subst. rewrite (cmp_lt_rev F)...
   + simpl. destruct (tree_cmp x z1) eqn:F; simpl; try rewrite E...
     simpl; destruct (tree_cmp y x) eqn:G...
     * assert (tree_cmp y z1 = LT)...
     * apply tree_cmp_eq_equal in G; subst...
Qed.

Lemma step_sort_equal s t : tree_step s t -> sort s = sort t.
Proof with firstorder using del_sort_equal, swap_sort_equal; congruence.
  intros A; induction A; try rewrite IHA; simpl...
Qed.

Lemma tree_step_equiv_equal s t: tree_step_equiv s t -> sort s = sort t.
Proof with firstorder using step_sort_equal; congruence.
  intros A; induction A; try rewrite <- IHA...
Qed.

Theorem tree_step_equiv_dec s t : dec (tree_step_equiv s t).
Proof.
  decide (sort s = sort t).
  - left. rewrite sort_equiv. rewrite e. symmetry; apply sort_equiv.
  - right. intros A. apply n. exact (tree_step_equiv_equal A).
Qed.

