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