td1.md 3.63 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
Programmation Fonctionnelle en Coq : TD1
========================================

**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.

## Fonctions

#### Exercice 1 : composition

Pierre Letouzey's avatar
Pierre Letouzey committed
36
Définir la fonction `compose : forall A B C, (B->C)->(A->B)->(A->C)`. La tester avec les fonctions `S` et `pred` des entiers `nat`.
37
38
39
40
41
42
43
44

#### Exercice 2 : pseudo-booléens

Définir (sans utiliser `bool`):

 - un type `mybool : Type`
 - deux constantes `mytrue` et `myfalse` de type `mybool`
 - une fonction `myif : forall A, mybool -> A -> A -> A` telle que `myif mytrue x y` se réduise en `x` et `myif myfalse x y` se réduise en `y`
Pierre Letouzey's avatar
Pierre Letouzey committed
45

46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
#### Exercice 3 : entiers de Church

On cherche à encoder en Coq les entiers de Church, pour lesquels l'entier naturel `n` est représenté par `λfλx.(f (f (... (f x))))``f` est appliqué `n` fois.

Définir (sans utiliser `nat`):

 - un type `church : Type`
 - une constante `zero` et `one` de type `church`
 - une fonction `succ` de type `church->church`
 - des fonctions `plus` et `mult` de type `church->church->church`
 - une fonction puissance
 - un test à zéro

Définir également deux fonctions `nat2church : nat -> church` et `church2nat : church -> nat` 

## Types de base

#### Exercice 4 : booléens

  - Écrire une fonction `checktauto : (bool->bool)->bool` qui teste si une fonction booléenne à un argument répond toujours `true`.

  - Même chose avec `checktauto2` et `checktauto3` pour des fonctions booléennes à 2 puis 3 arguments. On peut faire ça en énumerant à la main tous les cas, mais il y a évidemment plus malin, par exemple réutiliser `checktauto`.

  - Tester si `fun a b c => a || b || c || negb (a && b) || negb (a && c)` est une tautologie.
Pierre Letouzey's avatar
Pierre Letouzey committed
70
    NB: la commande `Open Scope bool_scope.` permet de disposer des notations `||` et `&&` (en lieu et place de `orb` et `andb`)
71

Pierre Letouzey's avatar
Pierre Letouzey committed
72
73
  - Définir des fonctions se comportant comme `negb`, `orb`, `andb` du système.

74
75
76
77
78
79
80
81
82
83
#### Exercice 5 : fonctions usuelles sur les entiers

Définir les fonctions suivantes sur le type `nat` (sans utiliser celles fournies par le système):

  - addition
  - multiplication
  - soustraction
  - factorielle
  - puissance
  - pgcd