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

seance2 : remplissage de paragraphes laissés pour plus tard

parent 59219ac8
......@@ -68,23 +68,59 @@ let delta = Poly (fun x -> app x x)
let dd : 'a = app delta delta
```
## Match, fix, règles de réduction associées
## Match
TODO
Le *match* (ou *pattern-matching*) est une analyse de cas, en suivant les constructeurs d'un type inductif.
A part de petites différences syntaxique (`=>` et mot-clé `end`), il se comporte de manière très similaire au `match` d'OCaml.
## Exemples de types inductifs usuels
```coq
match ... with
| C₁ x₁₁ ... x₁ₚ => ...
| ...
| Cₙ xₙ₁ ... xₙₖ => ...
end
```
La *tête* du match (ce qu'il y a entre `match` et `with`) doit être du bon type inductif, celui correspondant aux constructeurs `C₁` ... `Cₙ`.
Habituellement, les *branches* (les portions après `=>`) contiennent du code d'un même type. On verra par la suite que ceci n'est pas obligatoire (cf. la séance sur les types *dépendants*).
Réduction d'un match : lorsque la tête d'un match commençe par un constructeur inductif `Ci`, une *iota-réduction* est possible, elle remplace alors tout le match par la branche correspondante au constructeur `Ci`, en replaçant dedans les variables `xi₁`...`xiₚ` par les arguments concrets du constructeur en tête de match.
## Fix
La construction ̀Fixpoint` va permettre de créer des fonctions récursives en Coq. Attention, comme mentionné auparavant, certaines fonctions récursives seront rejetées par Coq, qui ne va accepter que des *fonctions récursives structurellement décroissantes*.
Le mot-clé `Fixpoint` s'emploie à la place du mot-clé `Definition`, voir les exemples plus bas (ou dans les TD).
TODO, grosso modo, c'était:
Il est également possible de définir une fonction récursive interne, à tout endroit d'un code, via le mot-clé `fix` (exemples la semaine prochaine). En fait, `Fixpoint` n'est pas une construction primitive de Coq, c'est un `Definition` suivi d'un `fix`.
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).
## Quelques types inductifs usuels
### Les entiers naturels en représentation de Peano
```coq
Print nat.
```
Require Import ZArith.
### Représentation binaire des entiers
```coq
Require Import ZArith.
Print N.
Print positive.
Print Z.
```
Note : passer par un type des entiers strictement positifs permet d'assurer l'unicité de la représentation, aussi bien pour `N` que pour `Z`. En particulier il y a un seul codage de zéro (`N0` dans le type `N`, `Z0` dans le type `Z`).
### Paires Coq
```coq
Print prod.
Definition fst {A B} (p:A*B) := match p with
......@@ -93,19 +129,29 @@ Definition fst {A B} (p:A*B) := match p with
Definition fst' {A B} (p:A*B) :=
let '(a,b) := p in a.
```
Inductive unit : Type := tt : unit.
### Un premier exemple de type dépendant
(** Un premier exemple de type dépendant *)
```coq
Inductive unit : Type := tt : unit.
Fixpoint pow n : Type :=
match n with
| 0 => unit
| S n => (nat * (pow n))%type
end.
```
### Le type option
```coq
Print option.
```
### Le type des listes
```coq
Print list.
Require Import List.
......@@ -118,7 +164,13 @@ Fixpoint length {A} (l : list A) :=
| [] => 0
| x :: l => S (length l)
end.
```
### Arbres en Coq
Contrairement à ce qui précède, ceci n'est pas un type prédéfini en Coq. En effet il y a tellement de types d'arbres différents selon les besoins que c'est à l'utilisateur de définir le sien. Par exemple, voici une version avec rien aux feuilles et une donnée entière aux noeuds.
```ocaml
Inductive tree :=
| leaf
| node : nat -> tree -> tree -> tree.
......
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