Commit db50fa0f authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

english version of seance1 and TD1

parent 67feca96
Initiation to Functional Programming in Coq
===========================================
**M2 LMFI**
## Launching Coq
There are several ways to use Coq:
* via `coqide`, a graphical interface based on `gtk`
* via `proofgeneral`, which is a plugin for `emacs`
* 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 the `ocaml` interactive loop.
Each method has its advocates (even the last one...).
The coq source files are always named with `.v` as extension (for "vernacular"...).
After launch, both `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).
In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.
Until January, we will mostly use the following commands:
* `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.
A dot `.` is mandatory to end each Coq phrase.
## Coq functional core
Coq directly derives from the lambda-calculus (due to Church in the 1930s) and its three basic constructions:
- variables
- function abstraction : `λx.t` (written `fun x => t` in Coq)
- function application : `t u` (same in Coq).
In other communities, the function application may be written `t(u)` (regular math style) or `(t)u` (Krivine style).
Here in Coq and many other functional languages we favor a light style, with parenthesis only in case of ambiguity : `f (x+1)` isn't `f x + 1` (which is rather `(f x) + 1`).
For instance `x y z` is a shortcut for `(x y) z` : one function `x` applied to two successive arguments `y`, then `z`.
And `x (y z)` is quite different : `y` will be a function receiving `z`, and the result is given to function `x`.
Important rule of thumb : in function applications, put parenthesis around every argument that isn't a variable or a constant.
Other important shortcut : `fun x y => t` is `fun x => fun y => t`. Actually, a binary function is a unary function returning a unary function !
## Typing
By default, lambda-calculus is said *raw* or *pure* or *untyped* : you can try applying anything to anything and look if it breaks.
Some untyped programming languages based on λ : Lisp or Scheme.
On the contrary, as most recent functional programming languages (e.g OCaml), Coq is *strongly typed* : the non-well-typed terms will be rejected in Coq during *type-checking*, before running any computation.
The main type constructor is the *functional arrow* `->`.
Note that `A->B->C` is `A->(B->C)`.
First, simply-typed lambda-calculus : just take lambda-calculus plus a typing judgement `Γ ⊢ t:T` described by the rules below. Here Γ is a *typing context*, i.e. a finite list of variables associated with their respective types.
- If `x:T` is in Γ then `Γ ⊢ x:T`
- If `Γ+x:τ ⊢ t:σ` then `Γ ⊢ (λx.t):(τ→σ)`
- If `Γ ⊢ t:(τ→σ)` and `Γ ⊢ u:τ` then `Γ ⊢ (t u) : σ`
Note that by forgetting all the terms in the previous rules and keeping only the types (and contexts being hence just list of types), we recover the logical rules of the minimal logic : the axiom rule and the implication intro/elim rules. That's the start of the Curry-Howard isomorphism (more on that in other courses).
Coq typing system (named CIC, for "Calculus of Inductive Construction") is an (huge) extension of these basic rules. For instance, we'll be able to define extra (inductive) types or (recursive) functions.
## Computations
Computation rule for λ-calculus : the β-reduction, where `(λx.t) u` gives `t{x:=u}` (for some reasonable definition of substitution).
In λ-calculus, this reduction may occur anywhere, in any order.
Example of theoretical property of this reduction : the confluence (see for instance https://plfa.github.io/Confluence/ ).
Famous example of term whose reduction is infinite : `Δ Δ` with `Δ = λx.(x x)`. From that, *fixpoint combinators* can be created and used for defining recursive functions in raw λ-calculus (but that's quite tricky, see the Y combinator for instance).
Now, in simply typed λ-calculus, computations interact nicely with types :
- The type is preserved during reduction (property known as "subject reduction").
- Strong normalization : a well-typed term may not have infinite reduction (hence `Δ Δ` cannot be well-typed).
- Strong normalization + confluence implies that reducing a well-typed term `t` as long as possible in any possible manner always ends on the unique normal form `t₀` of `t`.
Coq has the same β-reduction rule. Unlike in OCaml, this reduction may occur anywhere (but a concrete command such as `Compute` does implement a particular strategy).
Coq satisfies a subject reduction property, which is critical to exclude a whole family of runtime errors just by static typing (e.g. no "segfaults" in OCaml). Roughly, "if it types, it runs ok".
Of course, no direct equivalent of `Δ Δ` or fixpoint combinators in Coq due to typing. Instead, Coq provides a native way to define recursive functions (see later). Unlike OCaml, this is not a general recursivity, but only recursive functions that "obviously" terminates (for some criterion). This way, Coq is strongly normalizing. Moreover no trivial closed proofs of `False` could be built (see later). But this also implies that Coq is not *Turing-complete*. We'll see how the programmer may cope with that.
## Some more details on Coq types
No syntactic differences between Coq types and other terms : in Coq everything is term (unlike OCaml for instance).
Morally, a type is just something that may occur on the right of a typing judgment `Γ ⊢ t:τ`.
Now, since a type is in particular a Coq term, it should have a type. In Coq a important property is that whenever `Γ ⊢ t:τ` and `Γ ⊢ τ:s`, then
`s` is necessarily a *sort* (or universe), i.e. one of the constants `Type` or `Set` or `Prop`. This gives us a concrete definition of a Coq type : anything whose type is a sort.
* `Type` is the most general sort in Coq.
* `Prop` is used to express logical statements, we'll encounter it in the second half of this course
* `Set` is a (deprecated) alias for a `Type` "of lowest level"
To avoid paradoxes coming from `Γ ⊢ Type : Type`, actually `Type` is not just one universe but a hierarchy `Type₀ : Type₁ : Type₂ : ...`.
Normally these indices are hidden to the users, and we will not say more
about that here.
In Coq, the arrow type `A->B` is actually not a primitive construction, it is a particular case of a *product* `∀x:A,B` (Coq syntax `forall x:A, B`). When variable `x` does not occur in `B` (non-dependent product), we write `A->B`. For a first example of dependent product, see the definition of identity below.
Roughly, the typing rule for a product looks like :
- If `Γ ⊢ A:Type` and `Γ+x:A ⊢ B:Type` then `Γ ⊢ (forall x:A,B) : Type`
In reality, one must take care of the indices of the `Type` universes : lthe rightmost index is the max of the two others. And this typing rule has a particular case for `Prop` that we will not detail here.
We can now generalize the typing rules for functions and applications:
- If `Γ+x:A ⊢ t:B` then `Γ ⊢ (fun x => t):(forall x:A, B)`
- If `Γ ⊢ t:(forall x:A,B)` and `Γ ⊢ u:A` then `Γ ⊢ (t u) : B{x:=u}`
Note that for a non-dependent product, we recover the former rules for `A->B`. In particular, if `x` does not occur in `B` then `B{x:=u} = B`.
## Coq constants
Alongside variables and their types, a Coq typing context (or environment) `Γ` may also contain "constants" `(c:t:=u)` where `c` is the constant name, `t` and `u` are Coq terms giving the type and the definition body for this constant.
Of course, the system checks that `Γ ⊢ u:t` before accepting to add this constant `c` to the environment.
A reduction rule named `δ` (delta) allows to replace `c` by its body `u` at any time.
Beware of the vocabulary: since `u` may be a `fun`, this Coq "constant" may actually be a function, hence not so "constant" after all.
Coq syntax for adding such a global constant to the system:
```coq
Definition c : t := u.
```
When Coq is able to "infer" the type `t` from definition body `u`, writing `: t` is not mandatory. This is quite frequent (but not all Coq terms have a type that can be inferred automatically).
For a function definition (i.e. a body starting with `fun`), we could also write the arguments just after the function name.
For instance, all the following lines are equivalent:
```coq
Definition id_1 : forall X, X->X := fun (X:Type)(x:X) => x.
Definition id_2 : forall X, X->X := fun X x => x. (* type inference in fun *)
Definition id_3 := fun (X:Type)(x:X) => x. (* inference of the constant type *)
Definition id_4 (X:Type)(x:X) : X := x. (* constant with arguments after the constant name *)
Definition id_5 (X:Type)(x:X) := x. (* same, without explicit constant type *)
Definition id_6 X (x:X) := x. (* default sort is Type *)
```
Coq also provides a `let ... in` syntax for local definitions:
```
Definition test :=
let id := fun X (x:X) => x in
let id2 X := id (X->X) (id X) in
let id4 X := id2 (X->X) (id2 X) in
id4.
```
A `let x:=t in u` behave almost like `((fun x=>u) t)`.
Once again, a reduction rule (`ζ`, zeta) allows to discard this local abbreviation by replacing everywhere `x` by `t` in `u`.
## First data types : boolean and natural numbers.
Coq provides a type `bool` and constants `true` and `false`.
There is a construction `if ... then ... else ...`.
Some predefined boolean operations :
- negation : `negb`
- logical "and" : `andb` (syntax `&&` after doing `Open Scope bool_scope`)
- logical "or" : `orb` (syntax `||`)
Beware, unlike usual programming languages, the evaluation of `&&` and `||` is not necessarily *lazy* in Coq.
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.
For access to operations on natural numbers, load the `Arith` library:
```coq
Require Import
```
Some operations : addition `+`, multiplication `*`, euclidean division `/`, modulo `x mod y`.
Boolean comparisons of numbers : `x =? y` or `x <? y` or `x <=? y`.
We will see later how to perform efficient arithmetical operations (binary encoding) and how to handle negative numbers (type `Z`).
## Recursivity
`Fixpoint` allows to reuse the function we are actually defining in itself !
Before accepting a `Fixpoint`, Coq checks that this definition is syntactically decreasing. For that, a criterion of *stuctural decrease* is used, we will detail it later. In short, recursive calls must be done on *strict sub-terms*. Practically, this means using a construction `match ... with ... end` for accessing the previous integer (for instance).
```coq
Fixpoint factorial (n:nat) :=
match n with
| 0 => 1
| S m => (factorial m) * n
end.
```
This criterion is quite restrictive. For instance here, replacing `factorial m` with `factorial (n-1)` est refused, even though we could prove later that `m = (n-1)` in this case.
## First-class function and partial application
Functions may be given as arguments to other functions, or come as answers.
Functions may receive less that the expected number of arguments.
......@@ -15,7 +15,7 @@ Il y a plusieurs manières d'utiliser Coq:
Chaque méthode a ses aficionados (même la dernière...).
Par convention, les fichiers Coq utilise l'extension `.v` (pour "vernaculaire"...).
Par convention, les fichiers Coq utilisent l'extension `.v` (pour "vernaculaire"...).
Une fois lancées, les interfaces `coqide`, `proofgeneral` et `jsCoq` proposent une disposition assez similaire : le fichier en cours d'édition est à gauche, tandis que les preuves en cours seront affichées en haut à droite, et les messages du système en bas à droite (réponses de Coq ou messages d'erreurs). La portion du fichier déjà soumise à Coq est indiquée par des couleurs, et ces interfaces permettent de faire descendre cette zone, en envoyant une ou plusieurs phrases à Coq, ou au contraire de remonter (retour à un ancien état de Coq).
......
Functional Programming in Coq : TD1
===================================
**M2 LMFI**
## Launching Coq
There are several ways to use Coq:
* via `coqide`, a graphical interface based on `gtk`
* via `proofgeneral`, which is a plugin for `emacs`
* 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 the `ocaml` interactive loop.
Each method has its advocates (even the last one...).
The coq source files are always named with `.v` as extension (for "vernacular"...).
After launch, both `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).
In the source file, colors are used to indicate which part of the file has already been processed by Coq, and this colored zone will grow when we send more phrases to Coq. Conversely the colored zone may also shrink if we "undo" and get Coq back to some earlier state.
Until January, we will mostly use the following commands:
* `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.
A dot `.` is mandatory to end each Coq phrase.
## Functions and only that
#### Exercise 1 : function composition
Define a function `compose : forall A B C, (B->C)->(A->B)->(A->C)`. Test it with functions `S` and `pred` on natural numbers (type `nat`).
#### Exercise 2 : boolean ersatz
Define (without using `bool` nor any other inductive type):
- a type `mybool : Type`
- two constants `mytrue` and `myfalse` of type `mybool`
- a function `myif : forall A, mybool -> A -> A -> A` such that `myif mytrue x y` computes to `x` and `myif myfalse x y` computes to `y`
#### Exercise 3 : Church numerals
Encode in Coq the Church numerals, for which the number `n` is represented by `λfλx.(f (f (... (f x))))` where `f` is applied `n` times.
More precisely, define (without using `nat` nor any other inductive type):
- a type `church : Type`
- two constant `zero` and `one` of type `church`
- a function `succ` of type `church->church`
- two fonctions `plus` and `mult` of type `church->church->church`
- a function `power`
- a test `iszero`
Also define two functions `nat2church : nat -> church` and `church2nat : church -> nat`
## Base types
#### Exercise 4 : booleans
- Write a function `checktauto : (bool->bool)->bool` which tests whether a boolean unary function always answers `true`.
- Same for `checktauto2` et `checktauto3` for boolean fonctions expecting 2, then 3 arguments. This can be done by enumerating all cases, but there is a clever way to proceed (for instance by re-using `checktauto`.
- Check wether `fun a b c => a || b || c || negb (a && b) || negb (a && c)` is a tautology.
Note : the command `Open Scope bool_scope.` activates notations `||` and `&&` (respectively for functions `orb` and `andb`).
- Define some functions behavint like Coq standard functions `negb` and `orb` and `andb`.
#### Exercise 5 : usual functions on natural numbers.
Define the following functions on `nat` (without using the ones of Coq standard library):
- addition
- multiplication
- subtraction
- factorial
- power
- gcd
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment