TP0: A First Step into
the Coq Proof Assistant
Aim of this self-taught first experiment with Coq
- first by executing some Coq code and observing the behaviour of the proof assistant and
- have you start writing your first definitions, theorems and proofs in Coq by adapting the code provided.
Installing Coq
Coq
is installed, you may opt for various ways interacting with the proof assistant (see below).
While using coqide
or jsCoq
do not require any additional installation, if you consider using emacs
with the proofgeneral
mode or VSCode
, you will find relevant information on their installation in the page linked below:
Getting Documentation about Coq
Launching Coq
- via
coqide
, a graphical interface based ongtk
- via
proofgeneral
, which is a plugin foremacs
- via VSCode
- directly in a browser via
jsCoq
, for instance https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html (see https://github.com/ejgallego/jscoq for usage instructions) - or perhaps via
coqtop
, a read-eval-print loop (repl) which is quite bare, similar to theocaml
interactive loop.
.v
as extension (for "vernacular"...).
coqide
and proofgeneral
and jsCoq
provide interfaces with a similar layout :
- the file being edited is in the left half of the screen,
- while proofs in progress are in right top and
- system messages are in right bottom (Coq answers, error messages, etc).
Today's program
TP0.v
file thanks to a tool called coqdoc
. You can go
back and forth between the two documents: reading will be smoother
in the html page while the .v
file can be played in coqide
, jscoq
,
or your prefered IDE, standing for integrated development environment.)
jscoq
if you
prefer using jscoq scratchpad for now.
You will notice immediately that Coq comments are written between :
everything that is between those signs will be ignored by Coq. It will
usually be presented in your IDE with a different font / color to make
it easier to distinguish from the actual code.
- Definition : binds some name with a (non-recursive) Coq term
- Fixpoint : same, for a recursive definition
- Inductive : creates a new inductive type and its constructors
- Check : displays the type of a Coq term
- Print : displays the body of a definition or the details of an inductive type
- Compute : reduces a term (i.e. determines its normal form) and prints it.
.
is mandatory to end each Coq phrase.
What is not in today's program
- introducing your to functional programming with Coq
- introducing your to the use of a proof assistant to
First Terms and (Data) Types
Coq
is that of type-checking.
bool
Check true.
Check false.
Check bool.
Print bool.
There is a construction if ... then ... else ...,
as well as some predefined boolean operations :
- negation : negb
- logical "and" : andb (syntax &&, after doing Open Scope bool_scope)
- logical "or" : orb (syntax ||, after doing Open Scope bool_scope)
Check negb.
Check andb.
Check orb.
Print negb.
Print andb.
Print orb.
Open Scope bool_scope.
Check (true && false).
We can also compute, or evaluate, such an expression, which should return a boolean value (this is different from checking its type, in the previous line, which did not involve computing the boolean value):
Compute (true && false).
Exercise 1 :
Write four distinct boolean expressions using negb, andb and orb, including one which uses the three functions at the same time. Check their type and compute their boolean value.
Once one has built an expression e of a given type t, one can define a
constant c to hold that expression as:
Definition c : t := e.
For instance:
Definition andtf : bool := (true && false).
The new constant can now be checked, printed or used to build new terms:
Check andtf.
Print andtf.
Compute andtf.
Definition n : bool := negb andtf.
Print n.
Compute n.
Note that computing the value of n does not modify n:
Print n.
Note that Coq does not always need that we give the type of an expression. It can often infer it:
Definition nbis := negb andtf.
Print nbis.
Note that we cannot check the type of the notation && (Fail is a command that succeed when the body fails, we will come back to this).
Fail Check "&&".
... but we can print its definition:
Print "&&".
On the other hand, && is defined as an infixed notation for andb, that is, for any boolean expression x and y, x && y is a notation for andb x y. In particular, we can check the type of the function which, to booleans x and y, associates x && y:
Check (fun x y => x && y).
Compare with the expression below:
Check (fun x => fun y => x && y).
Since we can typecheck functions, we can also typecheck expressions involving such functions, which is different from evaluating them:
Check (fun x y => (negb x) || y).
Now that we have written a function, we can give it a name by using
Definition:
Definition impb := fun x y => (negb x) || y.
Check impb.
Print impb.
We will discuss type-checking in more details in forthcoming lectures, but you should already notice that type-checking and evaluation are very different questions. (Even though the type theory of Coq is so powerful that they must be connected.) The following illustrates this fact:
Parameter b: bool.
Check (if b then false else true).
Compute (if b then false else true).
Compute (if true then false else true).
Compute (if false then false else true).
Beware, unlike usual programming languages, the evaluation of && and || is not necessarily *lazy* in Coq. We can actually specify the type of evaluation strategy in variants of Compute to be studied later in the semester.
Coq provides a type nat for natural numbers. By default, typing 0, 1 and any other positive numeric constant gives you a nat. Beware : this is a "unary" encoding (Peano numerals), hence dramatically slow.
In order to get access to operations on natural numbers,
we load the Arith library (for more informations on the standard library, visit the corresponding section of the reference manual):
nat
Require Import Arith.
Check 0.
Check 1.
Check 42.
nat corresponds to natural numbers considered Peano's natural arithmetic, built from a constant O (the upper-case letter 'o') and a function symbol S for the successor. The use of the usual notation for natural number is a pretty-printing feature:
Check O.
Check S O.
The constructor S can itself be typed as:
Check S.
Some operations defined on nat:
We will see later how to perform efficient arithmetical operations (binary encoding) and how to handle negative numbers (type Z).
- addition +,
- multiplication *,
- euclidean division /,
- modulo x mod y.
- boolean comparisons of numbers : x =? y or x <? y or x <=? y.
Exercise 3:
Define the function succ_add of two arguments which returns the successor of the sum of its two input
Let us know turn our attention to the types and definitions of those operations.
Try the following command:
Print "+".
One sees that when asked to print the definition of *,
Coq refers to Init.Nat.add. Let's investigate:
Check Init.Nat.add.
Print Init.Nat.add.
Here, we can remark three things:
To see the impact of fix, let us try to define add without fix:
- the type of Init.Nat.add is nat -> nat -> nat which is to be read nat -> (nat -> nat), that is the type of a function that receives a natural as input and returns a function from nat to <nat as output.
- the definition of Init.Nat.add makes use of a new construction: fix (to define a function recursively) with the {struct n} to indicates that their is an argument, n, that structurally decreases at each recursive call, ensuring that any series of recursive calls will terminate. In fact we will see simpler means to define recursive functions in the following lectures, using the keyword Fixpoint.
- and the use of match ... with | 0 => ... | S n => ... end which allows to define the function to be define by case analysis (actually pattern-matching) on its first argument.
Fail Definition addfail (n m : nat) : nat :=
match n with
| 0 => m
| S p => S (addfail p m)
end.
In the message
addfail refers to the occurrence of addfail
in the body of the function definition:
Definition addfail (n m : nat) : nat :=
match n with
| 0 => m
| S p => S **addfail** p m
end.
With using fix or Fixpoint, a function being defined cannot
refer to itself.
The reference addfail was not found in the current environment.
Definition addfail (n m : nat) : nat :=
match n with
| 0 => m
| S p => S **addfail** p m
end.
Exercise 4:
Do the same thing as we did for + with *.Some observations about recursive functions and inductive types
Fixpoint power2 (n:nat) : nat :=
match n with
| 0 => 1
| S m => 2 * (power2 m)
end.
Check power2.
Compute power2 8.
Exercise 6:
Define the function fact : nat -> nat which computes the factorial by adapting the above examples.
To finish, let us have a look at how the type nat is defined:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
- create two new constructors (constants): O and S, that allow to build terms of type nat: O, S O, S (S O), S (S (S O)), etc.
- create a new type nat the elements of which are obtains by using the constructors as specified in the inductive type definition.
- notably ensuring that the constructors are injective (here, S t = S u => t = u for any t and u of type nat) and that two terms starting with different constructors are never equal (S t <> O).
- and last but not least, generating induction principles for type nat.
- nat is defined
- nat_rect is defined
- nat_ind is defined
- nat_rec is defined
- nat_sind is defined
Print nat.
Check nat_ind.
If you wish, you can print nat_ind and try to make sense of it.
But notice that it is not until few weeks that we will consider this.
Exercise 7:
Define the function pred : nat -> nat which, when given O returns O and when given some successor number (S n) returns its predecessor, that is n.Exercise 8:
Define the function even : nat -> bool which returns true if its input is even and false if it is odd.A first theorem
Theorem predsucc : forall n: nat, pred (S n) = n.
Proof.
intro n. simpl. reflexivity.
Qed.
Theorem is a slight variant of a Definition. (The difference
will be analyzed in the second part of the semester.)
It simply declares a constant predsucc of type
forall n: nat, pred (S n) = n. (that means that there are
still plenty of other type constructions to discover!)
and instead of providing a term of that type, it enters
the interactive mode, aiming and building a proof (or a term).
This interactive mode is shown on the top right of the
screen, showing the goal that must be proved:
_____________________________________(1/1)
forall n : nat, pred (S n) = n
Here the proof is simply by computation:
_____________________________________(1/1)
forall n : nat, pred (S n) = n
- it first introduces n in the context, assuming a generic nat n (as when we declare "let n be a natural number")
- it then uses a proof tactic simpl, which reduces pred (S n) to n and
- finishes the proof by reflexivity, noting that in the left and right hand side of the equality there are identical terms.
This page has been generated by coqdoc