Contribution: TreeDiameter

# Library TreeDiameter.TreeDiameter

Require Export Omega.
Require Export Arith.
Require Export List.
Require Export Wf_nat.

Section Paths.

Variable A : Set.
Definition graph := A->A->Prop.
Variable g : graph.

Inductive path : A -> A -> nat -> Prop :=
| path_nil : forall x, path x x 0
| path_cons : forall x1 x2 x3 n, g x1 x2 -> path x2 x3 n ->
path x1 x3 (S n).

Definition dist x y n :=
path x y n /\ forall m, path x y m -> n <= m.

Definition diameter n :=
(exists t1, exists t2, dist t1 t2 n) /\
(forall t1 t2 m, dist t1 t2 m -> m <= n).

Lemma path_trans : forall x y z n m,
path x y n -> path y z m -> path x z (n+m).
Proof.
induction 1; intros.
replace (0+m) with m; auto with *.
replace (S n+m) with (S (n+m)); auto with *.
apply path_cons with x2; auto.
Save.

Lemma path_1 : forall x y, g x y -> path x y 1.
Proof.
intros; apply path_cons with y; auto. apply path_nil.
Save.

Lemma path_snoc : forall x y z n, path x y n -> g y z -> path x z (S n).
Proof.
induction 1; intuition.
apply path_cons with z; auto.
apply path_nil.
apply path_cons with x2; auto.
Save.

Lemma path_sym :
(forall x y, g x y -> g y x) ->
forall n x y, path x y n -> path y x n.
Proof.
intro g_sym; induction 1.
apply path_nil.
apply path_snoc with x2; auto.
Save.

End Paths.
Implicit Arguments path [A].
Implicit Arguments dist [A].
Implicit Arguments diameter [A].
Hint Resolve path_sym path_1.
Hint Constructors path.

Inductive tree : Set :=
| Empty : tree
| Node : tree -> tree -> tree.

Inductive dir : Set := Left : dir | Right : dir.
Definition pos := list dir.

Inductive valid : tree -> pos -> Prop :=
| Vroot : forall t, valid t nil
| Vleft : forall l r p, valid l p -> valid (Node l r) (Left :: p)
| Vright : forall l r p, valid r p -> valid (Node l r) (Right :: p).

Hint Constructors valid.

Inductive adj : pos -> pos -> Prop :=
| Aleft1 : adj nil (cons Left nil)
| Aleft2 : adj (cons Left nil) nil
| Aright1 : adj nil (cons Right nil)
| Aright2 : adj (cons Right nil) nil
| Actx : forall d p1 p2, adj p1 p2 -> adj (d :: p1) (d :: p2).

Proof.
induction 1; auto.
Save.

Definition gt (t:tree) (p1 p2 : pos) : Prop :=
valid t p1 /\ valid t p2 /\ adj p1 p2.

Lemma gt_sym : forall t p1 p2, gt t p1 p2 -> gt t p2 p1.
Proof.
unfold gt; intuition.
Save.
Hint Resolve gt_sym.

Lemma gt_empty : forall t1 t2, ~(gt Empty t1 t2).
Proof.
red; intros.
inversion_clear H; intuition.
inversion H0; subst.
inversion H; subst.
inversion_clear H2.
Save.

Lemma path_gt_r: forall l r p1 p2 n,
path (gt r) p1 p2 n -> path (gt (Node l r)) (Right::p1) (Right::p2) n.
Proof.
induction 1; auto.
apply path_cons with (Right::x2); auto.
red in H; red; intuition.
Save.

Lemma path_gt_l: forall l r p1 p2 n,
path (gt l) p1 p2 n -> path (gt (Node l r)) (Left::p1) (Left::p2) n.
Proof.
induction 1; auto.
apply path_cons with (Left::x2); auto.
red in H; red; intuition.
Save.

