The Coq source of this tutorial is available here.

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

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.

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.

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.

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).

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`

.

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 `:=!`

.

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.

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.