module Rot where -- Depends on my customized Agda prelude -- http://bitbucket.org/robsimmons/agda-lib/src/518998444312 open import Prelude renaming (_≡_ to _==_ ; _≡≡_ to _===_ ; ∃ to exists ; _×_ to _&&_) -- ******************************** -- -- Part 1: Trees and tree rotations -- -- ******************************** -- data Tree (A : Set) : Set where <> : Tree A _<_>_ : Tree A -> A -> Tree A -> Tree A -- (t1 ++> t2) appends t2 to the rightmost leaf of t1 _++>_ : {A : Set} -> Tree A -> Tree A -> Tree A <> ++> t = t (t1 < x > t2) ++> t = t1 < x > (t2 ++> t) -- Defines an in-place traversal (for convienence, we do this backwards) traverse : {A : Set} -> Tree A -> ListT A traverse <> = [] traverse (t1 < x > t2) = traverse t1 ++ [ x ] ++ traverse t2 -- (t1 ~ t2) defines what it means for two trees be rotatable into each other data _~_ {A : Set} : Tree A -> Tree A -> Set where ~Refl : {t s : Tree A} -> t == s -> t ~ s ~Trans : {t1 t2 t3 : Tree A} -> t1 ~ t2 -> t2 ~ t3 -> t1 ~ t3 ~RotR : {x y : A}{t1 t2 t3 : Tree A} -> ((t1 < x > t2) < y > t3) ~ (t1 < x > (t2 < y > t3)) ~RotL : {x y : A}{t1 t2 t3 : Tree A} -> (t1 < x > (t2 < y > t3)) ~ ((t1 < x > t2) < y > t3) ~CongR : {x : A}{t1 t2 s2 : Tree A} -> t2 ~ s2 -> (t1 < x > t2) ~ (t1 < x > s2) ~CongL : {x : A}{t1 t2 s1 : Tree A} -> t1 ~ s1 -> (t1 < x > t2) ~ (s1 < x > t2) ~symm : {A : Set} {t1 t2 : Tree A} -> t1 ~ t2 -> t2 ~ t1 ~symm (~Refl Refl) = ~Refl refl ~symm (~Trans equiv1 equiv2) = ~Trans (~symm equiv2) (~symm equiv1) ~symm ~RotR = ~RotL ~symm ~RotL = ~RotR ~symm (~CongR equiv) = ~CongR (~symm equiv) ~symm (~CongL equiv) = ~CongL (~symm equiv) -- ****************************************************** -- -- Part 2: Setting up an induction metric "TM t" on terms -- -- ****************************************************** -- data TM {A : Set} : Tree A -> Set where Done : TM <> Recurse : {x : A}{t : Tree A} -> TM t -> TM (<> < x > t) Rotate : {x y : A}{t1 t2 t3 : Tree A} -> TM (t1 < x > (t2 < y > t3)) -> TM ((t1 < x > t2) < y > t3) metric : {A : Set} (t : Tree A) -> TM t metric <> = Done metric (t1 < x > t2) = helper t1 (metric t2) where append : {A : Set}{t1 t2 : Tree A} -> TM t1 -> TM t2 -> TM (t1 ++> t2) append Done t2 = t2 append (Recurse t1) t2 = Recurse (append t1 t2) append (Rotate t1) t2 = Rotate (append t1 t2) helper : {A : Set} {x : A}{t2 : Tree A} (t1 : Tree A) -> TM t2 -> TM (t1 < x > t2) helper <> tt = Recurse tt helper (t1 < x > t2) tt = Rotate (helper t1 (append (helper t2 Done) tt)) -- ************************************* -- -- Part 3 - Putting trees in normal form -- -- ************************************* -- data Normal {A : Set} : Tree A -> Set where NZ : Normal <> NS : {x : A}{t : Tree A} -> Normal t -> Normal (<> < x > t) norm : {A : Set} -> (t : Tree A) -> TM t -> exists λ tnorm -> (t ~ tnorm) && Normal tnorm && (traverse t == traverse tnorm) norm <> Done = <> , ~Refl refl , NZ , refl norm (<> < x > t) (Recurse y) with norm t y ... | tnorm , equiv , n , eq = <> < x > tnorm , ~CongR equiv , NS n , List.cons-cong2 eq norm ((t1 < x > t2) < y > t3) (Rotate tm) with norm _ tm ... | tnorm , equiv , n , eq = tnorm , ~Trans ~RotR equiv , n , List.append-assoc {as = traverse t1} {bs = x :: traverse t2} === eq -- Normal trees are identical if their traversals are identical normal-traverse : {A : Set} {t1 t2 : Tree A} -> Normal t1 -> Normal t2 -> traverse t1 == traverse t2 -> t1 == t2 normal-traverse NZ NZ equiv = refl normal-traverse NZ (NS y) () normal-traverse (NS y) NZ () normal-traverse (NS n1) (NS n2) eq with List.cons-elim eq ... | Refl , eq' with normal-traverse n1 n2 eq' ... | Refl = refl -- ************************ -- -- Part 4: The main theorem -- -- ************************ -- -- If two trees have the same in-order traversal, then it is possible to -- travel between them using only rotations. theorem : {A : Set} (t1 t2 : Tree A) -> traverse t1 == traverse t2 -> t1 ~ t2 theorem t1 t2 eq with norm t1 (metric t1) | norm t2 (metric t2) ... | t1norm , equiv1 , n1 , eq1 | t2norm , equiv2 , n2 , eq2 with normal-traverse n1 n2 (symm eq1 === eq === eq2) ... | eq' = ~Trans equiv1 (~Trans (~Refl eq') (~symm equiv2))