Lemma path_gt_r_root_inv : forall l r n,
(forall p2, path (gt (Node l r)) nil (Right::p2) n ->
exists n', n' < n /\ path (gt r) nil p2 n') /\
(forall p2, path (gt (Node l r)) nil (Left::p2) n ->
exists n', n' < n /\ path (gt l) nil p2 n') /\
(forall p1 p2,
path (gt (Node l r)) (Right::p1) (Right::p2) n ->
exists n', n'<=n /\ path (gt r) p1 p2 n') /\
(forall p1 p2,
path (gt (Node l r)) (Left::p1) (Left::p2) n ->
exists n', n'<=n /\ path (gt l) p1 p2 n') /\
(forall p1 p2,
path (gt (Node l r)) (Left::p1) (Right::p2) n ->
exists m1, exists m2,
path (gt l) p1 nil m1 /\ path (gt r) nil p2 m2 /\ n>=2+m1+m2).
Proof.
intros l r n; pattern n; apply (well_founded_ind lt_wf).
clear n; intros n Hn; intuition.
inversion H; subst.
destruct x2.
inversion H0; intuition.
inversion H5.
destruct d.
elim (Hn n0); intuition.
elim (H7 _ _ H1); intros m1 (m2,(h1,(h2,h3))).
exists m2; intuition.
elim (Hn n0); intuition.
elim (H3 x2 p2); intuition.
exists x; intuition.
inversion H0; intuition.
inversion H12.
rewrite H10; auto.
inversion H; subst.
destruct x2.
inversion H0; intuition.
inversion H5.
destruct d.
elim (Hn n0); intuition.
elim (H5 x2 p2); intuition.
exists x; intuition.
inversion H0; intuition.
inversion H12.
rewrite H10; auto.
elim (Hn n0); intuition.
assert (path (gt (Node l r)) (Left :: p2) (Right :: x2) n0).
apply path_sym; auto.
elim (H7 _ _ H6); intros m1 (m2,(h1,(h2,h3))).
exists m1; intuition.
inversion H; subst.
exists 0; auto.
destruct x2.
elim (Hn n0); intuition; clear H4 H5 H7.
elim (H2 p2); intuition.
exists x; intuition.
inversion H0; intuition.
inversion H9; subst; auto.
destruct d.
red in H0; intuition.
inversion H4.
elim (Hn n0); intuition; clear H4 H5 H7.
elim (H3 x2 p2); auto.
intros n' (h1,h2).
exists (S n'); intuition.
apply path_cons with x2; auto.
red; red in H0; intuition.
inversion H4; auto.
inversion H0; auto.
inversion H6; auto.
inversion H; subst.
exists 0; auto.
destruct x2.
elim (Hn n0); intuition; clear H2 H3 H7.
elim (H4 p2); intuition.
exists x; intuition.
inversion H0; intuition.
inversion H9; subst; auto.
destruct d.
elim (Hn n0); intuition; clear H2 H3 H7.
elim (H5 x2 p2); auto.
intros n' (h1,h2).
exists (S n'); intuition.
apply path_cons with x2; auto.
red; red in H0; intuition.
inversion H2; auto.
inversion H0; auto.
inversion H6; auto.
red in H0; intuition.
inversion H4.
inversion H; subst.
destruct x2; intuition.
exists 0.
elim (Hn n0); intuition.
elim (H2 _ H1); intuition.
exists x; intuition.
red in H0; intuition.
inversion H11; subst; auto.
destruct d.
elim (Hn n0); intuition.
elim (H7 _ _ H1); intros m1 (m2,(h1,(h2,h3))).
assert (path (gt (Node l r)) (Left :: p1) (Left :: x2) 1).
apply path_1; auto.
elim (Hn 1); intuition.
elim (H11 _ _ H6); clear H8 H10 H9 H11 H13.
intros m' (hm'1,hm'2).
exists (m'+m1); exists m2; intuition.
apply path_trans with x2; auto.
red in H0; intuition.
inversion H4.
Save.

Lemma path_gt_r_root : forall l r n p2,
path (gt (Node l r)) nil (Right::p2) n ->
exists n', n' < n /\ path (gt r) nil p2 n'.
Proof.
intros l r n; generalize (path_gt_r_root_inv l r n); intuition.
Save.

Lemma path_gt_r_inv : forall l r n p1 p2,
path (gt (Node l r)) (Right::p1) (Right::p2) n ->
exists n', n'<=n /\ path (gt r) p1 p2 n'.
Proof.
intros l r n; generalize (path_gt_r_root_inv l r n); intuition.
Save.

Lemma split : forall l r m p1 p2,
path (gt (Node l r)) (Left::p1) (Right::p2) m ->
exists m1, exists m2,
path (gt l) p1 nil m1 /\ path (gt r) nil p2 m2 /\ m>=2+m1+m2.
Proof.
intros l r m; generalize (path_gt_r_root_inv l r m); intuition.
Save.

Lemma path_gt_l_root : forall l r n p2,
path (gt (Node l r)) nil (Left::p2) n ->
exists n', n' < n /\ path (gt l) nil p2 n'.
Proof.
intros l r n; generalize (path_gt_r_root_inv l r n); intuition.
Save.

Lemma path_gt_l_inv : forall l r n p1 p2,
path (gt (Node l r)) (Left::p1) (Left::p2) n ->
exists n', n'<=n /\ path (gt l) p1 p2 n'.
Proof.
intros l r n; generalize (path_gt_r_root_inv l r n); intuition.
Save.

Require Export Max.

Fixpoint height (t:tree) : nat := match t with
| Empty => 0
| Node l r => S (max (height l) (height r))
end.

Ltac Max n m :=
cut (m <= n \/ n <= m);
[ intros [h|h]; [ rewrite max_l | rewrite max_r ]
| omega ].

Lemma max_1 : forall n m, n<=m -> max n m = m.
Proof. intros n m; Max n m; intuition. Save.

Lemma max_2 : forall n m p, n <= m -> n <= max m p.
Proof. intros n m p; Max m p; intuition. Save.

Lemma max_3 : forall n m, n>m -> max n m = n.
Proof. intros n m; Max n m; intuition. Save.

Lemma max_4 : forall n m p, n <= p -> n <= max m p.
Proof. intros n m p; Max m p; intuition. Save.

Lemma max_5 : forall n m, n <= max n m.
Proof. intros n m; Max n m; intuition. Save.

Lemma max_6 : forall n m, m <= max n m.
Proof. intros n m; Max n m; intuition. Save.

Lemma max_7 : forall n m, max n m <= n+m.
Proof. intros n m; Max n m; intuition. Save.

Lemma max_3_cases : forall x y z,
(x >= y /\ x >= z /\ max x (max y z) = x) \/
(y >= x /\ y >= z /\ max x (max y z) = y) \/
(z >= x /\ z >= y /\ max x (max y z) = z).
Proof.
intros x y z.
assert (y<=z \/ y>=z). omega. intuition.
replace (max y z) with z.
Max x z; intuition.
rewrite max_r; intuition.
replace (max y z) with y.
Max x y; intuition.
rewrite max_l; intuition.
Save.

Hint Resolve max_2.

Lemma dist_height : forall t, exists p, dist (gt t) nil p (height t).
Proof.
induction t; simpl.
unfold dist; exists (@nil dir); intuition.
case (le_gt_dec (height t1) (height t2)); intro.
rewrite max_1; auto.
clear IHt1; elim IHt2; intros p2; clear IHt2; exists (Right :: p2).
red; intuition.
apply path_cons with (cons Right nil); auto.
red; red in H; intuition.
red in H; intuition.
apply path_gt_r; auto.
red in H; intuition.
elim (path_gt_r_root _ _ _ _ H0); intros x (Hm1, Hm2).
generalize (H2 _ Hm2).
omega.
rewrite max_3; auto.
clear IHt2; elim IHt1; intros p1; clear IHt1; exists (Left :: p1).
red; intuition.
apply path_cons with (cons Left nil); auto.
red; red in H; intuition.
red in H; intuition.
apply path_gt_l; auto.
red in H; intuition.
elim (path_gt_l_root _ _ _ _ H0); intros x (Hm1, Hm2).
generalize (H2 _ Hm2).
omega.
Save.

Lemma dist_height_max :
forall t p n, dist (gt t) nil p n -> n <= height t.
Proof.
induction t; simpl.
unfold dist; intuition.
inversion H0; subst; auto.
elim (gt_empty _ _ H).
unfold dist; destruct p; simpl; intuition.
inversion H0; subst.
generalize (H1 0 H0); auto with *.
assert (S n0 <= 0).
apply H1; auto.
omega.
destruct d.
elim (path_gt_l_root _ _ _ _ H0); intros x (hx1,hx2).
apply le_trans with (1+height t1).
assert (x<n-1 \/ x=n-1). omega. intuition.
assert (n<=S x).
apply H1.
apply path_cons with (cons Left nil).
unfold gt; auto.
apply path_gt_l; auto.
omega.
assert (x<=height t1).
apply IHt1 with p; red; intuition.
assert (n<=S m).
apply H1.
apply path_cons with (cons Left nil).
unfold gt; auto.
apply path_gt_l; auto.
omega.
omega.
generalize (max_5 (height t1) (height t2)); omega.
elim (path_gt_r_root _ _ _ _ H0); intros x (hx1,hx2).
apply le_trans with (1+height t2).
assert (x<n-1 \/ x=n-1). omega. intuition.
assert (n<=S x).
apply H1.
apply path_cons with (cons Right nil).
unfold gt; auto.
apply path_gt_r; auto.
omega.
assert (x<=height t2).
apply IHt2 with p; red; intuition.
assert (n<=S m).
apply H1.
apply path_cons with (cons Right nil).
unfold gt; auto.
apply path_gt_r; auto.
omega.
omega.
generalize (max_6 (height t1) (height t2)); omega.
Save.

Definition Diameter t := diameter (gt t).

Lemma key_lemma : forall t1 t2 d1 d2,
Diameter t1 d1 -> Diameter t2 d2 ->
Diameter (Node t1 t2) (max d1 (max d2 (2+height t1+height t2))).
Proof.
unfold Diameter.
intros t1 t2 d1 d2 ((t11, (t12, h1t1),h2t1)).
intros ((t21,(t22,h1t2),h2t2)).
split.
elim (max_3_cases d1 d2 (2+height t1+height t2)).
intros (hmax1,(hmax2 ,hmax3)); rewrite hmax3; clear hmax3.
exists (Left::t11); exists (Left::t12); red; intuition.
apply path_gt_l.
red in h1t1; intuition.
red in h1t1; intuition.
elim (path_gt_l_inv _ _ _ _ _ H); intros m' (h1,h2).
apply le_trans with m'; auto.
intros [(hmax1,(hmax2,hmax3)) | (hmax1,(hmax2,hmax3))];
rewrite hmax3; clear hmax3.
exists (Right::t21); exists (Right::t22); red; intuition.
apply path_gt_r.
red in h1t2; intuition.
red in h1t2; intuition.
elim (path_gt_r_inv _ _ _ _ _ H); intros m' (h1,h2).
apply le_trans with m'; auto.
elim (dist_height t1); intros p1 hp1.
elim (dist_height t2); intros p2 hp2.
exists (Left::p1); exists (Right::p2); red; intuition.
red in hp1; red in hp2; intuition.
replace (2+height t1+height t2) with (height t1+(1+(1+(height t2)))); auto with *.
apply path_trans with (Left::nil).
apply path_gt_l; auto.
apply path_trans with (@nil dir); auto.
apply path_1; red; auto.
apply path_trans with (Right::nil); auto.
apply path_1; red; auto.
apply path_gt_r; auto.
elim (split _ _ _ _ _ H); intros m1 (m2, (h1,(h2,h3))).
red in hp1; red in hp2; intuition.
assert (path (gt t1) nil p1 m1); auto.
generalize (H1 m1 H4).
generalize (H3 m2 h2).
omega.
unfold dist; intuition.
destruct t0; destruct t3.
assert (path (gt (Node t1 t2)) nil nil 0); auto.
generalize (H1 0 H); omega.
destruct d.
do 2 apply max_4.
apply le_trans with (height (Node t1 t2)).
apply dist_height_max with (Left::t3); red; intuition.
simpl.
generalize (max_7 (height t1) (height t2)); omega.
do 2 apply max_4.
apply le_trans with (height (Node t1 t2)).
apply dist_height_max with (Right::t3); red; intuition.
simpl.
generalize (max_7 (height t1) (height t2)); omega.
destruct d.
do 2 apply max_4.
apply le_trans with (height (Node t1 t2)).
apply dist_height_max with (Left::t0); red; intuition.
simpl.
generalize (max_7 (height t1) (height t2)); omega.
do 2 apply max_4.
apply le_trans with (height (Node t1 t2)).
apply dist_height_max with (Right::t0); red; intuition.
simpl.
generalize (max_7 (height t1) (height t2)); omega.
destruct d; destruct d0; simpl.
apply max_2.
elim (path_gt_l_inv _ _ _ _ _ H0); intros m' (hm'1,hm'2).
assert (m<=m').
apply H1; apply path_gt_l; auto.
assert (dist (gt t1) t0 t3 m').
red; intuition.
replace m' with m; [idtac|omega].
apply H1; apply path_gt_l; auto.
replace m with m'; [idtac|omega].
apply (h2t1 _ _ _ H2).
do 2 apply max_4.
elim (split _ _ _ _ _ H0); intros m1 (m2, (h1,(h2,h3))).
assert (m <= m1+S(S m2)).
apply H1.
apply path_trans with (Left::nil); auto.
apply path_gt_l; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Right::nil); auto.
red; intuition.
apply path_gt_r; auto.
assert (m1 <= height t1).
apply dist_height_max with t0.
red; intuition.
assert (m1 <= m0 \/ m1 > m0). omega. intuition.
assert (path (gt (Node t1 t2)) (Left::t0) (Right::t3) (m0+S(S m2))).
apply path_trans with (Left::nil); auto.
apply path_gt_l; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Right::nil); auto.
red; intuition.
apply path_gt_r; auto.
generalize (H1 _ H3); omega.
assert (m2 <= height t2).
apply dist_height_max with t3.
red; intuition.
assert (m2 <= m0 \/ m2 > m0). omega. intuition.
assert (path (gt (Node t1 t2)) (Left::t0) (Right::t3) (m1+S(S m0))).
apply path_trans with (Left::nil); auto.
apply path_gt_l; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Right::nil); auto.
red; intuition.
apply path_gt_r; auto.
generalize (H1 _ H4); omega.
omega.
do 2 apply max_4.
assert (path (gt (Node t1 t2)) (Left::t3) (Right::t0) m); auto.
elim (split _ _ _ _ _ H); intros m1 (m2, (h1,(h2,h3))).
assert (m <= m2+S(S m1)).
apply H1.
apply path_trans with (Right::nil); auto.
apply path_gt_r; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Left::nil); auto.
red; intuition.
apply path_gt_l; auto.
assert (m1 <= height t1).
apply dist_height_max with t3.
red; intuition.
assert (m1 <= m0 \/ m1 > m0). omega. intuition.
assert (path (gt (Node t1 t2)) (Right::t0) (Left::t3) (m2+S(S m0))).
apply path_trans with (Right::nil); auto.
apply path_gt_r; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Left::nil); auto.
red; intuition.
apply path_gt_l; auto.
generalize (H1 _ H4); omega.
assert (m2 <= height t2).
apply dist_height_max with t0.
red; intuition.
assert (m2 <= m0 \/ m2 > m0). omega. intuition.
assert (path (gt (Node t1 t2)) (Right::t0) (Left::t3) (m0+S(S m1))).
apply path_trans with (Right::nil); auto.
apply path_gt_r; auto.
apply path_cons with (@nil dir); auto.
red; intuition.
apply path_cons with (Left::nil); auto.
red; intuition.
apply path_gt_l; auto.
generalize (H1 _ H5); omega.
omega.
apply max_4; apply max_2.
elim (path_gt_r_inv _ _ _ _ _ H0); intros m' (hm'1,hm'2).
assert (m<=m').
apply H1; apply path_gt_r; auto.
assert (dist (gt t2) t0 t3 m').
red; intuition.
replace m' with m; [idtac|omega].
apply H1; apply path_gt_r; auto.
replace m with m'; [idtac|omega].
apply (h2t2 _ _ _ H2).
Save.

Definition diamh (t:tree) :
{ r:nat*nat | let (d,h) := r in Diameter t d /\ h=height t }.
Proof.
induction t; simpl.
exists (0,0); intuition.
split.
exists (@nil dir); exists (@nil dir); red; intuition; auto.
intros.
inversion H.
inversion_clear H0; auto.
elim (gt_empty _ _ H2).
elim IHt1; intros (d1, h1); clear IHt1.
elim IHt2; intros (d2, h2); clear IHt2.
intuition.
exists (max d1 (max d2 (2+h1+h2)), 1+max h1 h2); split.
subst; apply key_lemma; auto.
subst; auto.
Defined.

Definition diam (t:tree) : { d:nat | Diameter t d }.
Proof.
refine (fun t => match diamh t with
| exist dh _ => (exist _ (fst dh) _)
end).
destruct dh; simpl; intuition.
Defined.