To play this document inside your browser use ALT-N and ALT-P.
You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.
Objective: learn the Coq system in the MC library
Functions are built using the fun .. => .. syntax. The command Check verifies that a term is well typed.
Notice that the type of n was inferred and that the whole term has type nat -> nat, where -> is the function space.
Function application is written by writing the function on the left of the argument (eg, not as in the mathematical practice).
Notice how 2 has a type that fits, and hence the type of the function applied to 2 is nat.
Terms (hence functions) can be given a name using the Definition command. The command offers some syntactic sugar for binding the function arguments.
Named terms can be printed.
Coq is able to compute with terms, in particular one can obtain the normal form via the Eval lazy in command.
Notice that computation
is made of many steps.
In particular f has to be unfolded (delta step)
and then the variable substituted for the argument
(beta).
Nothing but functions (and their types) are built-in in Coq. All the rest is defined, even 1, 2 and + are not primitive.
This slide corresponds to section 1.1 of the Mathematical Components book
Data types can be declared using the Inductive command.
Many of them are already available in the Coq library called Prelude that is automatically loaded. We hence just print them.
Inductive bool := true | false.
This command declares a new type bool and declares how the terms (in normal form) of this type are built. Only true and false are canonical inhabitants of bool.
To use a boolean value Coq provides the if..then..else.. syntax.
We define a few boolean operators that will come in handy later on.
The Infix command lets one declare infix notations. Precendence and associativity is already declared in the prelude of Coq, here we just associate the constants andb and orb to these notataions.
Natural numbers are defined similarly to booleans:
Inductive nat := O | S (n : nat).
Coq provides a special notation for literals, eg 3, that is just sugar for S (S (S O)).
The Mathematical Components library adds on top of that the postfix .+1, .+2, .. for iterated applications of S to terms other than O.
In order to use natural numbers Coq provides two tools. An extended if..then..else.. syntax to extract the argument of S and the Fixpoint command to define recusrsive functions.
Notice that p is a binder. When the if..then..else.. is evaluated, and n put in normal form, then if it is S t the variable p takes t and the then-branch is taken.
Now lets define addition using recursion
The if..then..else.. syntax is just sugar for match..with..end.
Let's now write the equality test for natural numbers
Other examples are subtraction and order
All the constants defined in this slide are already defined in Coq's prelude or in Mathematical Components. The main difference is that == is not specific to nat but overloaded (it works for most data types). This topic is to be developed in lesson 4.
This slide corresponds to section 1.2 of the Mathematical Components book
Containers let one aggregate data, for example to form a pair or a list. The interesting characteristic of containers is that they are polymorphic: the same container can be used to hold terms of many types.
Inductive seq (A : Type) := nil | cons (hd : A) (tl : seq A).
We learn that [::] is a notation for the empty sequence and that the type parameter ?A is implicit.
The infix :: notation stands for cons. This one is mostly used to pattern match a sequence.
The notation [:: .. ; .. ] can be used to form sequences by separating the elements with ;. When there are no elements what is left is [::] that is the empty seqeunce.
And of course we can use sequences with other data types
Let's now define the size function.
Given that the contents of containers are of an arbitrary type many common operations are parametrized by functions that are specific to the type of the contents.
Fixpoint map A B (f : A -> B) s := if s is e :: tl then f e :: map f tl else nil.
The seq library of Mathematical Components contains many combinators. Their syntax is documented in the header of the file.
This slide corresponds to section 1.3 of the Mathematical Components book
The section mecanism is used to describe a context under which definitions are made. Coq lets us not only define terms, but also compute with them in that context.
We use this mecanism to talk about symbolic computation.
Computation can take place in presence of variables as long as constructors can be consumed. When no more constructors are available computation is stuck.
Let's not look at a very common higher order function.
The best way to understand what foldr does is to postulate a virable f and compute.
If we plug addn in place of f we obtain a term that evaluates to a number.
This slide corresponds to sections 1.4 and 1.5 of the Mathematical Components book
Let's try to write this formula in Coq
$$ \sum_{i=1}^n (i * 2 - 1) = n ^ 2 $$
We need a bit of infrastruture
Combining iota and foldr we can get pretty close to the LaTeX source for the formula above.
This slide corresponds to section 1.6 of the Mathematical Components book