## Coq Programming with Subsets

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.### About Learning Coq

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*.### Subsets with the `sig` Type

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

#### Prelude

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 For instance,

Set Implicit Arguments.

`sig`(The name comes from “Sigma”; Σ-Types.) is defined in the Specif module together with the associated notations:
Inductive sig (A : Type) (P : A -> Prop) : Type :=

exist : forall x : A, P x -> sig P

Notation "{ x | P }" := (sig (fun x => P)) : type_scope.

Notation "{ x : A | P }" :=

(sig (fun x:A => P)) : type_scope.

exist : forall x : A, P x -> sig P

Notation "{ x | P }" := (sig (fun x => P)) : type_scope.

Notation "{ x : A | P }" :=

(sig (fun x:A => P)) : type_scope.

`{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:

Notation "'Sig_no'" := (False_rec _ _) (at level 42).

Notation "'Sig_yes' e" := (exist _ e _) (at level 42).

Notation "'Sig_take' e" :=

(match e with Sig_yes ex => ex end) (at level 42).

Notation "'Sig_yes' e" := (exist _ e _) (at level 42).

Notation "'Sig_take' e" :=

(match e with Sig_yes ex => ex end) (at level 42).

#### Examples

##### The Trivial One

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

Definition succ_strong: forall (n : nat), {m : nat | m = S n}.

refine (fun n => Sig_yes (S n)). trivial.

Defined.

refine (fun n => Sig_yes (S n)). trivial.

Defined.

Theallows to give an exact proof, […] likeexact, with a big difference: the user can leave some holes (denoted by_or(_:type)) in the term.refinewill generate as many subgoals as they are holes in the term.

*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 The first underscore is inferred by Coq (not through Anyway, this would not scale to more complex types (it took me already quite some time to come up with the right

`refine`tactic we would have to provide the`(P x)`argument of the`exist`constructor “by hand”:
Definition succ_strong_by_hand:

forall (n : nat), {m : nat | m = S n} :=

fun n =>

exist (* The P : A -> Prop *) _

(* The x : A *) (S n)

(* The P x *) (eq_refl (S n)).

forall (n : nat), {m : nat | m = S n} :=

fun n =>

exist (* The P : A -> Prop *) _

(* The x : A *) (S n)

(* The P x *) (eq_refl (S n)).

`refine`):
Definition succ_strong_no_inference_at_all:

forall (n : nat), {m : nat | m = S n} :=

fun n =>

exist (* The P : A -> Prop *) (fun t => eq t (S n))

(* The x : A *) (S n)

(* The P x *) (eq_refl (S n)).

forall (n : nat), {m : nat | m = S n} :=

fun n =>

exist (* The P : A -> Prop *) (fun t => eq t (S n))

(* The x : A *) (S n)

(* The P x *) (eq_refl (S n)).

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

Extraction succ_strong.

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

##### A Non-Total Function

Let's see another example: This time two goals remain to fill … We can put everything together in one “chain of tactics” without having references to local variables. We use the That's nicer. For posterity, we can also define the two following pieces of With them, we can solve this even more elegantly:

`pred_strong`which can be called only for`n > 0`.
Definition pred_strong :

forall n : nat, n > 0 -> {m : nat | n = S m}.

refine (fun n =>

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end).

forall n : nat, n > 0 -> {m : nat | n = S m}.

refine (fun n =>

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end).

(* n : nat _H : 0 > 0 |- False *)

inversion _H.

(* n : nat pn : nat _H : S pn > 0 |- S pn = S pn *)

reflexivity.

(* Proof Completed. *)

inversion _H.

(* n : nat pn : nat _H : S pn > 0 |- S pn = S pn *)

reflexivity.

(* Proof Completed. *)

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

`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`.
refine (fun n =>

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end);

solve

[ match goal with H: 0 > 0 |- _ => inversion H end

| auto ].

(* Proof Completed. *)

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end);

solve

[ match goal with H: 0 > 0 |- _ => inversion H end

| auto ].

(* Proof Completed. *)

`Ltac`which are reusable and*mostly*clean.
Restart.

`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.).
Ltac solve_by_inversion :=

match goal with

| H:_ |- _ =>

solve [ inversion H | clear H; solve_by_inversion

| fail 2 "Could not solve by inversion" ]

end.

match goal with

| H:_ |- _ =>

solve [ inversion H | clear H; solve_by_inversion

| fail 2 "Could not solve by inversion" ]

end.

`invert_or_auto`tries the previous one, and if it fails then`auto`.
Ltac invert_or_auto :=

try solve_by_inversion;

solve [ auto

| fail 2 "Could not solve by inversion nor auto" ].

try solve_by_inversion;

solve [ auto

| fail 2 "Could not solve by inversion nor auto" ].

refine (fun n =>

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end); invert_or_auto.

(* Proof Completed. *)

Defined.

match n with

| O => fun _ => Sig_no

| S pn => fun _ => Sig_yes pn

end); invert_or_auto.

(* Proof Completed. *)

Defined.

Now the funny part: the function

