➲  Date: Wed, 17 Aug 2011 21:01:56 +0200; Tags: [ocaml; coq].

For me, the future of programming should be to keep coding in OCaml, and start replacing some modules by formally proved Coq code. The direct Coq code would be extracted to OCaml, or would be generating the 1% performance-critical code which needs to be (meta‑)programmed in C or Assembler.

To start learning Coq, I definitely recommend Software Foundations by Pierce et al.: http://www.cis.upenn.edu/~bcpierce/sf/

• It is freely available on-line.
• It is very well written by very good teachers.
  The exercises are very progressive. With a very pragmatic approach, SF makes you really “touch” the Curry-Howard Isomorphism and digest Coq's features little by little.
  Actually, to my humble bibliographic knowledge, the 10 first chapters of SF are already the best book ever written on Computer Science.
• It is addictive.
  We call it the Video Game Effect.
  And really, imagine yourself hacking some proofs: ‘Well, it is late, and there is a cool movie on TV … but … OK, just one more theorem …’ and you end up at two in the morning with zombie-eyes but proud of your n-th four-stars exercise solved.

SF teaches you how to become a Coq beginner. The next step is then to learn how to really program and do engineering with Coq. For this, there is Certified Programming with Dependent Types by Adam Chlipala: http://adam.chlipala.net/cpdt/. It is very interesting and seems to be the way to go.

I have been on it for some time now and I find it quite difficult though. It goes maybe too fast for me on many things and it has a lot of notations, ad-hoc libraries, and inter-dependencies.

So, let's take some time here to make some “raw Coq” with good notations (I mean textual, explicit, easy to remember), in slow motion, and trying to detail as much as possible, in the hope it will be useful for others.

The following is intended for Coq beginners like me, i.e., people who have been learning with SF (or other) for some time and who want to program.

And let's start with subsets. The fast introduction is in CPDT's Subset chapter (which deals with much more than the sig type).

What follows is generated from a Coq development available on-line; you can run it with your favourite Coq-environment. As I am a beginner, there are certainly things poorly implemented; the goal is to understand and move on to the next steps. Do not hesitate to correct me in the comments.

The blue blocs are the actual Coq code, the grey/indented blocs are not executed (output examples, quotes from the standard library, etc.).

We start with this classical command, everything else we need for now is already in Coq's pre-loaded module of the standard library (the Prelude module). The type sig(The name comes from “Sigma”; Σ-Types.) is defined in the Specif module together with the associated notations: For instance, {x : nat | x > 42} is the type of the naturals strictly bigger than 42.

We also need False_rec (defined while defining the False in the Logic module). It will be useful to be able to put “something” for the cases which never happen (i.e. an “assert false” in OCaml).

This deserves a few more notations:

Let's start with the simplest example I could find. A function returning the successor of a natural number, and telling so in its type: It uses the refine tactic (see also this example) which

allows to give an exact proof, […] like exact, with a big difference: the user can leave some holes (denoted by _ or (_:type)) in the term. refine will generate as many subgoals as they are holes in the term.

The hack is to use refine to provide the body of the function definition while in proof mode; and hence be able to provide the proof(s) of the specification part later. In our case, there is only one generated subgoal (by the second “_” in the Sig_yes notation) and it is (solved by) trivial.

Without the refine tactic we would have to provide the (P x) argument of the exist constructor “by hand”: The first underscore is inferred by Coq (not through refine): Anyway, this would not scale to more complex types (it took me already quite some time to come up with the right eq and eq_refl). With refine instead, we let underscores for the “proofs” and we provide them later with usual Coq tactics.

Do not forget the Defined instead of Qed, so that Coq keeps the proof of the definition (with Qed, it would become “Opaque”).

We can already check the generated OCaml code:

(** val succ_strong : nat -> nat **)
let succ_strong n =
  S n

Let's see another example: pred_strong which can be called only for n > 0. This time two goals remain to fill … pred_strong would be now perfectly usable, but we are not yet completely happy because the proof is not “well engineered”: it references internal-state stuff like “_H”, and it depends on the order of the subgoals(CPDT has plenty of very interesting discussions and justifications about the subject, e.g. in the “Intro” or the “Large” chapters.). We can put everything together in one “chain of tactics” without having references to local variables. We use the solve tactic which simply tries to solve the goal with one of the branches given as arguments. We match the goal looking for hypotheses looking like the previous _H to invert them, for the other goal, we call auto. That's nicer. For posterity, we can also define the two following pieces of Ltac which are reusable and mostly clean. solve_by_inversion will try to solve the goal by inverting all the hypotheses(There is a more complete/searching one on Cocorico, the Coq wiki.). invert_or_auto tries the previous one, and if it fails then auto. With them, we can solve this even more elegantly:

Now the funny part: the function pred_strong takes as input an implicit natural number n and a “proof that n > 0”:

= Sig_yes 1
: {m : nat | 2 = S m}

Anyway, in OCaml, it still looks pretty normal:

(** val pred_strong : nat -> nat **)

let pred_strong = function
| O -> assert false (* absurd case *)
| S pn -> pn 

The eager reader can continue with CPDT's Subset chapter to see more implementations of “pred” with other rich dependent types.

Here is an implementation of List.map with a sig return type specifying what the result actually is. We use Coq's basic lists and we describe what the map function should do with an inductive proposition. map_spec links the input list, the input function and the resulting function.

Here is the signature of the specified_map: Simply because it is fun, we use the Proof with command which gives a meaning to the “...” notation. We feed auto with the constructors of map_spec (this could have been done also with a Hint). Without the notation Sig_take, we simply do pattern matching with one case: and that's done. But If we want to play with the notation, we introduce a tiny problem: There we are stuck with a (let (ex, _) := fx f t in ex) in the middle of the goal which auto does not want to expand any more … We can ask Coq to force it: And get the “Proof Completed” but we can still try to make something cleaner. After a bit of googling-trial-and-error, we get a tactic to force the destruct on our notation.

Let's do some tests …

= Sig_yes (42 :: 43 :: 44 :: 46 :: nil)
: {lm : list nat |
 map_spec (fun x : nat => x + 42) (0 :: 1 :: 2 :: 4 :: nil) lm}

We can also call pred_strong on a list of wrapped positive naturals:

= Sig_yes (0 :: 1 :: 2 :: nil)
: {lm : list nat |
  map_spec
    (fun t : strictly_positive =>
     match t with
     | gt_0 x x_gt_0 => let (ex, _) := pred_strong x_gt_0 in ex
     end) (gt_0 one_gt_0 :: gt_0 two_gt_0 :: gt_0 three_gt_0 :: nil) lm}

Finally, let's have a look at the OCaml code:

type 'a list =
| Nil
| Cons of 'a * 'a list

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was exist *)

(** val specified_map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec specified_map f = function
| Nil -> Nil
| Cons (h, t) -> Cons ((f h), (specified_map f t))

That's all for today. Next time, again from the Specif module: the sumbool type.

---

blog comments powered by Disqus