Coq Programming with Subsets

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

About Learning Coq

To start learning Coq, I definitely recommend Software Foundations by Pierce et al.:
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: 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.).


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).
Set Implicit Arguments.
The type 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.
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:
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).


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:
Definition succ_strong: forall (n : nat), {m : nat | m = S n}.
  refine (fun n => Sig_yes (S n)). trivial.
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”:
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)).
The first underscore is inferred by Coq (not through 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)).
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:
Extraction succ_strong.
(** val succ_strong : nat -> nat **)
let succ_strong n =
  S n
A Non-Total Function
Let's see another example: 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
This time two goals remain to fill …
  (* n : nat    _H : 0 > 0  |-   False *)
  inversion _H.
  (*  n : nat   pn : nat    _H : S pn > 0 |-    S pn = S pn *)
  (* 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.).
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.
  refine (fun n =>
    match n with
      | O => fun _ => Sig_no
      | S pn => fun _ => Sig_yes pn
  [ match goal with H: 0 > 0 |- _ => inversion H end
    | auto ].
  (* Proof Completed. *)
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.).
  Ltac solve_by_inversion :=
    match goal with
      | H:_ |- _ =>
        solve [ inversion H | clear H; solve_by_inversion
          | fail 2 "Could not solve by inversion" ]
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" ].
With them, we can solve this even more elegantly:
  refine (fun n =>
    match n with
      | O => fun _ => Sig_no
      | S pn => fun _ => Sig_yes pn
    end); invert_or_auto.
  (* Proof Completed. *)
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.
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.
(** 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 with a sig return type specifying what the result actually is.
Section List_map.
We use Coq's basic lists
  Require Import List.
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.
  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).
Here is the signature of the specified_map:
  Definition specified_map (A B: Set):
    forall (f: A -> B) (l: list A),
      { lm : list B | map_spec f l lm }.
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).
  Proof with eauto using ms_empty, ms_step.
Without the notation 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)
    (* Proof Completed. *)
and that's done. But If we want to play with the notation, we introduce a tiny problem:
    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))
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:
    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))
    try (destruct (fx f t))...
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.
    Ltac with_sig_take :=
        match goal with
          | [ |- context[ match ?E with Sig_yes x => _ end ] ] =>
            idtac "Destructing" E; destruct E
    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))
    (* Proof Completed. *)

End List_map.
Let's do some tests …
Eval compute in
  (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
    (fun t =>
      match t with
        | gt_0 x x_gt_0 => Sig_take pred_strong x_gt_0
    ((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 |
    (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 =
  (* 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

Sebastien Mondet


Site generated thanks to bracetax, camlmix, sebib, and more …
Updated on Sat, 10 Dec 2011 12:46:34 -0500.
Sebastien Mondet

Powered by Caml