Library coq3_B_A_BA_ouf

INITIATION A COQ (3) : types dépendants et arbres de preuve

Objectif : illustrer l'idée suivant laquelle
  • développer un programme dans un langage fonctionnel typé, et
  • construire une démonstration
correspondent à des activités identiques. C'est encore plus frappant lorsque l'on considère un système de types enrichi, par rapport à OCaml, avec des *types dépendants*, comme illustré avec les fonctions "ouf" ci-dessous.

I. Prélimilaires et révisions

Type coulfeu et fonction coul_suiv (comme coq1_B_A_BA.v).
Inductive coulfeu : Set :=
  | Vert : coulfeu
  | Orange : coulfeu
  | Rouge : coulfeu
.

Definition coul_suiv : coulfeu → coulfeu :=
  fun c ⇒
    match c with
    | Vert ⇒ Orange
    | Orange ⇒ Rouge
    | Rouge ⇒ Vert
    end.

Définition interactive (comme coq2_B_A_BA.v). On énonce d'abord le type du programme attendu
Definition coul_suiv2 : coulfeu → coulfeu.
Proof.
  intro c.
  destruct c as [ | | ].
  Show Proof.
  - exact Orange.
  - exact Rouge.
  - exact Vert.
Defined.

C'est bien la même
Print coul_suiv2.

Définition interactive avec refine (comme coq2_B_A_BA.v).
Definition coul_suiv3 : coulfeu → coulfeu.
Proof.
  refine (fun c ⇒ _).
  refine (match c with
          | Vert ⇒ _
          | Orange ⇒ Rouge
          | Rouge ⇒ _
          end).
  - refine Orange.
  - refine Vert.
Defined.

II. Petite nouveauté : la tactique apply

Une fonction sans importance qui appelle coul_suiv.
Definition appelle_cs : coulfeu → coulfeu :=
  fun c ⇒
    match c with
    | Vert ⇒ Orange
    | Orange ⇒ coul_suiv Rouge
    | Rouge ⇒ Vert
    end.

En mode interactif, utiliser la tactique apply.
Definition appelle_cs2 : coulfeu → coulfeu.
Proof.
  intro c.
  destruct c as [ | | ].
  Show Proof.
  - exact Orange.
  - apply coul_suiv. Show Proof. exact Rouge.
  - refine (coul_suiv _). exact Vert.
Defined.

C'est bien la même sauf sur le dernier cas
Print appelle_cs2.

La tactique refine pour la construction explicite incrémentale du code.
Definition appelle_cs3 : coulfeu → coulfeu.
Proof.
  refine (fun c ⇒ _).
  refine (match c with
          | Vert ⇒ Orange
          | Orange ⇒ _
          | Rouge ⇒ Vert
          end).
  - refine (coul_suiv _). refine Rouge.
Defined.

C'est bien la même.
Print appelle_cs3.

III. Construction pas à pas d'une preuve vue comme un programme

On peut aussi utiliser refine pour écrire des arbres de preuve. À la place du type coulfeu → coulfeu, on énonce la formule du lemme à prouver.
Lemma suivsuivsuivp_id :
  ∀ c:coulfeu, coul_suiv (coul_suiv (coul_suiv c)) = c.
Proof.
On fabrique une fonction qui rend une preuve d'égalité pour tout c
  refine (fun c ⇒ _).
Raisonnement par cas (comme destruct)
    refine (match c with
          | Vert ⇒ _
          | Orange ⇒ _
          | Rouge ⇒ _
          end).
  - cbn [coul_suiv]. refine eq_refl
ce que fabrique reflexivity
.
  - reflexivity
marche même sans cbn
.
  - refine eq_refl
de même
.
Qed.

