Idris2Doc : Data.Vect.Properties.Foldr

# Data.Vect.Properties.Foldr

```
foldr is the unique solution to the equation:

h f e [] = e
h f e (x :: xs) = x `h` (foldr f e xs)

(This fact is called 'the universal property of foldr'.)

Since the prelude defines foldr tail-recursively, this fact isn't immediate
and we need some lemmata to prove it.```
recordVectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> (A -> B -> B) -> B -> (VectnA -> B) -> Type
`  A function H : forall n. Vect n A -> B preserving the structure of vectors over A`

Totality: total
Constructor:
ShowVectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : VectnA -> B} -> H [] = E -> ((x : A) -> (xs : VectnA) -> H (x::xs) = Fx (Hxs)) -> VectHomomorphismPropertyFE (\0 {n:1607} => H)

Projections:
.cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : VectnA -> B} -> VectHomomorphismPropertyFE (\0 {n:1676} => H) -> (x : A) -> (xs : VectnA) -> H (x::xs) = Fx (Hxs)
.nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : VectnA -> B} -> VectHomomorphismPropertyFE (\0 {n:1616} => H) -> H [] = E
foldrUniqueness : (h : (Vectna -> b)) -> VectHomomorphismPropertyfe (\0 {n:2257} => h) -> (xs : Vectna) -> hxs = foldrfexs
`  foldr is the unique function preserving the vector structure`

foldrVectHomomorphism : VectHomomorphismPropertyfe (\0 {n:2073} => foldrfe)
`  Our tail-recursive foldr preserves the vector structure`

nilConsInitiality : (f : (a -> b -> b)) -> (e : b) -> (h1 : (Vectna -> b)) -> (h2 : (Vectna -> b)) -> VectHomomorphismPropertyfe (\0 {n:1748} => h1) -> VectHomomorphismPropertyfe (\0 {n:1757} => h2) -> (xs : Vectna) -> h1xs = h2xs
`  There is an extensionally unique function preserving the vector structure`

sumIsGTEtoParts : (xs : VectnNat) -> Elemxxs -> GTE (sumRxs) x
`  Each summand is `LTE` the sum`

sumMonotone : (xs : VectnNat) -> (ys : VectnNat) -> ((i : Finn) -> LTE (indexixs) (indexiys)) -> LTE (sumRxs) (sumRys)
`  `sumR : Vect n Nat -> Nat` is monotone`

sumR : (Foldablef, Numa) => fa -> a
`  Sum implemented with foldr`