Stream: math-comp users

Topic: Fold lemmas


view this post on Zulip 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.

view this post on Zulip 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