A demonstration of the Derive plugin I wrote for Coq (commit 078efbe in Coq). It helps writing program derivation à la Richard Bird: starting with an executable specification transform it until it is efficient. Writing Derive f From spec Upto eq As h produces a goal |- eq spec ?57. At the end of the proof, two definitions are created f (transpar…

Horner.v

(** In this file we go a little further and follow the derivation
    proposed by Jeremy Gibbons (
    http://patternsinfp.wordpress.com/2011/05/05/horners-rule/ ).  It
    uses the definitions in Scan.v. The problem is to compute the
    maximum sum of consecutive elements in a list [l]. It happens that
    there is a linear time solution for that problem. Again, we start
    with a simple executable specification, and using appropriate
    rewriting steps, we find the linear time solution. *)

Require Import Prelim List NList Scan.
Require Import Coq.Derive.Derive.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Numbers.Integer.Binary.ZBinary.

Open Scope Z_scope.

Definition segments {A:Type} : list A -> nlist∘list A :=
  NList.concat ∘ (NList.map initials) ∘ tails
.

Definition sum : list Z.t -> Z.t := List.fold_right Z.add 0.

(** I'm cheating here because I'm using natural numbers. *)
Definition maximum : nlist Z.t -> Z.t := NList.fold_right Z.max (fun n=>n).

Remark max_cons : forall y z, maximum (cons y z) = Z.max y (maximum z).
Proof.
  reflexivity.
Qed.

Remark max_app : forall y z, maximum (app y z) = Z.max (maximum y) (maximum z).
Proof.
  induction y as [ u | u y hy ].
  + (* case y=one u *)
    reflexivity.
  + (* case y=u:::y *)
    intros z; simpl.
    rewrite !max_cons, hy.
    rewrite Z.max_assoc.
    reflexivity.
Qed.

Lemma maximum_concat : maximum ∘ concat ≡ maximum ∘ (map maximum).
Proof.
  intros l.
  induction l as [ x | x l hl ].
  + (* l=one x *)
    reflexivity.
  + (* l=x:::l *)
    simpl in hl |- *.
    rewrite max_app,hl,max_cons.
    reflexivity.
Qed.

(** Variant that plays well with associativity *)
Corollary maximum_concat_a X (γ:X->_):
  maximum ∘ (concat∘γ) ≡ maximum ∘ ((map maximum) ∘ γ).
Proof.
  intros x.
  apply maximum_concat.
Qed.


Definition mss_spec : list Z.t -> Z.t := maximum ∘ (NList.map sum) ∘ segments.


Derive mss_spec₂ SuchThat (mss_spec ≡ mss_spec₂) As lemma1.
Proof.
  unfold mss_spec; simpl.
  unfold segments; simpl.
  rewrite NList.concat_map_a.
  rewrite maximum_concat_a.
  rewrite !NList.map_map_a.
  rewrite comp_assoc.
  subst mss_spec₂.
  reflexivity.
Qed.

Print mss_spec₂.
(* mss_spec₂ = 
   maximum ∘ (map maximum ∘ (map sum) ∘ initials) ∘ tails
     : list Z.t -> Z.t *)

Definition horner_max (x y:Z.t) := Z.max 0 (Z.add x y).
Lemma max_sum_initials_as_fold :
  maximum ∘ (map sum) ∘ initials ≡ List.fold_right horner_max 0.
Proof.
  (** As explained in J. Gibbons's article, Horner's rule (best know
      for polynomials) is a general property of semi-ring:
      1+u₀u₁+u₀u₁u₂+…+u₀u₁u₂…uₙ = 1+u₀(1+u₁+u₁u₂+…+u₁u₂…uₙ) =
      1+u₀(1+u₁(1+u₂(1+…(1+uₙ)…))) *)
  intros l; induction l as [ | x l hl ].
  + (* case l=[] *)
    reflexivity.
  + (* case l=x::l *)
    simpl in hl |- *.
    rewrite max_cons.
    generalize NList.map_map; intros map_map; unfold eqf in map_map; simpl in map_map.
    rewrite map_map.
    assert (forall x, sum∘(Datatypes.cons x) ≡ (Z.add x)∘sum) as sum_cons.
    { clear; intros x l; revert x.
      induction l as [ | x l hl ].
      all: reflexivity. }
    rewrite sum_cons.
    rewrite <- map_map.
    assert (forall l x, maximum (map (Z.add x) l) = Z.add x (maximum l)) as max_add_distr_l.
    { clear; induction l as [ x | x l hl ].
      + (* case l=one x *)
        reflexivity.
      + intros y; simpl.
        rewrite !max_cons.
        rewrite hl.
        rewrite Z.add_max_distr_l.
        reflexivity. }
    rewrite max_add_distr_l.
    rewrite hl.
    reflexivity.
Qed.

Derive mss SuchThat (mss_spec ≡ mss) As mss_definition.
Proof.
  rewrite lemma1.
  unfold mss_spec₂.
  lazymatch goal with | |- _ ≡ ?f => set (lhs:=f) end.
  rewrite  max_sum_initials_as_fold.
  generalize @scan_lemma; unfold scan_right_spec; intros sl.
  rewrite sl.
  subst mss.
  subst lhs; reflexivity.
Qed.

Print mss.
(* mss = maximum ∘ (scan_right horner_max 0)
     : list Z.t -> Z.t *)
Check mss_definition.
(* mss_definition
     : mss_spec ≡ mss *)

List.v

(** Additional list primitives *)

Require Import Prelim.
Require Export Coq.Lists.List.
Export ListNotations.
Require Import NList.

Definition add_to_tails {A} (x:A) (tails:nlist∘list A) : nlist∘list A :=
  (x::NList.hd tails) ::: tails
.
Definition tails {A} : list A -> nlist∘list A :=
  List.fold_right add_to_tails (one [])
.

Definition add_to_initials {A} (x:A) (initials:nlist∘list A) : nlist∘list A :=
  [] ::: (NList.map (List.cons x) initials)
.
Definition initials {A} (l:list A) : nlist∘list A :=
  List.fold_right add_to_initials (one []) l
.

NList.v

(** The type of non-empty lists. *)

Require Import Coq.Classes.Morphisms.
Require Import Prelim.

Inductive nlist (A:Type) :=
| one (x:A)
| cons (x:A) (l:nlist A)
.
Arguments one {A} x.
Arguments cons {A} x l.

Notation "x ::: l" := (cons x l) (at level 60, right associativity).

Definition hd {A} (l:nlist A) : A :=
  match l with
  | one x => x
  | x:::_ => x
  end
.

Fixpoint map {A B} (f:A->B) (l:nlist A) : nlist B :=
  match l with
  | one x => one (f x)
  | x:::l => cons (f x) (map f l)
  end
.

Fixpoint fold_right {A B} (f:A->B->B) (g:A->B) (l:nlist A) : B :=
  match l with
  | one x =>  g x
  | x:::l => f x (fold_right f g l)
  end
.

Fixpoint app {A} (l₁ l₂:nlist A) : nlist A :=
  match l₁ with
  | one x => x:::l₂
  | x:::l₁ => x ::: (app l₁ l₂)
  end
.

Fixpoint concat {A} (l:nlist (nlist A)) : nlist A :=
  match l with
  | one x => x
  | x:::l => app x (concat l)
  end
.

Instance map_eqf A B : Proper (eqf==>eqf) (@map A B).
Proof.
  intros f₁ f₂ hf l.
  induction l as [ x | x l hl ].
  + (* case l=one x *)
    simpl.
    rewrite hf.
    reflexivity.
  + (* case l=x:::l *)
    simpl.
    rewrite hf,hl.
    reflexivity.
Qed.

Instance map_eq A B : Proper (eqf ==> eq ==> eq) (@map A B).
Proof.
  intros f₁ f₂ hf l ? <-.
  apply map_eqf.
  assumption.
Qed.

Lemma hd_map {A B} (f:A->B) : forall l, hd (map f l) = f (hd l).
Proof.
  now destruct l.
Qed.

Lemma map_app A B (f:A->B) (l₁ l₂:nlist A) :
  map f (app l₁ l₂) = app (map f l₁)  (map f l₂).
Proof.
  induction l₁ as [ x | x l₁ hl₁ ].
  + (* case l₁=one x *)
    reflexivity.
  + (* case l₁=x:::l₁ *)
    simpl.
    rewrite hl₁.
    reflexivity.
Qed.

Lemma concat_map A B (f:A->B) :
  (map f) ∘ concat ≡ concat ∘ (map (map f)).
Proof.
  intros l.
  induction l as [ x | x l hl ].
  + (* case l=one x *)
    reflexivity.
  + (* case l=x:::l *)
    simpl.
    rewrite map_app.
    simpl in hl; rewrite hl.
    reflexivity.
Qed.

(** Variant that plays well with associativity *)
Corollary concat_map_a A B X (f:A->B) (γ:X->_) :
  (map f) ∘ concat ∘ γ ≡ concat ∘ (map (map f)) ∘ γ.
Proof.
  intros x.
  apply concat_map.
Qed.

Lemma map_map A B C (f:A->B) (g:B->C) : (map g) ∘ (map f) ≡ map (g∘f).
Proof.
  intros l.
  induction l as [ x | x l hl ].
  + (* case l=one x *)
    reflexivity.
  + (* case l=x:::l *)
    simpl.
    simpl in hl; rewrite hl.
    reflexivity.
Qed.

(** Variant that plays well with associativity *)
Corollary map_map_a A B C X (f:A->B) (g:B->C) (γ:X->_) :
  (map g) ∘ (map f) ∘ γ ≡ (map (g∘f)) ∘ γ.
Proof.
  intros x.
  apply map_map.
Qed.

Prelim.v

(** Composition, extensional equality, and a few lemma. *)

Require Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Definition composition {A B C} (f:A->B) (g:B->C) (x:A) := g (f x).
Arguments composition {A B C} f g x /.
Notation "f ∘ g" := (composition g f) (at level 5, right associativity).

Definition eqf {A B} (f g:A->B) : Prop := forall x, f x = g x.
Notation "f ≡ g" := (eqf f g) (at level 70).

Instance eqf_equiv {A B} : Equivalence (@eqf A B).
Proof.
  split.
  all: compute; congruence.
Qed.

Instance comp_eqf A B C : Proper (eqf==>eqf==>eqf) (@composition A B C).
Proof.
  intros f₁ f₂ hf g₁ g₂ hg x; simpl.
  rewrite hf,hg.
  reflexivity.
Qed.

Lemma comp_assoc A B C D (f:A->B) (g:B->C) (h:C->D) :
  (h∘g)∘f ≡ h∘(g∘f).
Proof.
  reflexivity.
Qed.

Lemma app_eq {A B} (f:A->B) {x y:A} : x = y -> f x = f y.
Proof.
  intros <-. reflexivity.
Qed.

Lemma eq_app (A B:Type) (f g:A->B) (x:A) : f = g -> f x = g x.
Proof.
  intros <-. reflexivity.
Qed.
Lemma eq_app2 (A B C:Type) (f g:A->B->C) x y : f = g -> f x y = g x y.
  intros <-. reflexivity.
Qed.

Scan.v

(** In this file I use the Derive plugin to get a linear time
    definition of [scan_right] starting from the more obvious yet
    inefficient definition: [scan_right f s l] is like doing
    [fold_right f s] on every terminal segment of [l]. *)

Require Import Prelim List NList.
Require Coq.Derive.Derive.
Require Import Coq.Classes.RelationClasses.

Section Scan.

  Context {A B:Type}.
  Context (f:A->B->B) (s:B).

  Definition scan_right_spec : list A -> nlist B :=
    (NList.map (List.fold_right f s)) ∘ tails.

  Derive scan_right SuchThat (scan_right_spec ≡ scan_right)  As scan_lemma.
  Proof.
    unfold scan_right_spec.
    unfold tails. subst scan_right.
    (* we want to express scan_right as a single [fold_right]. *)
    refine (transitivity (y := List.fold_right _ _) _ _); shelve_unifiable; [ | reflexivity ].
    intros l.
    induction l as [ | x l hl ].
    + (* l=[] *)
      simpl.
      reflexivity.
    + (* l=x::l *)
      simpl in hl |- *.
      rewrite hl.
      apply (app_eq hd) in hl.
      rewrite hd_map in hl.
      rewrite hl; clear hl.
      lazymatch goal with | |- _ = _ _ ?r => set (acc:=r) end.
      lazymatch goal with | |- ?rhs = _ => change rhs with ((fun x acc => f x (hd acc) ::: acc) x acc) end.
      apply eq_app2.
      reflexivity.
  Qed.

  Print scan_right.
  (* scan_right = 
List.fold_right (fun (x : A) (acc : nlist B) => f x (hd acc) ::: acc) (one s)
     : list A -> nlist B *)
  Check scan_lemma.
  (* scan_lemma
     : scan_right_spec ≡ scan_right *)

End Scan.