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