IVE READ CPDT

Certified Programming with Dependent Types

DOESNT GET MORE EXPERT THAN THIS http://adam.chlipala.net/cpdt/

Coq is awesome. I also read CPDT, and a bit of Software Foundations ( http://www.cis.upenn.edu/~bcpierce/sf/ ). My experience is that reading examples and doing exercises can make it seem easy but in reality verified software and formal proofs are difficult as fuck. Things that seem obvious turn out to be pretty hard to prove.

A week ago someone mentioned http://reprog.wordpress.com/2010/04/19/are-you-one-of-the-10-percent/ , so I coded up a Racket version of binary search in 30 minutes, making sure to get it right.

#lang racket

(require srfi/67)

(define (bsearch v e #:compare [compare default-compare])
  (let loop ((l 0) (u (vector-length v)))
    (if (= l u)
        #f
        (let ((h (+ l (quotient (- u l) 2))))
          (if3 (compare e (vector-ref v h))
            (loop l h)
            h
            (loop (+ h 1) u))))))

It seemed fine after testing, but like Dijkstra said: testing can be used to show the presence of bugs, but never to show their absence. That's why I set out to write it in Coq. So far I've only got it defined and proven to terminate.

Require Import Arith.
Require Import List.
Require Import Div2.
Require Import Program.

Lemma div2_lt_le : forall n m, n < m -> div2 n <= div2 m.
intro n. pattern n. apply ind_0_1_SS.
  auto with arith.
  auto with arith.
  intros. destruct m.
    inversion H0.
    destruct m.
      apply lt_S_n in H0. inversion H0.
      simpl. apply le_n_S. repeat apply lt_S_n in H0. exact (H m H0).
Qed.

Lemma div2_double_lt_le : forall n m, n < m -> n <= div2 (n + m).
intros.
rewrite <- div2_double at 1. apply div2_lt_le.
replace (2 * n) with (n + n).
  auto with arith.
  simpl. auto with arith.
Qed.

Lemma lt_div2' : forall l u, l < u -> div2 (l + u) < u.
intro l. pattern l. apply ind_0_1_SS.
  intros. auto with arith.

  intros. destruct u.
    inversion H.
    destruct u.
      auto with arith.
      replace (div2 _) with (S (div2 (S u))) by auto. auto with arith.

  intros. destruct u.
    inversion H0.
    destruct u.
     apply lt_S_n in H0. inversion H0.
     replace (_ + _) with (S (S (S (S (n + u))))).
       simpl. repeat apply lt_n_S. repeat apply lt_S_n in H0. auto with arith.
       repeat rewrite <- plus_Snm_nSm. reflexivity.
Qed.

Lemma minus_lt_compat_l : forall a n m, m < n -> n <= a -> a - n < a - m.
  induction a.
    intros. inversion H0. subst n. inversion H.

    intros. destruct n.
      inversion H.
      destruct m.
        auto with arith.
        simpl. auto with arith.
Qed.

Lemma minus_lt_compat_r : forall a n m, n < m -> a <= n -> n - a < m - a.
  induction a.

  intros. repeat rewrite <- minus_n_O. assumption.
  intros. destruct n.
    inversion H0.
    destruct m.
      inversion H.
      simpl. auto with arith.
Qed.

Program Fixpoint bsearch'
  (v : list nat)
  (e : nat)
  (l : nat)
  (u : { x : nat | l <= x})
  { measure (u - l) } :=
if le_lt_dec u l
then
  None
else
  let i := div2 (l + u) in
    match nat_compare e (nth i v 0) with
    | Lt => bsearch' v e l i
    | Eq => Some i
    | Gt => bsearch' v e (S i) u
end.
Obligation 1.
apply div2_double_lt_le. assumption.
Qed.
Obligation 2.
assert (div2 (l + u) < u).
  apply lt_div2'. assumption.
  apply minus_lt_compat_r.
    assumption.
    apply div2_double_lt_le. assumption.
Qed.
Obligation 3.
apply lt_div2'. assumption.
Qed.
Obligation 4.
apply minus_lt_compat_l.
  unfold lt. apply le_n_S. apply div2_double_lt_le. assumption.
  apply lt_div2'. assumption.
Qed.

Program Definition bsearch l e := bsearch' l e 0 (length l).
Obligation 1. auto with arith. Qed.

To prove that it actually returns correct results I'm going to try to prove this:

Require Import Sorted.

Lemma bsearch_correct_positive : forall l e n,
Sorted le l ->
bsearch l e = Some n -> (nth n l 1) = e.
Admitted.

Lemma bsearch_correct_negative : forall l e,
Sorted le l -> bsearch l e = None -> ~ In e l.
Admitted.