Kata

This is the verified version of Sums of Parts.

Let us consider this example (list written in general format):

xs = [0, 1, 3, 6, 10]

Its following parts:

xs = [0, 1, 3, 6, 10]
xs = [1, 3, 6, 10]
xs = [3, 6, 10]
xs = [6, 10]
xs = [10]
xs = []

The corresponding sums are (put together in a list): [20, 20, 19, 16, 10, 0]

We'll call this result "sums of parts" from now on.

Some more examples:

[1, 2, 3, 4, 5, 6] -> [21, 20, 18, 15, 11, 6, 0]

[744125, 935, 407, 454, 430, 90, 144, 6710213, 889, 810, 2579358] ->
[10037855, 9293730, 9292795, 9292388, 9291934, 9291504, 9291414,
9291270, 2581057, 2580168, 2579358, 0]

How do we calculate the sums of parts, and do so efficiently?

A naïve solution computes the sum of each part as we traverse through the list:

Fixpoint sum (xs : list Z) : Z :=
  match xs with
  | [] => 0
  | x :: xs' => x + sum xs'
  end.

Fixpoint parts_sums_naive (xs : list Z) : list Z :=
  match xs with
  | [] => [0]
  | x :: xs' => sum xs :: parts_sums_naive xs'
  end.

An efficient solution computes the sum of the entire list once, then subtracts each element from the sum as it traverses through the list:

Fixpoint parts_sums_efficient' (acc : Z) (xs : list Z) : list Z :=
  match xs with
  | [] => [acc]
  | x :: xs' => acc :: parts_sums_efficient' (acc - x) xs'
  end.

Definition parts_sums_efficient (xs : list Z) : list Z :=
  let total := sum xs in parts_sums_efficient' total xs.

Show that both approaches yield the same result.

N.B. For convenience, you are allowed to assume functional extensionality, though the axiom is not strictly required for this Kata.

Preloaded

Require Import Coq.ZArith.BinInt.
Open Scope Z_scope.
Require Import List.
Import ListNotations.

Fixpoint sum (xs : list Z) : Z :=
  match xs with
  | [] => 0
  | x :: xs' => x + sum xs'
  end.

Fixpoint parts_sums_naive (xs : list Z) : list Z :=
  match xs with
  | [] => [0]
  | x :: xs' => sum xs :: parts_sums_naive xs'
  end.

Fixpoint parts_sums_efficient' (acc : Z) (xs : list Z) : list Z :=
  match xs with
  | [] => [acc]
  | x :: xs' => acc :: parts_sums_efficient' (acc - x) xs'
  end.

Definition parts_sums_efficient (xs : list Z) : list Z :=
  let total := sum xs in parts_sums_efficient' total xs.