Get started

The Coq source of this tutorial is available here.

Install with OPAM

Make sure that you added the Coq repository:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-cybele

Hello world

Here is our first program:

Require Import Cybele.
Require Import String.
Import Monad.
Definition hello := print_string (sig := Sig.empty) "Hello world!".

It prints a message in the Cybele monad. If we check its type:

Check hello.

we get M Sig.empty unit. So we return a value of type unit in the monad. The Sig.empty tells we are using no memory. We run it:

Compute run hello 0.

The message is written in the output trace.

Program in the monad

We write the return operation ret. For the bind, we postfix common constructs by a !:

Compute run (sig := Sig.empty) (
  let! x := ret 12 in
  do! print_string "Twelve: " in
  print x) 0.

The let! does the bind. The do! sequences two instructions. We see that print is actually polymorphic and can display any kind of value.

Reflexive proofs

It is nice to run programs in the Cybele monad. But we ultimately want to extract their results to proofs in order to write decision procedures. Here comes the cybele tactic:

Lemma easy: True.
  cybele (ret (sig := Sig.empty) I).
Defined.

It extracts from an expression of type M sig A a value of type A (if the computation successes). For this example the proof of True is trivially I. In order to save space, the proof is implemented by reflexivity:

Print easy.

returns proof_by_reflection (ret I) ... eq_refl. The proofs holds the full monadic expression which is executed at type-checking time.

Fixpoints

We do not need to prove termination to write recursive functions:

Require Import Arith.Div2.
Definition log2: nat -> M Sig.empty nat :=
  fix_ (fun log2 n =>
    match n with
    | 0 | 1 => ret 0
    | _ =>
      let! r := log2 (div2 n) in
      ret (r + 1)
    end).

The general fixpoint operator is fix_, or dependent_fix in a dependently typed form. We compute the logarithm in base two without giving the induction principle for recursive calls on div2. But if we evaluate directly:

Compute run (log2 256) 0.

it returns "Not terminated". We need to feed in the maximal number of steps allowed, let us say 100 for safety:

Compute run (log2 256) 100.

Now we get 8. We could even write non-terminating programs:

Definition infinite: unit -> M Sig.empty unit :=
  fix_ (fun infinite _ => infinite tt).

Exceptions

We often need to write partial functions, especially in the case of decision procedures which work only on valid inputs. If we rewrite the logarithm function to handle the zero case:

Definition log2_error: nat -> M Sig.empty nat :=
  fix_ (fun log2_error n =>
    match n with
    | 0 => error "Log of zero."
    | 1 => ret 0
    | _ =>
      let! r := log2 (div2 n) in
      ret (r + 1)
    end).

we get an exception running it on zero. It is possible to catch them with the try! construct:

Compute run (try! log2_error 0 with _=> ret 0) 100.
Finally, we can lift option types to the monad using extract_some:
Compute run (sig := Sig.empty) (extract_some (Some 23)) 0.

answers 23.

References

The temporary memory is the main memory system, allowing to use references. Due to the type-system of Coq we need to type this dynamically allocated memory. The programmer gives a signature, the list of types which will be allocated in the memory. If we only need a natural number:

Require Import List.
Import ListNotations.
Definition sig := Sig.Make nil [nat: Type].

We manipulate references with a syntax similar to OCaml:

Definition twenty :=
  let! r := tmp_ref sig 0 12 in
  let! v := !r in
  do! r :=! v + 8 in
  !r.

computes the value 20. Allocation is done with tmp_ref sig 0 12, the index 0 being an index in the signature referring to the type nat. Dereferencings and assignments are done with ! and :=!.

Allocate many references

If we try to allocate another nat reference we get an error:

Definition two_refs :=
  let! r1 := tmp_ref sig 0 12 in
  let! r2 := tmp_ref sig 0 14 in
  !r1.
returns "The reference is already allocated". This is because there can be only one allocation per element of the signature. They are two solutions for our program. We can extend the signature if we know we will allocate only two references:
Definition sig_couple := Sig.Make nil [nat: Type; nat: Type].
Definition two_refs_couple :=
  let! r1 := tmp_ref sig_couple 0 12 in
  let! r2 := tmp_ref sig_couple 1 14 in
  !r1.
Or we can use an extensible container such as a list:
Definition sig_list := Sig.Make nil [list nat: Type].
Definition two_refs_list :=
  let! l := tmp_ref sig_list 0 [12; 14] in
  let! l_value := !l in
  extract_some (nth_error l_value 0).

It may be viewed as a limitation to have fixed number of allocations, but in practice it was always possible for us to overcome that using references to containers.

Pre-computations

Complex results can be pre-computed efficiently by the OCaml back-end. The program is executed twice, first in OCaml (the code is generated using the extraction mechanism) and then in Coq, using results given by the first execution.

The communication between the two is done through the input memory. It has the same behavior as the temporary memory, except that its final value after the first execution is saved and given as an initial memory value to Coq. The idea is that OCaml will write in it while Coq will read it. To encode these two behaviors, there is the select f g operator. It executes f in Coq but g in OCaml.

comments powered by Disqus