Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.
Functions are written using the fun .. => .. syntax. Down below we write the function:
$$ n \mapsto 1 + n $$
The command Check verifies that a term is well typed. The precise meaning will be given tomorrow morning, for now think about it as a well formed element of some set.
Coq answers by annotating the term with its type (the -> denotes the function space):
$$ \mathbb{N} \to \mathbb{N} $$
Function application is written by writing the function on the left of the argument (eg, not as in the mathematical practice).
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 of this type are built. Only true and false are *canonical* inhabitants of bool and they are called *constructors*.
Remark: a data type declaration prescribes the shape of values, not which operations are available nor their properties. We are going to use programs (functions) to describe the operations on a data type.
Coq provides one very primitive operation that works on data types. This operation lets you take a decision based on the canonical shape of the data. It is written match x with true => ... | false => .. end.
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).
Remark that the declaration is recursive.
Remark:
Coq provides a special notation for literals, eg 3, that is just sugar for S (S (S O)).
Now let's define a simple operation on natural numbers.
As for booleans, Coq provides a primitie operation to make decisions based on the canonical values.
Remark that p is a binder. When the match..with..end is evaluated, and n put in normal form, then if it is S t the variable p takes t and the second is taken.
Since the data type of natural number is recursive Coq provides another primitive operation called Fixpoint.
Let's now write the equality test for natural numbers
Other examples are subtraction and order
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 list (A : Type) := nil | cons (hd : A) (tl : list A).
The notation [:: .. ; .. ] can be used to form list by separating the elements with ;. When there are no elements what is left is [::] that is the empty list.
And of course we can use list 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 : list A) : list B := match s with cons e tl => cons (f e) map f tl | nil => nil end.
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 variable 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 infrastructure
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
Most of the statements that we consider in Mathematical Components are equalities.
It is not surprising one can equate two numbers.
Remark: to save space, variables of the same type can be writte (a b c : type) instead of (a : type) (b : type) ....
We have defined many boolean tests that can play the role of predicates.
More statements using equality and predicates in bool
Remark: in the first statement = really means
if and only if
.
Remark: Coq adds = true automatically when we state a lemma.
Our statements are made of programs. Hence they compute!
The by[] proof command solves trivial goals (mostly) by computation.
Fixpoint addn n m := match n with 0 => m | S p => S (addn p m) end.
Fixpoint subn m n : nat := match m, n with | S p, S q => subn p q | _ , _ => m end.
Fixpoint eqn (n : nat) (m : nat) : bool := match n, m with | 0, 0 => true | S p, S q => eqn p q | _, _ => false end.
Definition leq m n := m - n == 0.
Let's look around.
Locate looks for a symbol to find the name behing id.
It is not always the case the computation solves all our problems. In particular here there are no constructors to consume, hence computation is stuck.
To prove negbK we need a case split.
The proof of negbK requires a case analysis: given that b is of type bool, it can only be true or false.
The case: term command performs this proof step.
The constructors of bool have no arguments, but for example the second constructor of nat has one.
In this case one has to complement the command by supplying names for these arguments.
Sometimes case analysis is not enough.
Fixpoint muln (m n : nat) : nat := match m with 0 => 0 | S p => n + muln p n end.
We don't know how to prove this yet. But maybe someone proved it already...
The Search command is quite primitive but also your best friend.
It takes a head pattern, the whildcard _ in the examples above, followed by term or patterns.
You must always use in MC in order to limit the search space to the set of lemmas relevant to these lectures.
The rewrite tactic uses an equation. If offers many more flags than the ones we will see (hint: check the Coq user manual, SSReflect chapter).
Let's now look at another example to learn more about rewrite.