ILU3 - Partie Coq

Présentation du logiciel Coq

• Implémenté en OCaml

• Initié par Thierry Coquand et Gérard Huet, et développé par Inria depuis 1984, la dernière version stable étant :

• Comprend un langage fonctionnel pur, statiquement typé, et très expressif (on détaillera cet aspect dans quelques minutes), muni d’un environnement de preuve interactive (vu au Cours n°2).

• Coq a une grande communauté d’utilisateurs. Projets notables :

  • CompCert : compilateur C99 complètement prouvé en Coq [Inria]

  • C-CoRN : bibliothèque d’analyse constructive [à Nijmegen]

  • Preuve formelle du théorème des 4 couleurs [G. Gonthier, B. Werner]

  • MathComp : bibliothèque d’algèbre et preuve formelle du théorème de Feit–Thompson (la preuve papier fait \({>}300\) pages) [Inria, Microsoft Research]

  • Vérification de systèmes critiques (voir par exemple :

    https://github.com/ligurio/practical-fm)

  • FiatCrypto : "Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises" (Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare.)

• Ouvrage (publié chez Springer et téléchargeable en français) :

  Coq'Art: Interactive Theorem Proving and Program Development

Caractéristiques intéressantes de Coq

• langage fonctionnel pur proche d’OCaml

  • terminaison garantie (impossible d’écrire let rec f x = f x)

  • typage fort et très expressif (on peut définir des listes à taille fixée, des fonctions à arité variable, etc.)

• langage logique (expression de formules quantifiées, etc.)

  forall n : nat, n > 0 -> exists m : nat, S m = n

• environnement de preuve (assistance à la construction de preuve)

• vérification automatique de la correction de ces preuves

  vérification de preuve = vérification de type
• tactiques utilisateur pour automatiser les preuves :

  tauto pour la logique des propositions,

  firstorder pour la logique du premier ordre,

  lia pour l’arithmétique linéaire sur les entiers (2 * (n + 1) - n > n)

  etc.

  Require Import Lia. (* pour utiliser la tactique "lia" *)

Rappel : installation de l’environnement de TP

Utilisations possibles de Coq

• Synthèse du type d’une expression :

Check fun x y => x + y + 1.
fun x y : nat => x + y + 1
     : nat -> nat -> nat

• Évaluation d’expressions (calcul) :

Eval compute in (fun x y => x+y+1) 2 3.
= 6
: nat

• Implantation de fonctions et vérification de leurs propriétés :

Definition f x := x + 2.

Theorem f_croissante : forall x y : nat, x < y -> f x < f y.
forall x y : nat, x < y -> f x < f y
Proof.
forall x y : nat, x < y -> f x < f y
(* On ne détaille pas pour le moment le script de preuve => Cours 2 *)
Qed.

• Définition de sous-types :

Definition Mod3 := {x : nat | x < 3}.

• Synthèse de fonctions à partir d’une preuve de sa spécification :

Definition pred :
  forall n : nat, (* précond *) n > 0 ->
    {m : nat | (* postcond *) S m = n}.
forall n : nat, n > 0 -> {m : nat | S m = n}
Proof.
forall n : nat, n > 0 -> {m : nat | S m = n}
(* On ne détaille pas pour le moment le script de preuve *)
Defined.

Require Extraction.
(* Génération automatique de code OCaml à partir du code Coq prouvé *)
Recursive Extraction pred.

type nat =
| O
| S of nat

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

(** val pred : nat -> nat **)

let pred = function
| O -> assert false (* absurd case *)
| S n' -> n'

Positionnement de Coq par rapport aux types abstraits

Exemple de vérification modulaire

• Définition d'une signature

Module Type tPickGt.
  Parameter pick : nat -> nat.
  Axiom pick_gt : forall n, pick n > n.
End tPickGt.

• Implantation de la signature

Module PickGt <: tPickGt. (* vérif conformité sans masquage *)
  Definition pick n := S n.
  Lemma pick_gt : forall n, pick n > n.
forall n : nat, pick n > n
  Proof.
forall n : nat, pick n > n auto. Qed.
End PickGt.

• Utilisation d'un module respectant la signature

Module Use (P : tPickGt).
  Definition num := P.pick O.
  Lemma num_gt0 : num > O.
num > 0
  Proof.
num > 0 apply P.pick_gt. Qed.
End Use.

• Instantiation du module paramétré

Module M := Use(PickGt).

Types et expressions

Exemples d’expressions Coq et leur type

Check 0.
0
     : nat

Check true.
true
     : bool

Check fun x => x + 1.
fun x : nat => x + 1
     : nat -> nat

Check nat.
nat
     : Set

Check Set.
Set
     : Type

Exemples avancés d’expressions Coq et leur type

Check 2 <= 2.
2 <= 2
     : Prop

Check le 2 2.
2 <= 2
     : Prop

Check le_n 2.
le_n 2
     : 2 <= 2

Check le_n.
le_n
     : forall n : nat, n <= n

Check le.
le
     : nat -> nat -> Prop

(* Prop est le type des formules logiques *)
Check Prop.
Prop
     : Type

Remarques

• Prop est le type des formules logiques ;

• à ne pas confondre avec bool, le type des booléens.

Les deux ont leur utilité :

• les prédicats renvoyant un bool correspondent à des "prédicats calculables" (par exemple un algorithme décidant si un entier est pair ou pas) : on peut déterminer leur résultat par un calcul ;

• les prédicats renvoyant un Prop correspondent à des "prédicats logiques" (définis par une formule) : on peut prouver leur véracité par un raisonnement.

Le type des listes : comparaison OCaml / Coq

Check list.
list
     : Type -> Type

Éléments de syntaxe

• Les mots "terme" et "expression" sont synonymes.

• Rappel :

  En Coq, tout terme bien formé a un type (y compris les types !) ;

  contrairement à OCaml, les termes/expressions et les types ne forment pas deux "collections disjointes" ;

  donc la grammaire des termes ci-dessous contient aussi Type, Set, Prop :

terme ::= Type | Set | Prop           "sortes" (= types de type)
        | var                         "variable"
        | ( terme )
        | terme terme                 "application"
        | terme op terme              "opérateur infixe"
        | fun var : terme ⇒ terme     "abstraction"
        | let var := terme in terme   "définition locale"
        | if terme then terme else terme
        | terme -> terme              "type flèche" (= type des fonctions)

Exemples

Que renvoient les commandes suivantes ?

Check fun x => x + 1.
fun x : nat => x + 1
     : nat -> nat

Check (fun f x => f (f x)) (fun x => x + 1).
(fun (f : nat -> nat) (x : nat) => f (f x))
  (fun x : nat => x + 1)
     : nat -> nat

Eval compute in (fun f x => f (f x)) (fun x => x + 1) 3.
= 5
: nat

Definition f1 := fun x => x + 1. Eval compute in f1 0.
= 1
: nat

Definition double f := fun (x : nat) => f (f x). Check double.
double
     : (nat -> nat) -> nat -> nat

Definition double2 (f : nat -> nat) := fun x => f (f x). Check double2.
double2
     : (nat -> nat) -> nat -> nat

Fail Definition double3 f := fun x => f (f x).
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (fun (f : ?T -> ?T) (x : ?T) => f (f x))
More precisely: 
- ?T: Cannot infer ?T in the partial instance
  "?T -> ?T" found for the type of f.

Cette dernière définition est refusée car en Coq, les paramètres de généricité sont explicites. Pas de synthèse automatique de leur nom ; il faut expliciter ces arguments.

Généricité

Une fonction générique prend un type en paramètre.

Exemple de définition d'une fonction générique : la fonction identité.

Definition id := fun (T : Type) => fun (x : T) => x.
(* ou *)
Definition id_v2 := fun (T : Type) (x : T) => x.
(* ou *)
Definition id_v3 (T : Type) := fun (x : T) => x.
(* ou *)
Definition id_v4 (T : Type) (x : T) := x.
(* ou *)
Definition id_v5 T (x : T) := x.

\(\leadsto\) ces fonctions ont toutes 2 arguments !

Utilisation d’une fonction générique

Check id nat.
id nat
     : nat -> nat

Check id nat 0.
id nat 0
     : nat

Check id bool.
id bool
     : bool -> bool

Check id bool true.
id bool true
     : bool


Print id.
id = 
fun (T : Type) (x : T) => x
     : forall T : Type, T -> T

Arguments id _%type_scope

Généricité et typage

Type d’une fonction générique

• En OCaml : id : 'a -> 'a \(\leadsto\) pour tout type 'a, id prend un argument de type 'a et retourne un résultat de type 'a

• En Coq : id : forall a, a -> a \(\leadsto\) la quantification est explicite

• extension du langage des termes :

terme ::= Type | Set | Prop
        | var
        | ( terme )
        | terme terme
        | terme op terme
        | fun var : terme ⇒ terme
        | let var := terme in terme
        | if terme then terme else terme
        | terme -> terme             (type d'une fonction)
        | forall var : terme, terme  (type d'une fonction générique)

• Comme on le verra par la suite, t1 -> t2 est en fait

  une syntaxe alternative (plus intuitive) de "forall _ : t1, t2".

  Check id.
  id
       : forall T : Type, T -> T
  

Inférence d'arguments

Dans le terme id bool true ci dessus, Coq pourrait deviner automatiquement le premier argument bool puisque c'est le type du deuxième argument true d'après le type de id. Il est effectivement possible d'écrire

Check id _ true.
id bool true
     : bool

Coq remplace automatiquement le _ par la seule valeur possible bool.

On peut ainsi remplacer tout sous terme par un trou _ et laisser Coq tenter de le remplir. Coq retourne une erreur quand il ne trouve pas de solution canonique.

Fail Definition id_bool := id bool _.
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (id bool ?x)
More precisely: 
- ?x: Cannot infer this placeholder of type "bool".

Généricité et arguments implicites I

Les remarques qui suivent ne sont pas "exigibles à l'examen" mais permettront d'avoir plus de confort, notamment en TP, en évitant de devoir expliciter tous les paramètres de généricité lors de l'appel d'une fonction polymorphe.

Les arguments implicites permettent d'écrire id true au lieu de id _ true. Redéfinissons la fonction id après activation des arguments implicites

Set Implicit Arguments. (* au début du fichier en principe *)

Definition id' (T : Type) (x : T) := x.
Print id'.
id' = 
fun (T : Type) (x : T) => x
     : forall T : Type, T -> T

Arguments id' [T]%type_scope


(* même code que *)
Print id.
id = 
fun (T : Type) (x : T) => x
     : forall T : Type, T -> T

Arguments id _%type_scope


(* mais *)
About id'.
id' : forall [T : Type], T -> T

id' is not universe polymorphic
Arguments id' [T]%type_scope
id' is transparent
Expands to: Constant ilu3_coq_1.id'
(* id' : forall [T : Type], T -> T *)

(\(\leadsto\) noter le [T] au lieu de T)

L'argument T est implicite : il peut être inféré à partir de l'argument d'après.

D'où une syntaxe concise à la OCaml :

Check id' true.
id' true
     : bool


Set Printing All. (* affiche tout, dont les arguments implicites *)
Check id' true.
@id' bool true
     : bool

Le @ indique que tous les arguments de id' sont explicités. Grâce aux arguments implicites, entrer id' true est equivalent à entrer

Check @id' _ true.
@id' bool true
     : bool

Unset Printing All.

Généricité et arguments implicites II

En OCaml :

let id x = x;;

id 0;; (* : int = 0 *)

id true;; (* : bool = true *)

En Coq :

Set Implicit Arguments.

Definition id T (x:T) := x.

Check id 0. (* id 0 : nat *)

Check id true. (* id true : bool *)

Paramètres de généricité : un plus gros exemple

En OCaml :

let comp f g x = g (f x);;

val comp : (’a -> ’b) -> (’b -> ’c) -> ’a -> ’c = <fun>

comp (fun x -> x + 1) (fun x -> x * 2) 3;;

\(\leadsto\) ?

En Coq :

Pas de synthèse du nom des paramètres de généricité : il faut déclarer ces paramètres de généricité lors de la définition.

(* Set Implicit Arguments. (* déjà fait auparavant *) *)

Definition comp T1 T2 T3 (f:T1->T2) (g:T2->T3) (x : T1) : T3 := g (f x).
(* ou *)
Definition comp_v2 T1 T2 T3 (f:T1->T2) (g:T2->T3) (x : T1) := g (f x).
(* ou *)
Definition comp_v3 T1 T2 T3 (f:T1->T2) (g:T2->T3) x := g (f x).
(* ou *)
Definition comp_v4 T1 T2 T3 f (g:T2->T3) (x:T1) := g (f x).
(* ou *)
Definition comp_v5 T1 T2 T3 (f:T1->T2) g (x:T1) : T3 := g (f x).

Eval compute in comp (fun x => x + 1) (fun x => x * 2) 3.
= 8
: nat

Exercices

1. Ecrire la fonction mult2 retournant le double de son argument.

Definition mult2 := (* todo *)0.

2. Supposons défini le prédicat leq : nat -> nat -> bool, retournant true si son 1er argument est inférieur à son second.

   Définir la fonction max retournant le plus grand de ses 2 arguments.

   En déduire la fonction max3 retournant le plus grand de ses 3 arguments.

   Ecrire une variante max3' où la définition de max est locale.

   Parameter leq : nat -> nat -> bool.
   
   Definition max := (* todo *)0.
   
   Definition max3 := (* todo *)0.
   
   Definition max3' := (* todo *)0.

3. Quel est le type de l'expression suivante ?

Definition expr3 := fun (T:Type) (f:T -> T) x => f (f x).
(* *)

4. Quel est le type de l'expression suivante ? (donner 2 syntaxes équivalentes)

Definition expr4 := fun (T:Type) => T -> T.

5. Quel est le type de l'expression suivante ?

Definition expr5 := fun (T:Type) (x:T) => x=x.

6. Écrire une fonction de type forall a b : Type, a -> b -> a

Definition expr6 := (* todo *)0.

7. Écrire une fonction de type forall a b : Type, a -> (a -> b) -> b

Definition expr7 := (* todo *)0.

8. Écrire une fonction de type forall a b c : Type, (a -> b -> c) -> (a -> b) -> a -> c

Definition expr8 := (* todo *)0.

9. Écrire une fonction de type forall a b c : Type, (a -> c) -> (a -> b -> c)

Definition expr9 := (* todo *)0.

10. Écrire une fonction de type forall a b c : Type, (a -> b -> c) -> b -> a -> c

Definition expr10 := (* todo *)0.

11. Écrire une fonction de type forall a b : Type, (a -> a -> b) -> a -> b

Definition expr11 := (* todo *)0.

12. Peut-on écrire une fonction de type forall a b : Type, a -> b ?

(* En OCaml :

   let exemple =

 *)

(* En Coq ? *)

Retour sur -> et forall

T1 -> T2 correspond :

• au type des fonctions de T1 dans T2, c’est-à-dire

• au type des fonctions qui associent à tout x:T1 un élément de T2,

• que l’on peut aussi écrire forall (x : T1), T2

forall est une notation :

• généralisant ->,

• utile lorsque le type d’arrivée T2 dépend du terme fourni x.

La correspondance de Curry–Howard : double lecture

Types inductifs

Définition d’un type inductif paramétré par a1,...,am.

En OCaml :

type ('a1, ..., 'am) t =     (* m paramètres de généricité *)
  | C1 of t1_1 * ... * t1_n1 (* constructeur C1 d'arité n1 *)
  | ...
  | Ck of tk_1 * ... * tk_nk (* kième constructeur *)

En Coq :

Inductive t a1 ... am :=
  | C1 (p1 : t1_1) ... (pn1 : t1_n1)
  | ...
  | Ck (p1 : tk_1) ... (pnk : tk_nk). (* ne pas oublier le point *)

Analyse par cas

En OCaml :

match x with
| C1 (x1, ..., xn1) -> ...
| ...
| Ck (x1, ..., xnk) -> ...

En Coq :

match x with
| C1 x1 ... xn1 => ...
| ...
| Ck x1 ... xnk => ...
end

Différences :

• Les constructeurs sont typiquement "curryfiés" en Coq.

• Les -> sont remplacées par =>

• Il y a un end en plus (pratique)

• Sinon c'est la même syntaxe :-)

Exemples de types inductifs

Type de données prédéfini dans Coq :

Print bool.
Inductive bool : Set :=  true : bool | false : bool


Inductive entier_nat := Zero | Succ (p : entier_nat).
Inductive liste T := Vide | Cons (x : T) (l : liste T).

Eléments d’un type inductif :

Check true.
true
     : bool


Check (Succ (Succ Zero)).
Succ (Succ Zero)
     : entier_nat


Definition liste1 := @Cons entier_nat (Succ Zero) (Vide entier_nat).
Print liste1.
liste1 = 
Cons (Succ Zero) (Vide entier_nat)
     : liste entier_nat

Fonctions récursives

Fixpoint add n m :=
  match n with
  | Zero => m
  | Succ p => Succ (add p m)
  end.

Fixpoint long T (l : liste T) :=
  match l with
  | Vide _ => Zero
  | Cons x r => Succ (long r)
  end.

Est-ce normal d'écrire Cons x r => Succ (long r) ?

Précisons :

• Le constructeur Cons a trois arguments,

• La fonction long a 2 arguments...

• Mais on avait activé les arguments implicites : Set Implicit Arguments.

• On pourrait néanmoins écrire en étant pleinement explicite :

Fixpoint long_v2 T (l : liste T) :=
  match l with
  | Vide _ => Zero
  | @Cons _ x r => Succ (@long_v2 T r)
  end.

Eval compute in long_v2 liste1.
= Succ Zero
: entier_nat

Remarque: Coq n'est pas limité aux fonctions primitives récursives. Par exemple, la fonction d'Ackermann peut être définie comme ci-dessous et il serait possible de démontrer qu'elle est identique à la définition usuelle:

Fixpoint pow (f:nat->nat) n a :=
  match n with
    0 => a
  | S p => pow f p (f a)
  end.

Fixpoint ack a b : nat :=
match a with
| 0 => S b
| S a => pow (ack a) (S b) 1
end.

Eval compute in (ack 3 4).
= 125
: nat            

Schémas inductifs

Preuve par récurence sur les entiers naturels (construits avec Zero, Succ)

Est-ce que la fonction suivante (ou son type) vous rappellent quelque chose ?

Fixpoint entier_nat_ind (P : entier_nat -> Prop)
(fZero : P Zero) (fSucc : forall n : entier_nat, P n -> P (Succ n))
(n : entier_nat) : P n :=
  match n with
  | Zero => fZero
  | Succ n => fSucc n (entier_nat_ind P fZero fSucc n)
  end.

qui a pour type :

Check entier_nat_ind.
entier_nat_ind
     : forall P : entier_nat -> Prop,
       P Zero ->
       (forall p : entier_nat, P p -> P (Succ p)) ->
       forall e : entier_nat, P e

Il s'agit du "Principe d’induction" pour les entiers naturels, généré automatiquement par Coq.

(Et il se trouve que le "code" qui implémente ce principe correspond à l'itérateur le plus général sur le type entier_nat :)

Le type en question est donc :

forall P : entier_nat -> Prop, P Zero ->
  (forall n : entier_nat, P n -> P (Succ n))
-> forall n : entier_nat, P n.

Un peu d’intuition sur ce principe d’induction

• Hypothèses :

  • pZero : preuve de P Zero

  • pSucc : preuve de \(\forall n,\ P n \implies P (n+1)\)

• Conclusion :

  • \(\forall n,\ P n\)

On peut l'écrire sous la forme d'une "Règle d'inférence" :

(pZero : P Zero)  (pSucc : forall n : entier_nat, P n -> P (Succ n))
--------------------------------------------------------------------
     entier_nat_ind P pZero pSucc :  forall n : entier_nat, P n

L'effet domino

Une petite image vaut mieux qu'un long discours :

Le type inductif des listes (prédéfini)

Require Import List.
Import ListNotations.
(* Set Implicit Arguments. (* déjà fait auparavant *) *)

Check list.
list
     : Type -> Type


Print list.
Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A

Arguments list _%type_scope
Arguments nil {A}%type_scope
Arguments cons {A}%type_scope a l%list_scope : rename

Fixpoint list_ind T (P : list T -> Prop)
(pNil : P nil) (pCons : forall x l, P l -> P (x :: l)) l
: P l :=
  match l with
  | [] => pNil
  | x :: r => pCons x r (@list_ind T P pNil pCons r)
  end.

Généré automatiquement !

Permet la "preuve par induction" sur les listes (construites avec [] et ::)

Règle d'inférence du schéma inductif des listes

(pNil : P [])  (pCons : forall x l, P l -> P (x :: l))
------------------------------------------------------
        list_ind P pNil pCons :  forall l, P l

Ici, on a omis les types implicites (le param. de généricité T) par simplicité.

Correspondance entre les types et les formules logiques

Exemple de types inductifs : propositions logiques

Inductive and (P Q : Prop) : Prop :=
  Conj (p : P) (q : Q).

-->

  (p : P)  (q : Q)
--------------------
 Conj p q :  P /\ Q

Inductive or (P Q: Prop): Prop :=
  | Or1 (p: P)
  | Or2 (q: Q).

-->

      p : P              q : Q
-----------------  -----------------
 Or1 p :  P \/ Q    Or2 q :  P \/ Q

Inductive True : Prop := I.  -->  ----------
                                   I : True

Inductive False : Prop := .  -->  pas de preuve de `False` !

Inductive ex T (P: T -> Prop) :=
  ex_intro (t: T) (p: P t).

-->

          (t : T)  (p : P t)
----------------------------------------
 @ex_intro T P t p :  exists x : T, P x

À suivre au prochain cours

• Retour sur la correspondance de Curry-Howard

• Présentation des "tactiques Coq"

  pour construire une preuve interactivement/semi-automatiquement !