`pred_strong`takes as input an implicit natural number*n*and a “proof that*n > 0*”:
Theorem two_gt_0 : 2 > 0.

auto.

Qed.

Eval compute in pred_strong two_gt_0.

auto.

Qed.

Eval compute in pred_strong two_gt_0.

= Sig_yes 1 : {m : nat | 2 = S m}Anyway, in OCaml, it still looks pretty

*normal*:
Extraction pred_strong.

The eager reader can continue with CPDT's Subset chapter to see more implementations of “(** val pred_strong : nat -> nat **) let pred_strong = function | O -> assert false (* absurd case *) | S pn -> pn

`pred`” with other rich dependent types.##### A `List.map`

Here is an implementation of We use Coq's basic lists and we describe what the map function should do with an inductive proposition.

`List.map`with a`sig`return type specifying what the result actually*is*.
Section List_map.

Require Import List.

`map_spec`links the input list, the input function and the resulting function.
Inductive map_spec (A B: Set):

(A -> B) -> (list A) -> (list B) -> Prop :=

| ms_empty: forall f, map_spec f nil nil

| ms_step: forall f a la b lb,

(b = f a) -> map_spec f la lb ->

map_spec f (a :: la) (b :: lb).

(A -> B) -> (list A) -> (list B) -> Prop :=

| ms_empty: forall f, map_spec f nil nil

| ms_step: forall f a la b lb,

(b = f a) -> map_spec f la lb ->

map_spec f (a :: la) (b :: lb).

Here is the signature of the Simply because it is fun, we use the Without the notation and that's There we are stuck with a We can ask Coq to force it: And get the “ After a bit of googling-trial-and-error, we get a tactic to force the

`specified_map`:
Definition specified_map (A B: Set):

forall (f: A -> B) (l: list A),

{ lm : list B | map_spec f l lm }.

forall (f: A -> B) (l: list A),

{ lm : list B | map_spec f l lm }.

`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).
Proof with eauto using ms_empty, ms_step.

`Sig_take`, we simply do pattern matching with one case:
refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t =>

match fx f t with

| Sig_yes ll => Sig_yes (f h :: ll)

end

end)...

(* Proof Completed. *)

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t =>

match fx f t with

| Sig_yes ll => Sig_yes (f h :: ll)

end

end)...

(* Proof Completed. *)

*done*. But If we want to play with the notation, we introduce a tiny problem:
Restart.

refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end)...

refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end)...

`(let (ex, _) := fx f t in ex)`in the middle of the goal which`auto`does not want to expand any more …
Restart.

refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end);

try (destruct (fx f t))...

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end);

try (destruct (fx f t))...

`Proof Completed`” but we can still try to make something cleaner.
Restart.

`destruct`on our notation.
Ltac with_sig_take :=

repeat

match goal with

| [ |- context[ match ?E with Sig_yes x => _ end ] ] =>

idtac "Destructing" E; destruct E

end.

refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end);

with_sig_take...

(* Proof Completed. *)

Defined.

End List_map.

repeat

match goal with

| [ |- context[ match ?E with Sig_yes x => _ end ] ] =>

idtac "Destructing" E; destruct E

end.

refine (fix fx (f: A -> B) (l: list A):

{ lm : list B | map_spec f l lm } :=

match l with

| nil => Sig_yes nil

| cons h t => Sig_yes (f h :: (Sig_take fx f t))

end);

with_sig_take...

(* Proof Completed. *)

Defined.

End List_map.

Let's do some tests …

Eval compute in

(specified_map (fun x => x + 42) (0 :: 1 :: 2 :: 4 :: nil)).

(specified_map (fun x => x + 42) (0 :: 1 :: 2 :: 4 :: nil)).

= 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:
Inductive strictly_positive : Set :=

| gt_0: forall n : nat, (n > 0) -> strictly_positive.

Lemma one_gt_0: 1 > 0. auto. Qed.

Lemma three_gt_0: 3 > 0. auto. Qed.

Eval compute in

(specified_map

(fun t =>

match t with

| gt_0 x x_gt_0 => Sig_take pred_strong x_gt_0

end)

((gt_0 one_gt_0) :: (gt_0 two_gt_0) ::

(gt_0 three_gt_0) :: nil)).

| gt_0: forall n : nat, (n > 0) -> strictly_positive.

Lemma one_gt_0: 1 > 0. auto. Qed.

Lemma three_gt_0: 3 > 0. auto. Qed.

Eval compute in

(specified_map

(fun t =>

match t with

| gt_0 x x_gt_0 => Sig_take pred_strong x_gt_0

end)

((gt_0 one_gt_0) :: (gt_0 two_gt_0) ::

(gt_0 three_gt_0) :: nil)).

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

Recursive Extraction specified_map.

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

### Conclusion

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

`sumbool`type.# Sebastien Mondet

**Menu:**

Site generated thanks to bracetax, camlmix, sebib, and more …

Updated on Sat, 10 Dec 2011 12:46:34 -0500.

Sebastien Mondet

Updated on Sat, 10 Dec 2011 12:46:34 -0500.

Sebastien Mondet