## Stream: math-comp users

### Topic: Fold lemmas

#### Alexander Gryzlov (Nov 04 2022 at 14:45):

Seems that https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html doesn't have much lemmas for `foldr`/`foldl`. Do you think any of these would make a useful addition: https://gist.github.com/clayrat/8bad4899b1ed188567028259374585bb ? The fusion laws at least are supposed to be pretty fundamental.

#### Cyril Cohen (Nov 04 2022 at 15:45):

Makes sense... I'd suggest the following rephrasing / renaming

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

Lemma foldr_rev {T1 T2} (f : T1 -> T2 -> T2) x s :
foldr f x (rev s) = foldl (fun y => f^~ y) x s.
Proof. by elim: s x => //= y s + z => <-; rewrite rev_cons foldr_rcons. Qed.

(* replace proof from mathcomp *)
Lemma foldl_rev {T1 T2} (f : T2 -> T1 -> T2) x s :
foldl f x (rev s) = foldr (fun y => f^~ y) x s.
Proof. by rewrite -foldr_rev revK. Qed.

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

Lemma mapEfoldl {T1 T2} (f : T1 -> T2) s :
map f s = foldl (fun ys x => f x :: ys) [::] (rev s).
Proof. by rewrite mapEfoldr foldl_rev. Qed.

Lemma foldr_mapl {T T' R Q} l (g : R -> Q) (h : T -> T') r z s :
(forall x y, g (r x y) = l (h x) (g y)) ->
foldr l (g z) (map h s) = g (foldr r z s).
Proof. by move=> gr; elim: s => //= x s ->. Qed.
Arguments foldr_mapl {T T' R Q}.

Lemma foldl_mapl {T T' R Q} l (g : R -> Q) (h : T -> T') r z s :
(forall x y, g (r x y) = l (g x) (h y)) ->
foldl l (g z) (map h s) = g (foldl r z s).
Proof. by move=> gr; rewrite -!foldr_rev -map_rev; apply: foldr_mapl. Qed.
Arguments foldl_mapl {T T' R Q}.

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

Lemma foldrEl {T R} (f : T -> R -> R) z s :
foldr f z s = foldl (fun g b x => g (f b x)) id s z.
Proof. by rewrite -foldr_rev -foldl_rev foldlEr. Qed.

(* replace proof from mathcomp *)
Lemma foldr_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. exact: (foldr_mapl _ id). Qed.

Lemma foldl_map {R T1 T2} (h : T1 -> T2) (f : R -> T2 -> R) (z0 : R) s :
foldl f z0 (map h s) = foldl (fun z x => f z (h x)) z0 s.
Proof. exact: (foldl_mapl _ id). Qed.
``````

Last updated: Jan 29 2023 at 19:02 UTC