0 | |||
  1 | |||
  2 | ||| foldr is the unique solution to the equation:
  3 | |||
  4 | |||   h f e [] = e
  5 | |||   h f e (x :: xs) = x `h` (foldr f e xs)
  6 | |||
  7 | ||| (This fact is called 'the universal property of foldr'.)
  8 | |||
  9 | ||| Since the prelude defines foldr tail-recursively, this fact isn't immediate
 10 | ||| and we need some lemmata to prove it.
 11 | module Data.Vect.Properties.Foldr
 12 |
 13 | import Data.Vect
 14 | import Data.Vect.Elem
 15 | import Data.Fin
 16 | import Data.Nat
 17 |
 18 | import Syntax.PreorderReasoning
 19 | import Syntax.PreorderReasoning.Generic
 20 |
 21 | ||| Sum implemented with foldr
 22 | public export
 23 | sumR : Num a => Foldable f => f a -> a
 24 | sumR = foldr (+) 0
 25 |
 26 | %transform "sumR/sum" sumR = sum
 27 |
 28 | ||| A function H : forall n. Vect n A -> B preserving the structure of vectors over A
 29 | public export
 30 | record VectHomomorphismProperty {0 A, B : Type} (F : A -> B -> B) (E : B) (H : forall n . Vect n A -> B) where
 31 |   constructor ShowVectHomomorphismProperty
 32 |   nil  : H [] = E
 33 |   cons : {0 n : Nat} -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = x `F` (H xs)
 34 |
 35 | ||| There is an extensionally unique function preserving the vector structure
 36 | export
 37 | nilConsInitiality :
 38 |      (f : a -> b -> b) -> (e : b)
 39 |   -> (h1, h2 : forall n . Vect n a -> b)
 40 |   -> (prf1 : VectHomomorphismProperty f e h1)
 41 |   -> (prf2 : VectHomomorphismProperty f e h2)
 42 |   -> (xs : Vect n a) -> h1 xs = h2 xs
 43 | nilConsInitiality f e h1 h2 prf1 prf2 [] = Calc $
 44 |   |~ h1 []
 45 |   ~~ e     ...(prf1.nil)
 46 |   ~~ h2 [] ...(sym prf2.nil)
 47 |
 48 | nilConsInitiality f e h1 h2 prf1 prf2 (x :: xs) = Calc $
 49 |   |~ h1 (x :: xs)
 50 |   ~~ (x `f` (h1 xs)) ...(prf1.cons _ _)
 51 |   ~~ (x `f` (h2 xs)) ...(cong (x `f`) $ nilConsInitiality f e h1 h2 prf1 prf2 xs)
 52 |   ~~ h2 (x :: xs) ...(sym $ prf2.cons _ _)
 53 |
 54 | ||| extensionality is a congruence with respect to Data.Vect.foldrImpl
 55 | foldrImplExtensional :
 56 |   (f : a -> b -> b) -> (e : b)
 57 |   -> (go1, go2 : b -> b)
 58 |   -> ((y : b) -> go1 y = go2 y)
 59 |   -> (xs : Vect n a)
 60 |   -> foldrImpl f e go1 xs = foldrImpl f e go2 xs
 61 | foldrImplExtensional f e go1 go2 ext [] = ext e
 62 | foldrImplExtensional f e go1 go2 ext (x :: xs) =
 63 |   foldrImplExtensional f e _ _
 64 |   (\y => ext (f x y))
 65 |   xs
 66 |
 67 | ||| foldrImpl f e x : (b -> -) -> - is natural
 68 | foldrImplNaturality : (f : a -> b -> b) -> (e : b) -> (xs : Vect n a) -> (go1, go2 : b -> b)
 69 |   -> foldrImpl f e (go1 . go2) xs = go1 (foldrImpl f e go2 xs)
 70 | foldrImplNaturality f e    []     go1 go2 = Refl
 71 | foldrImplNaturality f e (x :: xs) go1 go2 = foldrImplNaturality f e xs go1 (go2 . (f x))
 72 |
 73 | ||| Our tail-recursive foldr preserves the vector structure
 74 | export
 75 | foldrVectHomomorphism : VectHomomorphismProperty f e (foldr f e)
 76 | foldrVectHomomorphism = ShowVectHomomorphismProperty
 77 |   { nil  = Refl
 78 |   , cons = \x, xs => Calc $
 79 |     |~ foldr f e (x :: xs)
 80 |     ~~ foldrImpl f e (id . (f x)) xs ...(Refl)
 81 |     ~~ foldrImpl f e ((f x) . id) xs ...(foldrImplExtensional f e _ _ (\y => Refl) xs)
 82 |     ~~ f x (foldrImpl f e id xs)     ...(foldrImplNaturality f e xs (f x) _)
 83 |     ~~ f x (foldr f e xs)            ...(Refl)
 84 |   }
 85 |
 86 | ||| foldr is the unique function preserving the vector structure
 87 | export
 88 | foldrUniqueness : (h : forall n . Vect n a -> b) -> VectHomomorphismProperty f e h -> (xs : Vect n a) -> h xs = foldr f e xs
 89 | foldrUniqueness {f} h prf xs = irrelevantEq $
 90 |   nilConsInitiality f e h (foldr f e) prf foldrVectHomomorphism xs
 91 |
 92 |
 93 | ||| Each summand is `LTE` the sum
 94 | export
 95 | sumIsGTEtoParts : {x : Nat} -> (xs : Vect n Nat) -> (x `Elem` xs) -> sumR xs `GTE` x
 96 | sumIsGTEtoParts (x :: xs) Here
 97 |   = CalcWith $
 98 |   |~ x
 99 |   ~~ x + 0 ...(sym $ plusZeroRightNeutral _)
100 |   <~ x + (sumR xs)   ...(plusLteMonotoneLeft x 0 _ LTEZero)
101 |   ~~ sumR (x :: xs)  ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)
102 |
103 | sumIsGTEtoParts {x} (y :: xs) (There later)
104 |   = CalcWith $
105 |     |~ x
106 |     <~ sumR xs       ...(sumIsGTEtoParts {x} xs later)
107 |     ~~ 0 + sumR xs   ...(Refl)
108 |     <~ y + (sumR xs) ...(plusLteMonotoneRight (sumR xs) 0 y LTEZero)
109 |     ~~ sumR (y :: xs) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)
110 |
111 | ||| `sumR : Vect n Nat -> Nat` is monotone
112 | export
113 | sumMonotone : {n : Nat} -> (xs, ys : Vect n Nat)
114 |   -> (prf : (i : Fin n) -> index i xs `LTE` index i ys)
115 |   -> (sumR xs `LTE` sumR ys)
116 | sumMonotone [] [] prf = LTEZero
117 | sumMonotone (x :: xs) (y :: ys) prf =
118 |   let prf' = sumMonotone xs ys (\i => prf (FS i))
119 |   in CalcWith $
120 |   |~ sumR (x :: xs)
121 |   ~~ x + sumR xs    ...((foldrVectHomomorphism {f = plus} {e = 0}).cons x xs)
122 |   <~ y + sumR ys    ...(plusLteMonotone  (prf 0) prf')
123 |   ~~ sumR (y :: ys) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons y ys)
124 |