Verification of a Fulcrum implementation against a reference implementation in Coq

fulcrum.v

Require Import List.
Require Import FunctionalExtensionality.
Require Import ZArith.
Require Import Zcompare.

(* c.f. https://twitter.com/Hillelogram/status/987432184217731073 *)

Set Implicit Arguments.

Lemma map_combine : forall A B C (f : A -> B) (g : A -> C) xs,
  map (fun x => (f x, g x)) xs = combine (map f xs) (map g xs).
Proof. induction xs; simpl; congruence. Qed.

Section Positions.

  Hypothesis A : Type.

  Fixpoint positions' (idx : nat) (xs : list A) :=
    match xs with
    | nil     => idx :: nil
    | _ :: xs => idx :: positions' (S idx) xs
    end.

  Definition positions := positions' 0.

End Positions.

Section Take.

  Hypothesis A : Type.

  Fixpoint take (n : nat) (xs : list A) :=
    match n, xs with
    | O,   _       => nil
    | _,   nil     => nil
    | S n, x :: xs => x :: take n xs
    end.

  Lemma take_all : forall xs ys, take (length xs) (xs ++ ys) = xs.
  Proof. induction xs; simpl; congruence. Qed.

  Fixpoint drop (n : nat) (xs : list A) :=
    match n, xs with
    | O,   xs    => xs
    | S n, nil   => nil
    | S n, _::xs => drop n xs
    end.

  Lemma drop_all : forall xs ys, drop (length xs) (xs ++ ys) = ys.
  Proof. induction xs; simpl; congruence. Qed.

  Fixpoint prefixes' (acc : list A) (xs : list A) : list (list A) :=
    match xs with
    | nil     => rev acc :: nil
    | x :: xs => rev acc :: prefixes' (x::acc) xs
    end.

  Lemma prefixes'_app : forall xs ys zs,
    prefixes' (zs ++ ys) xs = map (fun ps => rev ys ++ ps) (prefixes' zs xs).
  Proof.
    induction xs; intros ys zs; simpl.
    - rewrite rev_app_distr. reflexivity.
    - rewrite rev_app_distr. apply f_equal.
      replace (a :: zs ++ ys) with ((a::zs) ++ ys) by reflexivity.
      apply IHxs.
  Qed.

  Lemma prefixes'_singl (a : A) (xs : list A) :
    prefixes' (a :: nil) xs = map (fun ps => a :: ps) (prefixes' nil xs).
  Proof.
    replace (a::nil) with (nil ++ a::nil) by reflexivity. apply prefixes'_app.
  Qed.

  Definition prefixes := prefixes' nil.

  Lemma take_positions_prefixes' : forall xs ys,
      map (fun n : nat => take n (rev ys ++ xs)) (positions' (length ys) xs)
    = prefixes' ys xs.
  Proof.
    induction xs; simpl; intros ys.
    - replace (length ys) with (length (rev ys)) by apply rev_length. 
      rewrite take_all.
      reflexivity.
    - apply f_equal2.
      + replace (length ys) with (length (rev ys)) by apply rev_length.
        apply take_all.
      + replace (rev ys ++ a :: xs) with (rev (a :: ys) ++ xs)
             by (simpl; rewrite <- app_assoc; reflexivity).
        replace (S (length ys)) with (length (a :: ys))
             by trivial.
        apply IHxs.
  Qed.

  Lemma take_positions_prefixes (xs : list A) :
     map (fun n : nat => take n xs) (positions xs) = prefixes xs.
  Proof. exact (take_positions_prefixes' xs nil). Qed.

  Fixpoint suffixes (xs : list A) : list (list A) :=
    match xs with
    | nil   => nil :: nil
    | _::ys => xs :: suffixes ys
    end.

  Lemma drop_positions_suffixes' : forall xs ys,
    map (fun x : nat => drop x (ys ++ xs)) (positions' (length ys) xs) = suffixes xs.
  Proof.
    induction xs; simpl; intros ys.
    - rewrite drop_all. reflexivity.
    - rewrite drop_all. apply f_equal.
      replace (ys ++ a :: xs) with ((ys ++ a :: nil) ++ xs)
         by (rewrite <- app_assoc; reflexivity).
      replace (S (length ys)) with (length (ys ++ a :: nil))
         by (rewrite app_length; rewrite Plus.plus_comm; reflexivity).
      apply IHxs.
  Qed.

  Lemma drop_positions_suffixes (xs : list A) :
    map (fun x : nat => drop x xs) (positions xs) = suffixes xs.
  Proof. exact (drop_positions_suffixes' xs nil). Qed.

End Take.

Section Scan.

  Hypothesis A : Type.
  Hypothesis op : A -> A -> A.
  
  Fixpoint scan_left (accum : A) (xs : list A) : list A :=
    match xs with
    | nil     => accum :: nil
    | x :: xs => accum :: scan_left (op accum x) xs
    end.

  Lemma scan_fold_left : forall xs init,
    map (fun xs => fold_left op xs init) (prefixes xs) = scan_left init xs.
  Proof.
    induction xs; intro init; simpl.
    - reflexivity.
    - apply f_equal. rewrite prefixes'_singl. rewrite map_map. apply IHxs.
  Qed.

  Fixpoint scanr' (init : A) (xs : list A) : list A * A :=
    match xs with
    | nil => (init :: nil, init)
    | x :: xs =>
       let (ys, accum) := scanr' init xs in
       let accum       := op x accum in
       (accum :: ys, accum)
    end.

  Definition scan_right init xs := fst (scanr' init xs).

  Lemma scan_fold_right' (init : A) (xs : list A) :
    (map (fold_right op init) (suffixes xs), fold_right op init xs) = scanr' init xs.
  Proof.
    induction xs; simpl.
    - reflexivity.
    - destruct (scanr' init xs). inversion IHxs. congruence.
  Qed.

  Lemma scan_fold_right (xs : list A) (init : A) :
    map (fold_right op init) (suffixes xs) = scan_right init xs.
  Proof.
    unfold scan_right. rewrite <- scan_fold_right'. reflexivity.
  Qed.

End Scan.

Definition sum xs := fold_left (Z.add) xs 0%Z.

Definition diff p := Z.abs (fst p - snd p).

Definition fv xs i := diff (sum (take i xs), sum (drop i xs)).

Definition update_min_index p z :=
  match p with
  | (None, idx)           => (Some (z, 0), S idx)
  | (Some (z',idx'), idx) =>
      match (z ?= z')%Z with
      | Lt => (Some (z, idx), S idx)
      | _  => (Some (z', idx'), S idx)
      end
  end.

Definition min_index xs :=
  match fold_left update_min_index xs (None, 0) with
  | (None, _)          => None
  | (Some (_, idx), _) => Some idx
  end.

Definition fulcrum_spec xs :=
  min_index (map (fv xs) (positions xs)).

Definition fulcrum xs :=
  min_index
    (map diff (combine (scan_left Z.add 0%Z xs) (scan_right Z.add 0%Z xs))).

Lemma fulcrum_correct : forall xs, fulcrum_spec xs = fulcrum xs.
Proof.
  intros xs. unfold fulcrum_spec. unfold fv. unfold fulcrum.
  apply f_equal.
  rewrite <- map_map.
  apply f_equal.
  rewrite map_combine.
  apply f_equal2.
  - rewrite <- map_map. rewrite take_positions_prefixes. apply scan_fold_left.
  - rewrite <- map_map. rewrite drop_positions_suffixes. rewrite <- scan_fold_right.
    apply f_equal2.
    + extensionality ys. apply fold_symmetric; auto with zarith.
    + reflexivity.
Qed.

(* Tests! *)

Lemma test1 : fulcrum (5 :: 5 :: 10 :: nil)%Z = Some 2.
reflexivity. Qed.

Lemma test2 : fulcrum (1 :: 2 :: 3 :: 4 :: 5 :: -7 :: nil)%Z = Some 2.
reflexivity. Qed.