Commit 85c91818 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

seance1 : notes de cours

parent d6681028
Introduction à la Programmation Fonctionnelle en Coq
====================================================
**M2 LMFI**
## Démarrage
Il y a plusieurs manières d'utiliser Coq:
* via `coqide`, une interface graphique basée sur `gtk`
* via `proofgeneral`, qui est un mode pour `emacs`
* directement dans son navigateur en utilisant `jsCoq`, voir p.ex. https://x80.org/collacoq/
* ou éventuellement en lançant `coqtop`, une boucle d'interaction textuelle assez frustre à la `ocaml`
Chaque méthode a ses aficionados (même la dernière...).
Par convention, les fichiers Coq utilise 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).
Dans ce cours nous allons essentiellement utiliser les commandes suivantes:
* `Definition` : associe un nom à un terme Coq (non-récursif)
* `Fixpoint` : idem pour une définition récursive
* `Inductive` : création d'un nouveau type (inductif)
* `Check` : afficher le type d'un terme Coq
* `Print` : afficher le corps d'une définition ou le détail d'un type inductif
* `Compute` : calculer un terme, c'est-à-dire demander sa forme normale.
Un point `.` sert de terminateur à chaque phrase Coq.
## Coeur fonctionnel de Coq
Présentation du lambda-calcul, avec ses trois constructions de base :
- variables
- abstraction de fonction : `λx.t` (correspondant à `fun x => t` en Coq)
- application de fonction : `t u` (idem en OCaml)
Règle de calcul : la β-réduction où `(λx.t) u` donne `t{x:=u}` (la définition de la substitution est laissée en exercice).
Exemple de propriété théorique de la réduction du lamda-calcul : la confluence.
Exemple de terme dont la réduction est infinie : `ΔΔ` valant `(λx.(x x))(λx.(x x))`.
Pas d'équivalent en Coq pour des raisons de typage.
Typage simple du lambda-calcul :
- On type les variables en regardant dans un environnement de typage Γ
- Si `Γ+x:τ ⊢ t:σ` alors `Γ ⊢ (λx.t):(τ→σ)`
- Si `Γ ⊢ t:(τ→σ)` et `Γ ⊢ u:τ` alors `Γ ⊢ (t u) : σ`
Lien avec la logique minimale (gérant uniquement l'implication) : il suffit de ne garder que les types dans les règles précédentes.
C'est (le début de) l'isomorphisme de Curry-Howard.
Le typage de Coq est une évolution de ces règles de départ.
Propriétés essentielles du lambda-calcul simplement typé :
- Préservation du typage lors de la réduction
- Normalisation forte : un terme bien typé ne peut avoir de réduction infinie.
Ceci combiné à la confluence signifie que la réduction d'un terme `t` finit toujours en temps fini sur une unique forme normale `t₀` de `t`.
Même si le lambda-calcul de Coq (nommé CIC pour "Calculus of Inductive Construction") est bien plus riche, il satisfait encore ces propriétés.
Note: la terminaison de tous les calculs n'est normalement *pas* une propriété souhaitable pour un langage de programmation (cf par exemple la récursion générale d'Ocaml : `let rec`). Pour Coq ce choix permet de garantir l'absence de preuves closes de `False`. On verra par la suite l'impact de ce choix sur le programmeur.
## Un premier point sur les types Coq
Pas de différences syntaxiques entre les types Coq et les autres termes, en Coq tout est terme.
Moralement, un type est quelque chose qui peut être à droite d'un jugement de typage `Γ ⊢ t:τ`.
On peut aussi se poser la question du type d'un type. En Coq un type de type va forcément être une *sorte* ou (univers), à savoir `Type`, `Set` ou `Prop`.
* `Type` est la sorte la plus générale en Coq.
* `Prop` sert à exprimer des propriétés logiques, on le verra très peu dans ce cours
* `Set` est un alias désuet pour un cas particulier de `Type`
Pour éviter des paradoxes liés à `Γ ⊢ Type : Type`, il n'y a pas un univers `Type` mais une hiérarchie `Type₀ : Type₁ : Type₂ : ...`.
Normalement ces indices sont cachés à l'utilisateur, et on n'aura pas besoin de rentrer dans ces considérations.
En Coq, le type flèche `A->B` n'est pas primitif, c'est un cas particulier d'une construction plus générale, le *produit* `∀x:A,B` (syntaxe Coq `forall x:A, B`). Lorsque la variable `x` n'apparaît pas dans `B` (produit *non-dépendant*), on écrit `A->B`. Pour un premier exemple de produit dépendant, voir par exemple la définition de l'identité dans la section suivante.
En première approximation, la règle de typage d'un produit ressemble à ceci:
- Si `Γ ⊢ A:Type` et si `Γ+x:A ⊢ B:Type` alors `Γ ⊢ (forall x:A,B) : Type`
En réalité, il faudrait se préoccuper des indices des univers `Type` : le dernier est le max des deux précédents. Et cette règle de typage a également une variante pour `Prop`, qui ne nous intéresse pas ici.
On généralise alors les règles de typage des fonctions et applications:
- Si `Γ+x:A ⊢ t:B` alors `Γ ⊢ (fun x => t):(forall x:A, B)`
- Si `Γ ⊢ t:(forall x:A,B)` et `Γ ⊢ u:A` alors `Γ ⊢ (t u) : B{x:=u}`
Notez que pour un produit non-dépendant, on retrouve les anciennes règles pour `A->B`. En particulier, si `x` n'apparaît pas dans `B` alors `B{x:=u} = B`.
## Constantes Coq
Outre des variables et leurs types, l'environnement `Γ` de Coq peut également contenir des "constantes" `(c:t:=u)``c` est le nom de la constante, et `t` et `u` sont deux termes Coq donnant le type et le corps de cette constante.
Evidemment, le système vérifie `Γ ⊢ u:t` avant d'accepter l'ajout de cette constante `c` à l'environnement.
Une règle de réduction nommée `δ` (delta) permet à tout moment de remplacer `c` par son corps `u`.
Attention au vocabulaire, comme `u` peut être un `fun`, notre constante peut être une fonction, donc pas si "constante" que cela.
Syntaxe d'ajout d'une constante globale au système:
```coq
Definition c : t := u.
```
Si Coq peut "inférer" le type `t` à partir du corps `u` de la définition, la partie `: t` est alors optionnelle.
Pour une définition de fonction (corps débutant par `fun`), on peut également placer les arguments juste après le nom de la fonction.
Par exemple les lignes suivantes sont équivalentes :
```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 dispose également d'une syntaxe `let ... in` permettant de nommer localement des termes.
```
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.
```
Un `let x:=t in u` se comporte quasiment comme `((fun x=>u) t)`.
Là encore, une règle de réduction (`ζ`, zeta) permet de supprimer cette abbréviation locale en remplaçant partout `x` par `t` dans `u`.
## Premiers types de données : Booléens et Entiers
Coq fournit le type `bool` et ses constantes `true` et `false`.
On dispose d'une construction `if ... then ... else ...`.
Quelques opérations booléennes :
- la negation : `negb`
- le "et" logique : `andb` (syntaxe `&&` après un `Open Scope bool_scope`)
- le "ou" logique : `orb` (syntaxe `||`)
Attention, contrairement aux langages usuels, l'évaluation de `&&` et `||` n'est pas forcément *paresseuse* en Coq.
Pour la suite, chargez la bibliothèque `Arith`:
```coq
Require Import
```
Coq fournit un type `nat` des entiers naturels. Attention c'est un codage "unaire" (entiers de Peano) donc extraordinairement lent.
Quelques opérations sur les entiers : addition `+`, multiplication `*`, division entière `/`, modulo `x mod y`.
On disposera de comparaisons sur les entiers : test d'égalité `x =? y` ou d'ordre `x <? y` ou `x <=? y`, etc.
Attention en Coq 8.4 il faut charger également la bibliothèque ̀NPeano` et installer une notation manquante:
```coq
Infix "=?" := Nat.eqb (at level 70, no associativity) : nat_scope.
```
On verra par la suite des structures d'entiers plus efficaces (codage binaire) et/ou étendu aux nombres relatifs (type `Z`).
## Recursivité
`Fixpoint` permet de réutiliser la fonction qu'on est en train d'écrire !
Avant d'accepter un `Fixpoint`, Coq vérifie que cette définition récursive est visiblement décroissante. Cela se fait selon un critère de décroissance *structurelle* que nous alors revoir plus en détail par la suite. En résumé, les appels récursifs doivent avoir lieu sur des *sous-termes stricts*. En pratique, cela signifie utiliser la construction `match ... with ... end` pour obtenir (par exemple) l'entier immédiatement précédent celui de départ.
```coq
Fixpoint factorial (n:nat) :=
match n with
| 0 => 1
| S m => (factorial m) * n
end.
```
Ce critère est très contraignant. Par exemple ici remplacer le `factorial m` par un `factorial (n-1)` est refusé !
## Fonctions de première classse et application partielle
Des fonctions en argument ou en réponse ...
Des arguments qui manquent ...
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