Added lemmas about foldl, scanl, foldr and rcons and cons

1 files changed, 15 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 37fe1e6..f73c119 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2522,6 +2522,9 @@ Variables (R : Type) (f : T2 -> R -> R) (z0 : R).
 Lemma foldr_cat s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1.
 Proof. by elim: s1 => //= x s1 ->. Qed.
 
+Lemma foldr_rcons s x : foldr f z0 (rcons s x) = foldr f (f x z0) s.
+Proof. by rewrite -cats1 foldr_cat. Qed.
+
 Lemma foldr_map s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s.
 Proof. by elim: s => //= x s ->. Qed.
 
@@ -2576,6 +2579,9 @@ Proof.
 by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK.
 Qed.
 
+Lemma foldl_rcons z s x : foldl z (rcons s x) = f (foldl z s) x.
+Proof. by rewrite -cats1 foldl_cat. Qed.
+
 End FoldLeft.
 
 Section Scan.
@@ -2606,9 +2612,17 @@ Lemma scanl_cat x s1 s2 :
   scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2.
 Proof. by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1. Qed.
 
+Lemma scanl_rcons x s1 y  :
+  scanl x (rcons s1 y) =  rcons (scanl x s1) (foldl g x (rcons s1 y)).
+Proof. by rewrite -!cats1 scanl_cat foldl_cat. Qed.
+
+Lemma nth_cons_scanl s n : n <= size s ->
+  forall x, nth x1 (x :: scanl x s) n = foldl g x (take n s).
+Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite IHs. Qed.
+
 Lemma nth_scanl s n : n < size s ->
   forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s).
-Proof. by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite ?take0 ?IHs. Qed.
+Proof. by move=> n_lt x; rewrite -nth_cons_scanl. Qed.
 
 Lemma scanlK :
   (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x).