sum.v

Inductive SumList : nat -> Type :=
  | s_nil : SumList 0
  | s_cons : forall n {m}, SumList m -> SumList (m + n).

Require Import List Compare_dec.
Fixpoint prefix_sum_lists (l : list nat) : list {n: nat & SumList n} :=
   match l with
   | nil => nil
   | n :: l0 =>
       existT SumList n (s_cons n s_nil)
       :: map (λ H : {n0 : nat & SumList n0},
             let (x, s) := H in existT (λ n0 : nat, SumList n0) (x + n) (s_cons n s))
            (prefix_sum_lists l0)
   end.

Fixpoint sum_lists (l : list nat) : list {n: nat & SumList n} := 
  match l with
    | nil => nil
    | n :: l0 => prefix_sum_lists l ++ sum_lists l0
  end.

Fixpoint to_list n (l : SumList n): list nat := 
   match l with
   | s_nil => nil
   | s_cons n m l => n :: to_list m l
   end.

Definition max_list (l : list nat) : list nat :=
  let (n,l) := fold_right (fun x y => if le_dec (projT1 x) (projT1 y) then x else y) (existT _ _ s_nil) (sum_lists l)
    in to_list n l.