IVE READ CPDT

Certified Programming with Dependent Types

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

The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science.

How exactly is this relevant to our interests? Did you ever find
 yourself saying: "I wish I could *PROVE* this research project
 correct?"

me neither

practical engineering with the Coq
practical engineering with the Cock

>>3
`Coq' is French for `cock' (the rooster).

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.

Learn Coq today and become a PROGRAMMEUR EXPERT!

Learn Coq today and become and EXPERT PROGRAMMEUR

Learn programming today and become an EXPERT DICK!

>>5
Dude you can prove that mathematically in shorter than that. Either Coq sucks or you suck (at) Coq.

>>5
char *bsearch(char *a, char e, int n) {
 char *l=a, *r=l+n-1;
 for(;;) {
  char *m = l+(r-l+1)/2;
  if(l>=r)
   if(*m==e)
    return m;
   else
    return 0;
  else if(e>*m)
   l = m;
  else
   r = m;
 }
}

>>9
Computers don't read maths, there are more complex proofs that require interpretation of written language to prove. For example, Cantor's diagonal argument can be stated concisely but codifying it is another story. Coq has to put up with taking codified input only (obviously), so things can get verbose.

Besides, the contents of >>5 contains a lot of explicit details you would simply refer to, or take for granted: check out the "Lemma div2_double_lt_le" -- it's actually quite short when you think about it. The need for its presence might be frustrating on the other hand.

Incidentally, I'm not the biggest fan of Coq. I think it's great that it exists but I would never use it. The problem with provers: they're complex to write for, and what happens if you make a mistake when expressing your requirements? How likely is it that you might encounter requirements more difficult to codify than to satisfy correctly in code? I think the chances of wasting quite a lot of time are too high.