When we studied List.fold_left and List.fold_right, we discussed how they sometimes compute the same function, but in general do not. For example,

  List.fold_left (+) 0 [1; 2; 3]
= (((0 + 1) + 2) + 3
= 6
= 1 + (2 + (3 + 0))
= List.fold_right (+) lst [1;2;3]


but

  List.fold_left (-) 0 [1;2;3]
= (((0 - 1) - 2) - 3
= -6
<> 2
= 1 - (2 - (3 - 0))
= List.fold_right (-) lst [1;2;3]


Based on the equations above, it looks like the fact that + is commutative and associative, whereas - is not, explains this difference between when the two fold functions get the same answer. Let's prove it!

First, recall the definitions of the fold functions:

let rec fold_left f acc lst =
match lst with
| [] -> acc
| h :: t -> fold_left f (f acc h) t

let rec fold_right f lst acc =
match lst with
| [] -> acc
| h :: t -> f h (fold_right f t acc)


Second, recall what it means for a function f : 'a -> 'a to be commutative and associative:

Commutative:  forall x y, f x y = f y x
Associative:  forall x y z, f x (f y z) = f (f x y) z


Those might look a little different than the normal formulations of those properties, because we are using f as a prefix operator. If we were to write f instead as an infix operator op, they would look more familiar:

Commutative:  forall x y, x op y = y op x
Associative:  forall x y z, x op (y op z) = (x op y) op z


When f is both commutative and associative we have this little interchange lemma that lets us swap two arguments around:

Lemma (interchange): f x (f y z) = f y (f x z)

Proof:

f x (f y z)
=   { associativity }
f (f x y) z
=   { commutativity }
f (f y x) z
=   { associativity }
f y (f z x)

QED


Now we're ready to state and prove the theorem.

Theorem: If f is commutative and associative, then
forall lst acc,
fold_left f acc lst = fold_right f lst acc.

Proof: by induction on lst.
P(lst) = forall acc,
fold_left f acc lst = fold_right f lst acc

Base case: lst = []
Show: forall acc,
fold_left f acc [] = fold_right f [] acc

fold_left f acc []
=   { evaluation }
acc
=   { evaluation }
fold_right f [] acc

Inductive case: lst = h :: t
IH: forall acc,
fold_left f acc t = fold_right f t acc
Show: forall acc,
fold_left f acc (h :: t) = fold_right f (h :: t) acc

fold_left f acc (h :: t)
=   { evaluation }
fold_left f (f acc h) t
=   { IH with acc := f acc h }
fold_right f t (f acc h)

fold_right f (h :: t) acc
=   { evaluation }
f h (fold_right f t acc)


Now, it might seem as though we are stuck: the left and right sides of the equality we want to show have failed to "meet in the middle." But we're actually in a similar situation to when we proved the correctness of facti earlier: there's something (applying f to h and another argument) that we want to push into the accumulator of that last line (so that we have f acc h).

Let's try proving that with its own lemma:

Lemma: forall lst acc x,
f x (fold_right f lst acc) = fold_right f lst (f acc x)

Proof: by induction on lst.
P(lst) = forall acc x,
f x (fold_right f lst acc) = fold_right f lst (f acc x)

Base case: lst = []
Show: forall acc x,
f x (fold_right f [] acc) = fold_right f [] (f acc x)

f x (fold_right f [] acc)
=   { evaluation }
f x acc

fold_right f [] (f acc x)
=   { evaluation }
f acc x
=   { commutativity of f }
f x acc

Inductive case: lst = h :: t
IH: forall acc x,
f x (fold_right f t acc) = fold_right f t (f acc x)
Show: forall acc x,
f x (fold_right f (h :: t) acc) = fold_right f (h :: t) (f acc x)

f x (fold_right f (h :: t) acc)
=  { evaluation }
f x (f h (fold_right f t acc))
=  { interchange lemma }
f h (f x (fold_right f t acc))
=  { IH }
f h (fold_right f t (f acc x))

fold_right f (h :: t) (f acc x)
=   { evaluation }
f h (fold_right f t (f acc x))

QED


Now that the lemma is completed, we can resume the proof of the theorem. We'll restart at the beginning of the inductive case:

Inductive case: lst = h :: t
IH: forall acc,
fold_left f acc t = fold_right f t acc
Show: forall acc,
fold_left f acc (h :: t) = fold_right f (h :: t) acc

fold_left f acc (h :: t)
=   { evaluation }
fold_left f (f acc h) t
=   { IH with acc := f acc h }
fold_right f t (f acc h)

fold_right f (h :: t) acc
=   { evaluation }
f h (fold_right f t acc)
=   { lemma with x := h and lst := t }
fold_right f t (f acc h)

QED


It took two inductions to prove the theorem, but we succeeded! Now we know that the behavior we observed with + wasn't a fluke: any commutative and associative operator causes fold_left and fold_right to get the same answer.