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.

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
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:1607} => 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:1676} => 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:1616} => H) -> H [] = E

foldrUniqueness : (h : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:2257} => h) -> (xs : Vect n a) -> h xs = foldr f e xs

  foldr is the unique function preserving the vector structure

foldrVectHomomorphism : VectHomomorphismProperty f e (\0 {n:2073} => foldr f e)

  Our tail-recursive foldr preserves the vector structure

nilConsInitiality : (f : (a -> b -> b)) -> (e : b) -> (h1 : (Vect n a -> b)) -> (h2 : (Vect n a -> b)) -> VectHomomorphismProperty f e (\0 {n:1748} => h1) -> VectHomomorphismProperty f e (\0 {n:1757} => h2) -> (xs : Vect n a) -> h1 xs = h2 xs

  There is an extensionally unique function preserving the vector structure

sumIsGTEtoParts : (xs : Vect n Nat) -> Elem x xs -> GTE (sumR xs) x

  Each summand is `LTE` the sum

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

sumR : (Foldable f, Num a) => f a -> a

  Sum implemented with foldr