How to fold a vector

Stream: new members

[Mukesh Tiwari]

Hi everyone, how can I fold a vector. I am getting this error unknown constant 'Vector.foldl'.

import Aesop
import Mathlib
import Batteries

open Mathlib
open Batteries

section bulletproofdefinition

  variable {G : Type*} {F : Type*}
    [AddCommGroup G] [DecidableEq G]
    [Field F] [DecidableEq F]
    [Module F G]

  #print Vector
  /-
    Committing a vector of Group elements to a vector of group elements.
  -/
  def pedersen_commitment_vector {n : Nat} (g : Vector G n)
    (h : G) (m : Vector F n) (r : F) : G:=
     Vector.foldl (fun acc ((mi, gi) : F × G) => acc + mi • gi)
     (r • h) (Vector.zipWith m g (fun mi gi => (mi, gi)))

This works fine though and I am wondering if this the idiomatic way to work with vectors?

def pedersen_commitment_vector {n : Nat} (g : Vector G n)
    (h : G) (m : Vector F n) (r : F) : G :=
     Array.foldl (fun acc ((mi, gi) : F × G) => acc + mi • gi)
     (r • h) (Array.zipWith m.toArray g.toArray (fun mi gi => (mi, gi)))

[Quang Dao]

There's no reason why Vector.foldl would do anything different from applying Array.foldl to the underlying array. So what you wrote is fine, maybe you could also do

def pedersen_commitment_vector {n : Nat} (g : Vector G n)
    (h : G) (m : Vector F n) (r : F) : G :=
     Array.foldl (fun acc ((mi, gi) : F × G) => acc + mi • gi)
     (r • h) (Vector.zipWith m g (fun mi gi => (mi, gi))).toArray

[Mukesh Tiwari]

Thanks @Quang Dao !