Commit 19e81a51 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

session 2 in english

parent ce857c1b
Functional Programming in Coq (session 2)
=========================================
**M2 LMFI**
## Universe constraints
A followup of session 1 : some (ab)use of Coq universes are rejected by the system, since they endanger the logical soundness. The reason is similar to Russel's paradox, it is known as the [Hurkens' paradox](https://coq.inria.fr/library/Coq.Logic.Hurkens.html) in type theory.
See [corrections/td1.v](corrections/td1.v) for an example of *universe inconsistency* when defining `church_minus` (additional question after exercice 3). Since `church` is `forall X, (X->X)->(X->X)` here we would like to form `church church` and have it equivalent to `(church->church)->(church->church)`. This amounts to replacing variable `X` (of a certain `Type_i`) by the whole `church` itself, but here `church` can only be in `Type_(i+1)` or more (try this typing yourself!) . This `church church` application is hence not doable when universe levels are fixed at the time `church` is defined. A solution here with a modern Coq : activate *universe polymorphism*, and let Coq pick universe levels when a definition is *used*, not when it is defined. This helps greatly in practice (but not always).
## General recursivity and logical consistence
Coq is logically sound as long as we cannot produce a *closed* proof of `False`, a type which is normally empty. Here *closed* means without variables nor axioms in the typing environment. Without even knowing how `False` is defined in Coq, a fully general recursivity would give us such a proof. Reminder : in Coq there is no syntactic distinction between proofs and programs.
```coq
Fixpoint loop (n:nat) : False := loop n
Definition boom : False := loop 0.
```
Obviously such a definition is rejected by Coq. Here is the `OCaml` equivalent of this code (no question of logical soundness in this case):
```ocaml
let rec loop (n:int) : 'a = loop n
let any : 'a = loop 0 (* Type-checking ok, but then the evaluation loops as expected *)
```
Similarly, Coq relies crucially on the property that a closed term in an *inductive* type (see next section) will evaluate (we say also "reduce") to one of the constructors of this type, followed by the right number of arguments. This allows to derive properties such as : all boolean expression is either equal to ``true` or to `false`, all natural number of type `nat` is either zero or a successor, etc.
Once again, an unrestricted general recursivity would break this property. For example:
```coq
Fixpoint flipflop (b:bool) := negb (flipflop b).
Definition alien : flipflop true.
```
If `flipflop` would be accepted by Coq (it is not!), we would have the equation `flipflop true = negb (flipflop true)`, and hence `alien = negb alien`. This `alien` cannot hence be `true`, nor `false`.
## Inductive types
The keyword `Inductive` allow to enrich the system with a new type definition, expressed via several *constructor* rules. The general syntax of a inductive type declaration is :
```coq
Inductive t :=
| C₁ : A₁₁ -> ... -> A₁ₚ -> t
| ...
| Cₙ : Aₙ₁ -> ... -> Aₙₖ -> t
```
The `Cᵢ` are *constructors* of type `t`, they may require some arguments (or not), but anyway they always have `t` as result type (after the rightmots arrow).
In fact, `t` itselft may have arguments, turning it into an *inductive type scheme* (we also say *inductive predicate*). We'll see examples of that later.
Basic examples (already in the Coq standard library, no need to copy-paste them).
```coq
Inductive bool :=
| true : bool
| false : bool.
Inductive nat :=
| O : nat
| S : nat -> nat.
```
## Positivity constraints
Some inductive declarations are rejected by Coq, once again for preserving logical soundness. Roughly speaking, the inductive type being currently declared cannot appear as argument of an arguments of a constructor of this type. This condition is named *strict positivity*.
Illustration of the danger, in OCaml:
```ocaml
(* First, a "lambda-calcul" version *)
type lam = Fun : (lam -> lam) -> lam (* In the type of Fun, the leftmost "lam" would be a non-positive occurrence in Coq *)
let identity = Fun (fun t -> t)
let app (Fun f) g = f g
let delta = Fun (fun x -> app x x)
let dd = app delta delta (* infinite evaluation, even without "let rec" ! *)
(* Second, a version producing a infinite computation in any type (hence could be in Coq's False) *)
type 'a poly = Poly of ('a poly -> 'a)
let app (Poly f) g = f g
let delta = Poly (fun x -> app x x)
let dd : 'a = app delta delta
```
In Coq, this term `dd` would be a closed proof of `False` is these kinds of inductive types would be accepted. Once again, this is also closely related with the fact that Coq is strongly normalizing (no infinite computations).
## Match
The *match* operator (or *pattern-matching*) is a case analysis, following the different possible constructors of an inductive type.
It is very similar to OCaml's match, except for little syntactic differences (`=>` in "branches", final keyword `end`).
```coq
match ... with
| C₁ x₁₁ ... x₁ₚ => ...
| ...
| Cₙ xₙ₁ ... xₙₖ => ...
end
```
The *head* of a match (what is between `match` and `with`) should be of the right inductive type, the one corresponding to constructors `C₁` ... `Cₙ`.
Usually, the *branches* (parts after `=>`) contains codes that have all the same type. We'll see later that this is not mandatory (see session on *dependent types*).
Computation and match : when the head of a match starts with a inductive constructor `Ci`, a *iota-reduction* is possible. It replaces the whole match with just the branch corresponding to constructor `Ci`, and also replaces all variables `xi₁`...`xiₚ` by concrete arguments found in match head after ̀Ci`.
Example:
```coq
Compute
match S (S O) with
| O => O
| S x => x
end.
```
This will reduce to `S O` (i.e. number 1 with nice pretty-printing). This computation is actually the definition of `pred` (natural number predecessor) applied to `S (S O)` i.e. number 2.
## Fix
The `Fixpoint` construction allows to create recursive functions in Coq. Beware, as mentionned earlier, some recursive functions are rejected by Coq, which only accepts *structurally decreasing recursive functions*.
The keyword `Fixpoint` is to be used in replacement of `Definition`, see examples below or in TD2.
Actually, there is a more primitive notion called `fix`, allowing to define an *internal* recursive function, at any place of a code. And `Fixpoint` is just a `Definition` followed by a `fix`. More on that later, but anyway, favor `Fixpoint` over `fix` when possible, it's way more convenient.
A `Fixpoint` or `fix` defines necessarily a function, with at least one (inductive) argument which is distinguished for a special role : the *decreasing argument* or *guard*. Before accepting this function, Coq checks that each recursive call is made on a syntactic *strict subterm* of this special argument. Roughly this means any subpart of it obtained via a `match` on this argument (and no re-construction afterwards). Nowadays, Coq determines automatically which argument may serve as guard, but you can still specify it manually (syntax `{struct n}`).
Computation of a `Fixpoint` or `fix` : when the guard argument of a fixpoint starts with an inductive constructor `Ci`, a reduction may occur (it is also called *iota-réduction*, just as for `match`). This reduction replaces the whole fixpoint with its body (what is after the `:=`), while changing as well in the body the name of the recursive function by the whole fixpoint (for preparing forthcoming iterations).
## Some usual inductive types
### nat : natural numbers represented as Peano integers
```coq
Print nat.
```
### Binary representation of numbers
```coq
Require Import ZArith.
Print positive.
Print N.
Print Z.
```
Nota bene : the "detour" by a specific type `positive` for strictly positive numbers allows to ensure that these representations are canonical, both for `N` and for `Z`. In particular, there is only one encoding of zero in each of these types (`N0` in type `N`, `Z0` in type `Z`).
### Coq pairs
```coq
Print prod.
Definition fst {A B} (p:A*B) := match p with
| (a,b) => a
end.
Definition fst' {A B} (p:A*B) :=
let '(a,b) := p in a.
```
### A first example of dependent type
```coq
Inductive unit : Type := tt : unit.
Fixpoint pow n : Type :=
match n with
| 0 => unit
| S n => (nat * (pow n))%type
end.
```
### The option type
```coq
Print option.
```
### The list type
```coq
Print list.
Require Import List.
Import ListNotations.
Check (3 :: 4 :: []).
Fixpoint length {A} (l : list A) :=
match l with
| [] => 0
| x :: l => S (length l)
end.
```
### Trees in Coq
No predefined type of trees in Coq (unlike `list`, `option`, etc). Indeed, there are zillions of possible variants, depending on your precise need. Hence each user will have to define its own (which is not so difficult). For instance here is a version with nothing at leaves and a natural number on nodes.
```ocaml
Inductive tree :=
| leaf
| node : nat -> tree -> tree -> tree.
```
Programmation Fonctionnelle en Coq (seance 2)
Programmation Fonctionnelle en Coq (séance 2)
=============================================
**M2 LMFI**
## Contraintes d'univers
Voir [td1.v] pour un exemple de *universe inconsistency* lors du `church_minus` (prolongement de l'exo 3): on voudrait que le type `church` puisse servir en tant que `X` dans le `forall X, (X->X)->(X->X)` qu'est `church`. Solution ici avec un Coq moderne: activer le *polymorphisme d'univers*.
En complément de la séance 1 : Coq rejète certains usages des univers menant à des cycles de typage, qui mettent en danger la cohérence de la logique. La raison en est similaire au paradoxe de Russel, on parle ici de [paradoxe de Hurkens](https://coq.inria.fr/library/Coq.Logic.Hurkens.html) en théorie des types.
Voir [corrections/td1.v](corrections/td1.v) pour un exemple de *universe inconsistency* lors du `church_minus` (prolongement de l'exo 3): on voudrait que le type `church` puisse servir en tant que `X` dans le `forall X, (X->X)->(X->X)` qu'est `church` lui-même. Mais si `X` est dans un certain `Type_i`, alors `church` ne peut être qu'au niveau `Type_(i+1)` ou plus (faites ce typage vous-même!). Et donc on ne peut pas former l'application `church church` si les niveaux d'univers sont figés lors de la définition de `church`. Solution ici avec un Coq moderne : activer le *polymorphisme d'univers*, qui déterminera les niveaux d'univers de chaque instance de `church` à l'utilisation, et non à la définition. Cela aide grandement en pratique (mais pas toujours).
## Récursion générale et cohérence logique
......@@ -97,7 +101,7 @@ Il est également possible de définir une fonction récursive interne, à tout
Un `Fixpoint` ou `fix` définit obligatoirement une fonction, un argument de cette fonction joue un rôle particulier, on parle d'argument de décroissance (ou de *garde*). Avant d'accepter cette fonction récursive, Coq vérifie que chaque appel récursif se fait sur un sous-terme strict de cet argument (c'est-à-dire quelque-chose sortant d'un match sur cet argument). Par défaut, Coq cherche automatiquement quelque argument peut jouer ce rôle de garde, mais on peut le spécifier manuellement (syntaxe `{struct n}`).
Réduction d'un `Fixpoint` ou `fix` : lorsque l'argument de garde d'un fix commençe par un constructeur inductif `Ci`, une réduction est possible (on parle aussi de *iota-réduction*). On remplace alors tout le fix par son corps (ce qui suit le `:=`), en changeant dedans le nom de la conction récursive par le fix de départ (pour permettre des itérations ultérieures).
Réduction d'un `Fixpoint` ou `fix` : lorsque l'argument de garde d'un fix commençe par un constructeur inductif `Ci`, une réduction est possible (on parle aussi de *iota-réduction*). On remplace alors tout le fix par son corps (ce qui suit le `:=`), en changeant dedans le nom de la fonction récursive par le fix de départ (pour permettre des itérations ultérieures).
## Quelques types inductifs usuels
......
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