0 | module Data.Nat.Views
 1 |
 2 | import Control.WellFounded
 3 | import Data.Nat
 4 |
 5 | %default total
 6 |
 7 | ||| View for dividing a Nat in half
 8 | public export
 9 | data Half : Nat -> Type where
10 |      HalfOdd : (n : Nat) -> Half (S (n + n))
11 |      HalfEven : (n : Nat) -> Half (n + n)
12 |
13 | ||| View for dividing a Nat in half, recursively
14 | public export
15 | data HalfRec : Nat -> Type where
16 |      HalfRecZ : HalfRec Z
17 |      HalfRecEven : (n : Nat) -> (rec : Lazy (HalfRec n)) -> HalfRec (n + n)
18 |      HalfRecOdd : (n : Nat) -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
19 |
20 | ||| Covering function for the `Half` view
21 | public export
22 | half : (n : Nat) -> Half n
23 | half Z = HalfEven Z
24 | half (S k) with (half k)
25 |   half (S (S (n + n))) | HalfOdd n = rewrite plusSuccRightSucc (S n) n in
26 |                                            HalfEven (S n)
27 |   half (S (n + n)) | HalfEven n = HalfOdd n
28 |
29 | public export
30 | halfRec : (n : Nat) -> HalfRec n
31 | halfRec n with (sizeAccessible n)
32 |   halfRec  Z | acc = HalfRecZ
33 |   halfRec (S n) | acc with (half n)
34 |     halfRec (S (S (k + k))) | Access acc | HalfOdd k
35 |       = rewrite plusSuccRightSucc (S k) k
36 |           in HalfRecEven _ (halfRec (S k) | acc (S k) (LTESucc (LTESucc (lteAddRight _))))
37 |     halfRec (S (k + k)) | Access acc | HalfEven k
38 |       = HalfRecOdd _ (halfRec k | acc k (LTESucc (lteAddRight _)))
39 |