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.
```

## Definitions

`sumR : Num a => Foldable f => f a -> a`
`  Sum implemented with foldr`

Visibility: public export
`record VectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> (A -> B -> B) -> B -> (Vect n A -> B) -> Type`
`  A function H : forall n. Vect n A -> B preserving the structure of vectors over A`

Totality: total
Visibility: public export
Constructor:
`ShowVectHomomorphismProperty : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> H [] = E -> ((x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)) -> VectHomomorphismProperty F E (\0 {n:3420} => H)`

Projections:
`.cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3591} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)`
`.nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3463} => H) -> H [] = E`
`.nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3463} => H) -> H [] = E`
Visibility: public export
`nil : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3528} => H) -> H [] = E`
Visibility: public export
`.cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3591} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)`
Visibility: public export
`cons : {0 A : Type} -> {0 B : Type} -> {0 F : A -> B -> B} -> {0 E : B} -> {0 H : Vect n A -> B} -> VectHomomorphismProperty F E (\0 {n:3671} => H) -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = F x (H xs)`
Visibility: public export
Fixity Declaration: infixr operator, level 5
`nilConsInitiality : (f : (a -> b -> b)) -> (e : b) -> (h1 : (Vect n a -> b)) -> (h2 : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:3751} => h1) -> VectHomomorphismProperty f e (\0 {n:3763} => h2) -> (xs : Vect n a) -> h1 xs = h2 xs`
`  There is an extensionally unique function preserving the vector structure`

Visibility: export
`foldrVectHomomorphism : VectHomomorphismProperty f e (\0 {n:4159} => foldr f e)`
`  Our tail-recursive foldr preserves the vector structure`

Visibility: export
`foldrUniqueness : (h : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:4359} => h) -> (xs : Vect n a) -> h xs = foldr f e xs`
`  foldr is the unique function preserving the vector structure`

Visibility: export
`sumIsGTEtoParts : (xs : Vect n Nat) -> Elem x xs -> GTE (sumR xs) x`
`  Each summand is `LTE` the sum`

Visibility: export
`sumMonotone : (xs : Vect n Nat) -> (ys : Vect n Nat) -> ((i : Fin n) -> LTE (index i xs) (index i ys)) -> LTE (sumR xs) (sumR ys)`
`  `sumR : Vect n Nat -> Nat` is monotone`

Visibility: export