Commit 07797e4f authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Sections redondantes avec la partie 1 du cours indiquées comme Révisions:

parent 45c0c04b
......@@ -7,20 +7,23 @@ Pierre Letouzey (d'après A. Miquel)
> La documentation du système Coq est consultable en ligne: http://coq.inria.fr/doc/
### Démarrage du système ###
### Révision : Démarrage du système ###
Il existe actuellement plusieurs manières principales 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/
* 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 à la `ocaml`
Chaque méthode a ses aficionados (même la dernière). Pour utiliser `proofgeneral` sur les machines de l'UFR, il suffit d'ajouter la ligne `(load-file "~letouzey/.emacs-coq")` à votre `.emacs` puis lancer `emacs` sur un fichier Coq (d'extension `.v`).
Chaque méthode a ses aficionados (même la dernière).
Une fois lancées, les deux interfaces `coqide` et `proofgeneral` 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).
Par convention, les fichiers Coq utilise l'extension `.v` (pour "vernaculaire"...).
### Commandes Coq ###
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).
### Révision : Commandes Coq ###
En Coq, une commande est formée d'un nom de commande (commençant par une majuscule), éventuellement suivie d'un ou plusieurs arguments, et terminée par un point. Exemples:
```
......
......@@ -5,7 +5,7 @@ M2 LMFI
Pierre Letouzey (d'après A. Miquel)
### Le type inductif des entiers ###
### Révision : Le type inductif des entiers ###
En Coq, l'introduction d'un nouveau type de données s'effectue à l'aide d'un mécanisme de *définition inductive* qui ressemble beaucoup à la définition d'un type concret en Caml. Ainsi, le type `nat` des entiers naturels est introduit dans la bibliothèque standard de Coq (cf. fichier [Init/Datatypes.v](https://coq.inria.fr/stdlib/Coq.Init.Datatypes.html)) à l'aide de la définition inductive suivante:
```
......@@ -20,6 +20,8 @@ constantes:
- le constructeur `S : nat -> nat`
Attention, le constructeur du zéro s'appelle `O` à la base (la lettre O), même si le système accepte ensuite aussi des notations à bases de chiffres : `0` pour `O`, `1` pour `(S O)`, `2` pour `(S (S O))`, etc.
### Principes d'induction ###
La définition inductive ci-dessus engendre automatiquement un certain nombre de principes d'induction, dont le plus utilisé en pratique est le schéma de récurrence :
```
nat_ind :
......
......@@ -5,7 +5,7 @@ M2 LMFI
Pierre Letouzey (d'après A. Miquel)
## Définition des listes en Coq ##
## Révision : Définition des listes en Coq ##
En Coq, on peut charger via les commandes suivantes la définition
standard des listes, leurs notations, ainsi que des fonctions
......@@ -39,7 +39,7 @@ réponse avec `Check list_ind`.
qui généralise le type flèche `T -> U`, et qu'on appelle
*produit dépendant*.
#### Arguments implicites ####
#### Révision : Arguments implicites ####
Normalement, des types de la forme `forall A : Type,...` pour
`nil` et `cons` font donc que ces derniers attendent un premier argument
......@@ -59,7 +59,7 @@ Sinon, une autre approche possible est d'utiliser la syntaxe
`{A:Type}` au lieu de `(A:Type)` pour les arguments de fonctions que
l'on souhaite rendre implicites (cf. la définition de `app` ci-dessous).
#### Notations ####
#### Révision : Notations ####
En plus des implicites, Coq fournit également un système de notations
permettant d'alléger l'écriture. Pour les listes, des notations
......
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