From b4466fdb4e667c88330321e372bd6f93ee9c3513 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Sat, 10 Oct 2020 11:13:59 +0200 Subject: Create a summary page for the strongly-specified functions series --- site/posts/StronglySpecifiedFunctions.org | 17 ++ site/posts/StronglySpecifiedFunctions.v | 390 ------------------------- site/posts/StronglySpecifiedFunctionsProgram.v | 2 +- site/posts/StronglySpecifiedFunctionsRefine.v | 390 +++++++++++++++++++++++++ 4 files changed, 408 insertions(+), 391 deletions(-) create mode 100644 site/posts/StronglySpecifiedFunctions.org delete mode 100644 site/posts/StronglySpecifiedFunctions.v create mode 100644 site/posts/StronglySpecifiedFunctionsRefine.v (limited to 'site/posts') diff --git a/site/posts/StronglySpecifiedFunctions.org b/site/posts/StronglySpecifiedFunctions.org new file mode 100644 index 0000000..9bd488d --- /dev/null +++ b/site/posts/StronglySpecifiedFunctions.org @@ -0,0 +1,17 @@ +#+OPTIONS: toc:nil num:nil + +#+BEGIN_EXPORT html +

A Series on Strongly-Specified Functions in Coq

+#+END_EXPORT + +Using dependent types and the ~Prop~ sort, it becomes possible to specify +functions whose arguments and results are constrained by properties. Using such +a “strongly-specified” function requires to provide a proof that the supplied +arguments satisfy the expected properties, and allows for soundly assuming the +results are correct too. However, implementing dependently-typed functions can +be challenging. In this series, we explore several approaches available to Coq +developers. + +- [[./StronglySpecifiedFunctionsRefine.html][Using the ~refine~ Tactics]] :: + +- [[./StronglySpecifiedFunctionsProgram.html][Using the ~Program~ Framework]] :: diff --git a/site/posts/StronglySpecifiedFunctions.v b/site/posts/StronglySpecifiedFunctions.v deleted file mode 100644 index 5d0e69a..0000000 --- a/site/posts/StronglySpecifiedFunctions.v +++ /dev/null @@ -1,390 +0,0 @@ -(** * Strongly-Specified Functions in Coq, part 1: using the <> Tactic *) - -(** This is the first article (initially published on #January 11, 2015#) of a series of two on - how to write strongly-specified functions in Coq. You can read the next part - #here#. - - 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. - - #
# - - #
site/posts/StronglySpecifiedFunctions.v
# *) - -(** ** Is this list empty? *) - -(** Since we will manipulate lists in this article, we first - enable several notations of the standard library. *) - -From Coq Require Import List. -Import ListNotations. - -(** 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 <> 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 <> *) - -(** 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 <> *) - -(** 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 <>, Coq has created the <> and - <> 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 - <>. *) - -(** ** 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 <> framework distributed with the Coq - standard library helps, but it is better to understand what <> achieves - under its hood, which is basically what we have done in this article. *) diff --git a/site/posts/StronglySpecifiedFunctionsProgram.v b/site/posts/StronglySpecifiedFunctionsProgram.v index f7f84df..8ffb70c 100644 --- a/site/posts/StronglySpecifiedFunctionsProgram.v +++ b/site/posts/StronglySpecifiedFunctionsProgram.v @@ -3,7 +3,7 @@ This is the second article (initially published on #January 01, 2017#) of a series of two on how to write strongly-specified functions in Coq. You can read the previous part - #here#. # *) + #here#. # *) (** #
# diff --git a/site/posts/StronglySpecifiedFunctionsRefine.v b/site/posts/StronglySpecifiedFunctionsRefine.v new file mode 100644 index 0000000..d9bb3aa --- /dev/null +++ b/site/posts/StronglySpecifiedFunctionsRefine.v @@ -0,0 +1,390 @@ +(** * Strongly-Specified Functions in Coq, part 1: using the <> Tactic *) + +(** This is the first article (initially published on #January 11, 2015#) of a series of two on + how to write strongly-specified functions in Coq. You can read the next part + #here#. + + 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. + + #
# + + #
site/posts/StronglySpecifiedFunctionsRefine.v
# *) + +(** ** Is this list empty? *) + +(** Since we will manipulate lists in this article, we first + enable several notations of the standard library. *) + +From Coq Require Import List. +Import ListNotations. + +(** 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 <> 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 <> *) + +(** 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 <> *) + +(** 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 <>, Coq has created the <> and + <> 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 + <>. *) + +(** ** 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 <> framework distributed with the Coq + standard library helps, but it is better to understand what <> achieves + under its hood, which is basically what we have done in this article. *) -- cgit v1.2.3