0 | module Data.Tree.Perfect
  1 |
  2 | import Control.WellFounded
  3 | import Data.Monoid.Exponentiation
  4 | import Data.Nat.Views
  5 | import Data.Nat
  6 | import Data.Nat.Order.Properties
  7 | import Data.Nat.Exponentiation
  8 | import Syntax.WithProof
  9 | import Syntax.PreorderReasoning.Generic
 10 |
 11 | %default total
 12 |
 13 | public export
 14 | data Tree : Nat -> Type -> Type where
 15 |   Leaf : a -> Tree Z a
 16 |   Node : Tree n a -> Tree n a -> Tree (S n) a
 17 |
 18 | public export
 19 | Functor (Tree n) where
 20 |   map f (Leaf a) = Leaf (f a)
 21 |   map f (Node l r) = Node (map f l) (map f r)
 22 |
 23 | public export
 24 | replicate : (n : Nat) -> a -> Tree n a
 25 | replicate Z a = Leaf a
 26 | replicate (S n) a = let t = replicate n a in Node t t
 27 |
 28 | public export
 29 | {n : _} -> Applicative (Tree n) where
 30 |   pure = replicate n
 31 |
 32 |   Leaf f <*> Leaf a = Leaf (f a)
 33 |   Node fl fr <*> Node xl xr = Node (fl <*> xl) (fr <*> xr)
 34 |
 35 | public export
 36 | data Path : Nat -> Type where
 37 |   Here  : Path Z
 38 |   Left  : Path n -> Path (S n)
 39 |   Right : Path n -> Path (S n)
 40 |
 41 | public export
 42 | toNat : {n : _} -> Path n -> Nat
 43 | toNat Here = Z
 44 | toNat (Left p) = toNat p
 45 | toNat {n = S n} (Right p) = toNat p + pow2 n
 46 |
 47 | export
 48 | toNatBounded : (n : Nat) -> (p : Path n) -> toNat p `LT` pow2 n
 49 | toNatBounded Z Here = reflexive
 50 | toNatBounded (S n) (Left p) = CalcWith $
 51 |   |~ S (toNat p)
 52 |   <~ pow2 n          ...( toNatBounded n p )
 53 |   <~ pow2 n + pow2 n ...( lteAddRight (pow2 n) )
 54 |   ~~ pow2 (S n)      ...( sym unfoldPow2 )
 55 | toNatBounded (S n) (Right p) = CalcWith $
 56 |   let ih = toNatBounded n p in
 57 |   |~ S (toNat p) + pow2 n
 58 |   <~ pow2 n + pow2 n      ...( plusLteMonotoneRight _ _ _ ih )
 59 |   ~~ pow2 (S n)           ...( sym unfoldPow2 )
 60 |
 61 | namespace FromNat
 62 |
 63 |   ||| This pattern-matching in `fromNat` is annoying:
 64 |   ||| The    `Z (S _)` case is impossible
 65 |   ||| In the `k (S n)` case we want to branch on whether `k `LT` pow2 n`
 66 |   ||| and get our hands on some proofs.
 67 |   ||| This view factors out that work.
 68 |   public export
 69 |   data View : (k, n : Nat) -> Type where
 70 |     ZZ   : View Z Z
 71 |     SLT  : (0 p : k `LT` pow2 n) -> View k (S n)
 72 |     SNLT : (0 p : k `GTE` pow2 n) ->
 73 |            (0 rec : minus k (pow2 n) `LT` pow2 n) -> View k (S n)
 74 |
 75 |   public export
 76 |   view : (k, n : Nat) -> (0 _ : k `LT` (pow2 n)) -> View k n
 77 |   view Z Z p = ZZ
 78 |   view (S _) Z p = void $ absurd (fromLteSucc p)
 79 |   view k (S n) p with (@@ lt k (pow2 n))
 80 |     view k (S n) p | (True ** eq) = SLT (ltIsLT k (pow2 n) eq)
 81 |     view k (S n) p | (False ** eq) = SNLT gte prf where
 82 |
 83 |       0 gte : k `GTE` pow2 n
 84 |       gte = notLTImpliesGTE (notltIsNotLT k (pow2 n) eq)
 85 |
 86 |       0 prf : minus k (pow2 n) `LT` pow2 n
 87 |       prf = CalcWith $
 88 |         |~ S (minus k (pow2 n))
 89 |         <~ minus (pow2 (S n)) (pow2 n)
 90 |            ...( minusLtMonotone p pow2Increasing )
 91 |         ~~ minus (pow2 n + pow2 n) (pow2 n)
 92 |            ...( cong (\ m => minus m (pow2 n)) unfoldPow2 )
 93 |         ~~ pow2 n
 94 |            ...( minusPlus (pow2 n) )
 95 |
 96 | ||| Convert a natural number to a path in a perfect binary tree
 97 | public export
 98 | fromNat : (k, n : Nat) -> (0 _ : k `LT` pow2 n) -> Path n
 99 | fromNat k n p with (view k n p)
100 |   fromNat Z Z p | ZZ = Here
101 |   fromNat k (S n) p | SLT lt = Left (fromNat k n lt)
102 |   fromNat k (S n) p | SNLT _ lt = Right (fromNat (minus k (pow2 n)) n lt)
103 |
104 | ||| The `fromNat` conversion is compatible with the semantics `toNat`
105 | export
106 | fromNatCorrect : (k, n : Nat) -> (0 p : k `LT` pow2 n) ->
107 |                  toNat (fromNat k n p) === k
108 | fromNatCorrect k n p with (view k n p)
109 |   fromNatCorrect Z Z p | ZZ = Refl
110 |   fromNatCorrect k (S n) p | SLT lt = fromNatCorrect k n lt
111 |   fromNatCorrect k (S n) p | SNLT gte lt
112 |      = rewrite fromNatCorrect (minus k (pow2 n)) n lt in
113 |        irrelevantEq $ plusMinusLte (pow2 n) k gte
114 |
115 | public export
116 | lookup : Tree n a -> Path n -> a
117 | lookup (Leaf a) Here = a
118 | lookup (Node l _) (Left p) = lookup l p
119 | lookup (Node _ r) (Right p) = lookup r p
120 |