Oublions les preuves et revenons à la programmation ordinaire ... enfin, presque ordinaire : on commence par un programme calculant non pas une donnée, mais un type (qui s'écrit Set en Coq : le type de nat, etc.)
Ici on sort des possibilités de OCaml
Definition ouf : coulfeu → Set :=
  fun c ⇒
    match c with
    | Vert ⇒ nat
    | Orange ⇒ bool
    | Rouge ⇒ bool → nat
    end.

On l'utilise pour écrire une fonction de c dont le résultat dépend de c : c'est ce qu'on appelle un type dépendant : on ne peut pas l'écrire avec une flèche comme d'habitude, c-à-d. coulfeu → "quelque_chose", car ce "quelque_chose" dépend de l'entrée. Là encore, on sort des possibilités de OCaml (dans un match le type retourné est le même dans chaque cas).
Definition ouf_ouf : ∀ c : coulfeu, ouf c :=
  fun c ⇒
    match c with
    | Vert ⇒ 2
    | Orange ⇒ true
    | Rouge ⇒ fun b ⇒ match b with true ⇒ 8 | false ⇒ 5 end
    end.

En fait, A → B peut s'écrire ∀ a: A, B, exemple :
Check (∀ c : coulfeu, nat).

Développement interactif de ouf_ouf.
Definition ouf_ouf2 : ∀ c, ouf c.
Proof.
  refine (fun c ⇒ _).
  refine (match c with
    | Vert ⇒ _
    | Orange ⇒ _
    | Rouge ⇒ _
    end).
  - cbn [ouf]. refine 2.
  - cbn [ouf]. refine true.
  - cbn [ouf]. refine (fun b ⇒ _). destruct b as [ | ].
    + refine 8.
    + refine 5.
Defined.

Compute (ouf_ouf2 Vert).
Compute (ouf_ouf2 Orange).
Compute (ouf_ouf2 Rouge).
Compute (ouf_ouf2 Rouge false).

ouf_ouf2 est bien le la même chose que ouf_ouf.
Lemma meme_ouf_ouf : ouf_ouf2 = ouf_ouf.
Proof. reflexivity. Qed.

L'affichage fait apparaître une clause "return" dans le match. On voit alors explicitement que le programme reste bien typé.
Print ouf_ouf.
Print ouf_ouf2.

Definition suivsuivsuiv_id_direct :
  ∀ c:coulfeu, coul_suiv (coul_suiv (coul_suiv c)) = c :=
  fun c ⇒
    match c with
    | Vert ⇒ eq_refl
    | Orange ⇒ eq_refl
    | Rouge ⇒ eq_refl
    end.

  +-----------------------+
  | En résumé, à retenir. |
  +-----------------------+
En Coq on a deux activités : poser des définitions et démontrer des théorèmes. En réalité il s'agit d'une seule et même activité, car une démonstration n'est au fond rien d'autre qu'une fonction qui fabrique une preuve de la conclusion pour tout paramètre effectif donné en entrée, par exemple une preuve de coul_suiv (coul_suiv (coul_suiv c)) = c pour tout c. On est ici dans un univers où les preuves sont matérialisées par des arbres appelés arbres de preuve. Ces derniers sont, d'une manière générale, des structures de données dont on a vu jusqu'ici quelques espèces, notamment :
  • des feuilles étiquetées "réflexivité de l'égalité" fabriquant des preuves de formules x = x ;
  • des nœuds binaires étiquetés "rewrite" fabriquant une preuve de P y à partir d'un sous-arbre prouvant une égalité de la forme x = y et d'un sous-arbre prouvant P x ;
  • des nœuds étiquetés "intro" permettant de prouver des propriétés de la forme P → Q, ou plus généralement ∀x, P x ; on obtient ainsi des (AST de) programmes fonctionnels manipulant des (arbres de) preuves.
Les types de tous ces arbres de preuve sont exprimés avec une formule logique, comprenant notamment la flèche (se lisant indifféremment comme l'implication ou comme un type fonctionnel) et le quantificateur ∀.
Les formules Q → R et P → Q → R sont des types de fonctions ayant respectivement 1 et 2 arguments. Pour l'uniformité, on considérera que R est également le type d'une fonction, ayant 0 argument, ce qui permet de voir tous les arbres de preuve comme des (AST de) programmes fonctionnels.
On a également vu la notion de *type dépendant* sur l'exemple de la fonction ouf_ouf qui rend un résultat dont *le type* (et non seulement le résultat) dépend de l'entrée, ce qui est au-delà des possibilités des langages usuels y compris OCaml.
On observe alors qu'en tant que type, une proposition à démontrer telle que coul_suiv (coul_suiv (coul_suiv c)) = c est un type dépendant : d'une manière générale P vert et P rouge sont des propriétés distinctes, et en particulier coul_suiv (coul_suiv (coul_suiv Vert)) = Vert est une égalité distincte de coul_suiv (coul_suiv (coul_suiv Rouge)) = Rouge, même s'il se trouve que leurs preuves sont analogues du fait de la simplicité de l'exemple.
Plus profondément, on a illustré la correspondance suivante, dite de Curry-Howard : 
            preuve         =   programme fonctionnel (sous forme d'AST)
            formule        =   type
     prouver une formule   =   programmer
La correspondance de Curry-Howard est une avancée conceptuelle majeure qui fonde les assistants modernes à la preuve comme Coq.