From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(**
----------------------------------------------------------
##
----------------------------------------------------------
##
** Lesson 1: summary
- functions
- simple data
- containers
- symbolic computations
- higher order functions and mathematical notations
#
#
----------------------------------------------------------
##
** Functions
Functions are built using the [fun .. => ..] syntax.
The command [Check] verifies that a term is well typed.
#
#
*)
Check (fun n => 1 + n + 1).
(**
#
#
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).
#
#
*)
Check 2.
Check (fun n => 1 + n + 1) 2.
(**
#
#
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.
#
#
*)
Definition f := (fun n => 1 + n + 1).
(* Definition f n := 1 + n + 1. *)
(* Definition f (n : nat) := 1 + n + 1. *)
(**
#
#
Named terms can be printed.
#
#
*)
Print f.
(**
#
#
Coq is able to compute with terms, in particular
one can obtain the normal form via the [Eval lazy in]
command.
#
#
*)
Eval lazy in f 2.
(**
#
#
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).
#
#
*)
Eval lazy delta [f] in f 2.
Eval lazy delta [f] beta in f 2.
(**
#
#
Nothing but functions (and their types) are built-in in Coq.
All the rest is defined, even [1], [2] and [+] are not primitive.
#
#
#
#
#
#
** Data types
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.]
#
#
*)
Print bool.
(**
#
#
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.
#
#
*)
Definition twoVtree (b : bool) := if b then 2 else 3.
Eval lazy in twoVtree true.
Eval lazy delta in twoVtree true.
Eval lazy delta beta in twoVtree true.
Eval lazy delta beta iota in twoVtree true.
(**
#
#
We define a few boolean operators that will come in handy
later on.
#
#
*)
Definition andb (b1 b2 : bool) := if b1 then b2 else false.
Definition orb (b1 b2 : bool) := if b1 then true else b2.
Infix "&&" := andb.
Infix "||" := orb.
Check true && false || false.
(**
#
#
The [Infix] command lets one declare infix notations.
Precedence 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).]
#
#
*)
Print 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].
#
#
*)
Check 3.
Check (fun x => (x + x).+2).
Eval lazy in (fun x => (x + x).+2) 1.
(**
#
#
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.
#
#
*)
Definition pred (n : nat) :=
if n is p.+1 then p else 0.
Eval lazy in pred 7.
(**
#
#
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
#
#
*)
Fixpoint addn n m :=
if n is p.+1 then (addn p m).+1 else m.
Infix "+" := addn.
Eval lazy in 3 + 2.
(**
#
#
The [if..then..else..] syntax is just sugar for
[match..with..end].
#
#
*)
Print addn.
(**
#
#
Let's now write the equality test for natural numbers
#
#
*)
Fixpoint eqn n m :=
match n, m with
| 0, 0 => true
| p.+1, q.+1 => eqn p q
| _, _ => false
end.
Infix "==" := eqn.
Eval lazy in 3 == 4.
(**
#
#
Other examples are subtraction and order
#
#
*)
Fixpoint subn m n : nat :=
match m, n with
| p.+1, q.+1 => subn p q
| _ , _ => m
end.
Infix "-" := subn.
Eval lazy in 3 - 2.
Eval lazy in 2 - 3. (* truncated *)
Definition leq m n := m - n == 0.
Infix "<=" := leq.
Eval lazy in 4 <= 5.
(**
#
#
#
#
#
(notes)
#
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
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).]
#
#
*)
Check nil.
Check cons 3 [::].
(**
#
#
We learn that [[::]] is a notation for the empty sequence
and that the type parameter [?A] is implicit.
#
#
*)
Check 1 :: nil.
Check [:: 3; 4; 5 ].
(**
#
#
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
#
#
*)
Check [:: 3; 4; 5 ].
Check [:: true; false; true ].
(**
#
#
Let's now define the [size] function.
#
#
*)
Fixpoint size A (s : seq A) :=
if s is _ :: tl then (size tl).+1 else 0.
Eval lazy in size [:: 1; 8; 34].
(**
#
#
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.
]]
#
#
*)
Definition l := [:: 1; 2; 3].
Eval lazy in [seq x.+1 | x <- l].
(**
#
#
The #
seq#
library of Mathematical Components contains many combinators. Their syntax
is documented in the header of the file.
#
#
#
#
#
#
** Symbols
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.
#
#
*)
Section symbols.
Variables v : nat.
Eval lazy in pred v.+1 .
Eval lazy in pred v .
(**
#
#
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.
#
#
*)
Fixpoint foldr A T f (a : A) (s : seq T) :=
if s is x :: xs then f x (foldr f a xs) else a.
(**
#
#
The best way to understand what [foldr] does
is to postulate a variable [f] and compute.
#
#
*)
Variable f : nat -> nat -> nat.
Eval lazy in foldr f 3 [:: 1; 2 ].
(**
#
#
If we plug [addn] in place of [f] we
obtain a term that evaluates to a number.
#
#
*)
Eval lazy in foldr addn 3 [:: 1; 2 ].
End symbols.
(**
#
#
#
#
#
#
** Higher order functions and mathematical notations
Let's try to write this formula in Coq
#$$ \sum_{i=1}^n (i * 2 - 1) = n ^ 2 $$#
We need a bit of infrastruture
#
#
*)
Fixpoint iota m n := if n is u.+1 then m :: iota m.+1 u else [::].
Eval lazy in iota 0 5.
(**
#
#
Combining [iota] and [foldr] we can get pretty
close to the LaTeX source for the formula above.
#
#
*)
Notation "\sum_ ( m <= i < n ) F" :=
(foldr (fun i a => F + a) 0 (iota m (n-m))).
Check \sum_(1 <= x < 5) (x * 2 - 1).
Eval lazy in \sum_(1 <= x < 5) (x * 2 - 1).
(**
#
#
#
#
#
#
#
#
** Lesson 1: sum up
- [fun .. => ..]
- [Check]
- [Definition]
- [Print]
- [Eval lazy]
- [Inductive] declarations [bool], [nat], [seq].
- [match .. with .. end] and [if .. is .. then .. else ..]
- [Fixpoint]
- [andb] [orb] [eqn] [leq] [addn] [subn] [size] [foldr]
#
#
*)