Commit 4d513c3b authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

déménagement des fichiers Coq vers le dépôt coq-lmfi

parent f939754f
Cours de programmation fonctionnelle en Coq (M2 LMFI, Paris Diderot)
====================================================================
Ancien dépôt du cours de programmation fonctionnelle en Coq (M2 LMFI, Université de Paris)
==========================================================================================
Note: le sous-répertoire `ocaml` contient:
**Les fichiers sont [maintenant ici](https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/tree/master/1-prog)** dans un dépôt regroupant les deux parties du cours (programmation et preuves).
Il ne reste ici que le sous-répertoire `ocaml` contenant:
- les notes des séances de pré-rentrée (initiation à la programmation OCaml)
- des feuilles de TD en OCaml pour l'ancienne mouture de ce module (Modèles de la Programmation, en OCaml)
### Projet
A suivre très bientôt
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 judgment `Γ ⊢ 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 : the 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 *structural 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.
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`, p.ex. https://jscoq.github.io/node_modules/jscoq/examples/scratchpad.html
(voir https://github.com/ejgallego/jscoq pour le mode d'emploi)
* 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 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).
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 ...
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.