Foldl/r extra

folds.v

From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma map_foldr {T1 T2} (f : T1 -> T2) xs :
  map f xs = foldr (fun x ys => f x :: ys) [::] xs.
Proof. by []. Qed.

Lemma fusion_foldr {T R Q} (g : R -> Q) f0 f1 z0 z1 (xs : seq T) :
  (forall x y, g (f0 x y) = f1 x (g y)) -> g z0 = z1 ->
  g (foldr f0 z0 xs) = foldr f1 z1 xs.
Proof. by move=>Hf Hz; elim: xs=>//= x xs <-. Qed.

Lemma fusion_foldl {T R Q} (g : R -> Q) f0 f1 z0 z1 (xs : seq T) :
  (forall x y, g (f0 x y) = f1 (g x) y) -> g z0 = z1 ->
  g (foldl f0 z0 xs) = foldl f1 z1 xs.
Proof.
move=>Hf Hz; elim: xs z0 z1 Hz =>//= x xs IH z0 z1 Hz.
by apply: IH; rewrite Hf Hz.
Qed.

Lemma foldl_foldr {T R} (f : R -> T -> R) z xs :
  foldl f z xs = foldr (fun b g x => g (f x b)) id xs z.
Proof. by elim: xs z=>/=. Qed.

Lemma foldr_foldl {T R} (f : T -> R -> R) z xs :
  foldr f z xs = foldl (fun g b x => g (f b x)) id xs z.
Proof.
elim/last_ind: xs z=>//= xs x IH z.
by rewrite foldl_rcons -IH foldr_rcons.
Qed.

Lemma fusion_map {R T1 T2} (h : T1 -> T2) (f : T2 -> R -> R) (z0 : R) s :
   foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.
Proof. by rewrite map_foldr; apply: fusion_foldr. Qed.