Gentle introduction to Coq: the beginning

Foreword

It's no secret that mistakes in programs can lead to sad consequences. History knows many cases where overflowing a counter or an unhandled exception resulted in high material costs and human losses. For example, on June 4, 1996, the European launch vehicle Ariane 5 literally fell apart on the 39th second of flight. An analysis of the incident revealed that the accident was due to a software error. The damage amounted to about $ 7 billion. In February 1991, the Patriot missile missed the target due to a rounding error, managed to fly an extra 500 meters. Damage: 28 dead and more than a hundred wounded. This kind of errors are found in the hardware. A recent bug in Pentium processors, due to the wrong division of floating-point numbers, forced Intel to replace the defective chips. This mistake cost the company $ 475 million.

When designing hardware or software with increased reliability requirements, formal verification is widely used - a formal proof of the conformity of the subject of verification to its formal description. The subject here can be algorithms, digital circuits, HDL hardware descriptions, etc.

The formal verification procedure is quite a long and routine exercise. Therefore, it is not justified in all cases. Ordinary testing is also suitable for everyday applications. Here we must understand that testing can not prove the absence of errors in the program and its compliance with the formal description.

Of course, not all statements can be proved automatically. In such cases, proof checking systems (proof checker, proof assistant) come to the rescue, one of which is Coq.
')

Introduction

Coq is an interactive shell for proving theorems that uses its own functional programming language with dependent types - Gallina. It was invented and implemented by the staff of the French Institute INRIA in the mid-80s. Coq is currently available for GNU / Linux, Windows and MacOS. Source codes are distributed under the terms of the license LGPL v.2.

There are several ways to work with Coq: in the console in interactive mode, in graphic mode in CoqIDE or in Emacs using the Proof General plugin.



So, Coq is installed and ready to go. Let's try to write something!

There are no built-in batteries in the Coq language - neither logical values ​​nor numbers (in fact, there is a standard library with many useful definitions and lemmas, but for academic purposes, we assume that there is nothing like this). Instead, Coq provides powerful tools for defining new data types and functions that operate and transform these types. Consider a specific example:

 Inductive day: Type: =
   |  monday: day
   |  tuesday: day
   |  wednesday: day
   |  thursday: day
   |  friday: day
   |  saturday: day
   |  sunday: day.

With this declaration, we tell Coq that we want to define a new set of data values ​​— a type. This type is named day , and the values ​​of this type are monday , tuesday and so on. Now we can write a function over day values. We write a function that calculates the next working day:

 Definition next_weekday (d: day): day: =
   match d with
   |  monday => tuesday
   |  tuesday => wednesday
   |  wednesday => thursday
   |  thursday => friday
   |  friday => monday
   |  saturday => monday
   |  sunday => monday
   end.

In Coq, there is type inference, pattern matching, and other things inherent in functional programming languages.

Once we have defined the function, it's time to test its performance with a few examples. First, we can use the Eval simpl :

 Eval simpl in (next_weekday friday).
    (* ==> monday: day *)
 Eval simpl in (next_weekday (next_weekday saturday)).
    (* ==> tuesday: day *)

Secondly, we can explicitly specify the expected result and instruct Coq to check it:

 Example test_next_weekday:
   (next_weekday (next_weekday saturday)) = tuesday.
 Proof.  simpl.  reflexivity.  Qed.

When working in CoqIDE, it is convenient to use step-by-step program execution to see intermediate results:


The third way is to extract the definition into some programming language (OCaml, Scheme or Haskell). This is one of the main features of the Coq system, for which everything was developed:

 Extraction Language Ocaml.
 Extraction "/tmp/day.ml" next_weekday.

Here is the result of the extraction of our function in OCaml:

 type day =
 |  Monday
 |  Tuesday
 |  Wednesday
 |  Thursday
 |  Friday
 |  Saturday
 |  Sunday

 (** val next_weekday: day -> day **)

 let next_weekday = function
 |  Monday -> Tuesday
 |  Tuesday -> Wednesday
 |  Wednesday -> Thursday
 |  Thursday -> Friday
 |  _ -> Monday

Conclusion

In the following sections, we will look at ways to define recursive functions and work with the main tactics of evidence.

Recommended reading:

1. Software foundations
2. Certified Programming with Dependent Types

The next part .