**diff options**

author | Thomas Letan <lthms@soap.coffee> | 2020-02-04 18:13:38 +0100 |
---|---|---|

committer | Thomas Letan <lthms@soap.coffee> | 2020-02-04 18:13:38 +0100 |

commit | 9754a53fdc14f6ee4cf00f851cda68d69889bdcd (patch) | |

tree | 0af2ae9e1488f22b56e92cb6b17bb82e2f919bd3 /site/posts/StronglySpecifiedFunctions.v |

Initial commit with previous content and a minimal theme

Diffstat (limited to 'site/posts/StronglySpecifiedFunctions.v')

-rw-r--r-- | site/posts/StronglySpecifiedFunctions.v | 375 |

1 files changed, 375 insertions, 0 deletions

diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v new file mode 100644 index 0000000..f1d7cb7 --- /dev/null +++ b/site/posts/StronglySpecifiedFunctions.v @@ -0,0 +1,375 @@ +(** # +<h1>Strongly-Specified Functions in Coq with the <code>refine</code> Tactic</h1> +<time datetime="2015-07-11">2015-07-11</time> + # *) + +(** I started to play with Coq, the interactive theorem prover + developed by Inria, a few weeks ago. It is a very powerful tool, + yet hard to master. Fortunately, there are some very good readings + if you want to learn (I recommend the Coq'Art). This article is + not one of them. + + In this article, we will see how to implement strongly-specified + list manipulation functions in Coq. Strong specifications are used + to ensure some properties on functions' arguments and return + value. It makes Coq type system very expressive. Thus, it is + possible to specify in the type of the function [pop] that the + return value is the list passed in argument in which the first + element has been removed for example. + + But since we will manipulate lists in this article, we first + enable several notations of the standard library. *) + +From Coq Require Import List. +Import ListNotations. + +(** #<div id="generate-toc"></div># *) + +(** ** Is this list empty? *) + +(** It's the first question to deal with when manipulating + lists. There are some functions that require their arguments not + to be empty. It's the case for the [pop] function, for instance: + it is not possible to remove the first element of a list that does + not have any elements in the first place. + + When one wants to answer such a question as “Is this list empty?”, + he has to keep in mind that there are two ways to do it: by a + predicate or by a boolean function. Indeed, [Prop] and [bool] are + two different worlds that do not mix easily. One solution is to + write two definitions and to prove their equivalence. That is + [forall args, predicate args <-> bool_function args = true]. + + Another solution is to use the [sumbool] type as middleman. The + scheme is the following: + + - Defining [predicate : args → Prop] + - Defining [predicate_dec : args -> { predicate args } + { ~predicate args }] + - Defining [predicate_b]: + +<< +Definition predicate_b (args) := + if predicate_dec args then true else false. +>> *) + +(** *** Defining the <<empty>> predicate *) + +(** A list is empty if it is [[]] ([nil]). It's as simple as that! *) + +Definition empty {a} (l : list a) : Prop := l = []. + +(** *** Defining a decidable version of <<empty>> *) + +(** A decidable version of [empty] is a function which takes a list + [l] as its argument and returns either a proof that [l] is empty, + or a proof that [l] is not empty. This is encoded in the Coq + standard library with the [sumbool] type, and is written as + follows: [{ empty l } + { ~ empty l }]. *) + + Definition empty_dec {a} (l : list a) : { empty l } + { ~ empty l }. + + Proof. + refine (match l with + | [] => left _ _ + | _ => right _ _ + end); + unfold empty; trivial. + unfold not; intro H; discriminate H. + Defined. + +(** In this example, I decided to use the [refine] tactic which is + convenient when we manipulate the [Set] and [Prop] sorts at the + same time. *) + +(** *** Defining <<empty_b>> *) + +(** With [empty_dec], we can define [empty_b]. *) + + Definition empty_b {a} (l : list a) : bool := + if empty_dec l then true else false. + +(** Let's try to extract [empty_b]: + +<< +type bool = +| True +| False + +type sumbool = +| Left +| Right + +type 'a list = +| Nil +| Cons of 'a * 'a list + +(** val empty_dec : 'a1 list -> sumbool **) + +let empty_dec = function +| Nil -> Left +| Cons (a, l0) -> Right + +(** val empty_b : 'a1 list -> bool **) + +let empty_b l = + match empty_dec l with + | Left -> True + | Right -> False +>> + + In addition to <<list 'a>>, Coq has created the <<sumbool>> and + <<bool>> types and [empty_b] is basically a translation from the + former to the latter. We could have stopped with [empty_dec], but + [Left] and [Right] are less readable that [True] and [False]. Note + that it is possible to configure the Extraction mechanism to use + primitive OCaml types instead, but this is out of the scope of + this article. *) + +(** ** Defining some utility functions *) + +(** *** Defining [pop] *) + +(** There are several ways to write a function that removes the first + element of a list. One is to return `nil` if the given list was + already empty: *) + +Definition pop {a} ( l :list a) := + match l with + | _ :: l => l + | [] => [] + end. + +(** But it's not really satisfying. A `pop` call over an empty list + should not be possible. It can be done by adding an argument to + `pop`: the proof that the list is not empty. *) + +(* begin hide *) +Reset pop. +(* end hide *) +Definition pop {a} (l : list a) (h : ~ empty l) : list a. + +(** There are, as usual when it comes to lists, two cases to + consider. + + - [l = x :: rst], and therefore [pop (x :: rst) h] is [rst] + - [l = []], which is not possible since we know [l] is not empty. + + The challenge is to convince Coq that our reasoning is + correct. There are, again, several approaches to achieve that. We + can, for instance, use the [refine] tactic again, but this time we + need to know a small trick to succeed as using a “regular” [match] + will not work. + + From the following goal: + +<< + a : Type + l : list a + h : ~ empty l + ============================ + list a +>> *) + +(** Using the [refine] tactic naively, for instance this way: *) + + refine (match l with + | _ :: rst => rst + | [] => _ + end). + +(** leaves us the following goal to prove: + +<< + a : Type + l : list a + h : ~ empty l + ============================ + list a +>> + + Nothing has changed! Well, not exactly. See, [refine] has taken + our incomplete Gallina term, found a hole, done some + type-checking, found that the type of the missing piece of our + implementation is [list a] and therefore has generated a new + goal of this type. What [refine] has not done, however, is + remember that we are in the case where [l = []]! + + We need to generate a goal from a hole wherein this information is + available. It is possible using a long form of [match]. The + general approach is this: rather than returning a value of type + [list a], our match will return a function of type [l = ?l' -> + list a], where [?l] is value of [l] for a given case (that is, + either [x :: rst] or [[]]). Of course, As a consequence, the type + of the [match] in now a function which awaits a proof to return + the expected result. Fortunately, this proof is trivial: it is + [eq_refl]. *) + +(* begin hide *) + Undo. +(* end hide *) + refine (match l as l' return l = l' -> list a with + | _ :: rst => fun _ => rst + | [] => fun equ => _ + end eq_refl). + +(** For us to conclude the proof, this is way better. + +<< + a : Type + l : list a + h : ~ empty l + equ : l = [] + ============================ + list a +>> + + We conclude the proof, and therefore the definition of [pop]. *) + + rewrite equ in h. + exfalso. + now apply h. +Defined. + +(** It's better and yet it can still be improved. Indeed, according to its type, + [pop] returns “some list”. As a matter of fact, [pop] returns “the + same list without its first argument”. It is possible to write + such precise definition thanks to sigma-types, defined as: + +<< +Inductive sig (A : Type) (P : A -> Prop) : Type := + exist : forall (x : A), P x -> sig P. +>> + + Rather that [sig A p], sigma-types can be written using the + notation [{ a | P }]. They express subsets, and can be used to constraint + arguments and results of functions. + + We finally propose a strongly-specified definition of [pop]. *) + +(* begin hide *) +Reset pop. +(* end hide *) +Definition pop {a} (l : list a | ~ empty l) : { l' | exists a, proj1_sig l = cons a l' }. + +(** If you think the previous use of [match] term was ugly, brace yourselves. *) + + refine (match proj1_sig l as l' + return proj1_sig l = l' -> { l' | exists a, proj1_sig l = cons a l' } with + | [] => fun equ => _ + | (_ :: rst) => fun equ => exist _ rst _ + end eq_refl). + +(** This leaves us two goals to tackle. + + First, we need to discard the case where [l] is the empty list. + +<< + a : Type + l : {l : list a | ~ empty l} + equ : proj1_sig l = [] + ============================ + {l' : list a | exists a0 : a, proj1_sig l = a0 :: l'} +>> *) + + + destruct l as [l nempty]; cbn in *. + rewrite equ in nempty. + exfalso. + now apply nempty. + +(** Then, we need to prove that the result we provide ([rst]) when the + list is not empty is correct with respect to the specification of + [pop]. + +<< + a : Type + l : {l : list a | ~ empty l} + a0 : a + rst : list a + equ : proj1_sig l = a0 :: rst + ============================ + exists a1 : a, proj1_sig l = a1 :: rst +>> *) + + + destruct l as [l nempty]; cbn in *. + rewrite equ. + now exists a0. +Defined. + +(** Let's have a look at the extracted code: + +<< +(** val pop : 'a1 list -> 'a1 list **) + +let pop = function +| Nil -> assert false (* absurd case *) +| Cons (a, l0) -> l0 +>> + + If one tries to call [pop nil], the [assert] ensures the call fails. Extra + information given by the sigma-type have been stripped away. It can be + confusing, and in practice it means that, we you rely on the extraction + mechanism to provide a certified OCaml module, you _cannot expose + strongly-specified functions in its public interface_ because nothing in the + OCaml type system will prevent a miseuse which will in practice leads to an + <<assert false>>. *) + +(** ** Defining [push] *) + +(** It is possible to specify [push] the same way [pop] has been. The only + difference is [push] accepts lists with no restriction at all. Thus, its + definition is a simpler, and we can write it without [refine]. *) + +Definition push {a} (l : list a) (x : a) : { l' | l' = x :: l } := + exist _ (x :: l) eq_refl. + +(** And the extracted code is just as straightforward. + +<< +let push l a = + Cons (a, l) +>> *) + +(** ** Defining [head] *) + +(** Same as [pop] and [push], it is possible to add extra information in the + type of [head], namely the returned value of [head] is indeed the firt value + of [l]. *) + +Definition head {a} (l : list a | ~ empty l) : { x | exists r, proj1_sig l = x :: r }. + +(** It's not a surprise its definition is very close to [pop]. *) + + refine (match proj1_sig l as l' return proj1_sig l = l' -> _ with + | [] => fun equ => _ + | x :: _ => fun equ => exist _ x _ + end eq_refl). + +(** The proof are also very similar, and are left to read as an exercise for + passionate readers. *) + + + destruct l as [l falso]; cbn in *. + rewrite equ in falso. + exfalso. + now apply falso. + + exists l0. + now rewrite equ. +Defined. + +(** Finally, the extracted code is as straightforward as it can get. + +<< +let head = function +| Nil -> assert false (* absurd case *) +| Cons (a, l0) -> a +>> *) + +(** ** Conclusion & Moving Forward *) + +(** Writing strongly-specified functions allows for reasoning about the result + correctness while computing it. This can help in practice. However, writing + these functions with the [refine] tactic does not enable a very idiomatic + Coq code. + + To improve the situation, the <<Program>> framework distributed with the Coq + standard library helps, but it is better to understand what <<Program>> achieves + under its hood, which is basically what we have done in this article. *) |