UP | HOME

Praxis de la preuve en Coq
Du calcul des séquents aux tactiques

Table of Contents

1 Séquents en Coq

En Coq, les séquents sont intuitionnistes. Lorsque le séquent n'a pas de but, le but False est ajouté, ce qui est cohérent avec l'interprétation par une disjonction des buts. Dans notre description des séquents aux ordres supérieurs, nous avions distingué les propositions des déclarations. Dans la suite, nous procédons comme Coq, qui considère les propositions comme les autres types : les propositions sont aussi présentes dans les hypothèses du séquent sous forme de déclaration, la variable représentant une preuve de la proposition.

Séquent en Coq

hypothèses              Γ ::= ∅ | (h : p), Γ | (x : T), Γ | (f : T), Γ | (P : T), Γ
			      (liste de déclarations, éventuellement vide)
séquent intuitionniste si ::= Γ ⊢ p (en supposant la conjonction Γ, est déduit la proposition p)

Dans la suite, nous établissons la correspondance entre les règles du calcul des séquents et les tactiques. Une tactique permet de passer d'une conclusion à ses prémisses, en chaînage arrière. Les tactiques de Coq proviennent non pas du calcul des séquents mais de la déduction naturelle : en effet Coq repose sur la correspondance de Curry-Howard entre la programmation et la démonstration en déduction naturelle. Cependant, il est simple de traduire une preuve en calcul des séquents en une preuve en déduction naturelle. Nous étudierons cette traduction en même temps que la correspondance ; la correspondance avec les tactiques en donne déjà un aperçu.

De manière générale, nous choisissons les tactiques les plus élémentaires mais mentionnons cependant des tactiques plus élaborées qui étendent ces tactiques élémentaires. Lors de l'application d'une tactique, il peut être nécessaire de nommer des hypothèses. Deux options sont possibles : soit Coq procède automatiquement au nommage, soit l'utilisateur introduit les noms. Une bonne pratique est de ne jamais utiliser dans ses preuves les noms introduits automatiquement par Coq.

2 Tactiques pour les types fonctionnels

  • A -> B
    • fonctions de A vers B
    • implication par A de B (A, B : Prop)
      • interprétation probatoire : fonction associant à toute preuve de A une preuve de B
  • ∀(x : A), B_x
    • familles fonctionnelles (b_x : B_x)x : A
      • généralisation des fonctions
        • A -> B := ∀(x : A), B (B ne dépendant pas de x)
    • quantification universelle (lorsque (x : A) ⊢ B_x : Prop)
      • interprétation probatoire : famille associant à toute preuve ou élément x de A une preuve de B_x

Tactiques

2.1 [->-G]

Γ1 ⊢ p   (h : q), Γ2 ⊢ r         
------------------------ [->-G]  
(i : p -> q), Γ1, Γ2 ⊢ r
>   assert q as h; (apply i || idtac). (* première prémisse || seconde prémisse 
                                          apply i -> but p     idtac -> but r   *)

2.2 [->-D]

(h : p), Γ ⊢ q
-------------- [->-D]
  Γ ⊢ p -> q
> intro h.

2.3 inverse de [->-D] (règle dérivable)

		       ----------------------   ----------
Γ ⊢ p -> q             p -> q, (h : p), Γ ⊢ p   q, ... ⊢ q
----------             -----------------------------------
(h : p), Γ ⊢ p -> q    p -> q, (h : p), Γ ⊢ q   
--------------
(h : p), Γ ⊢ q
> generalize h.

Cette règle dérivable est utile pour faire passer des hypothèses dans le but. Elle est utilisée dans de nombreuses tactiques TODO.

2.4 [∀-G]

(h : p[x := t]), Γ ⊢ q   Γ ⊢ t : T       
---------------------------------- [∀-G] 
    (h : ∀(x : T). p), Γ ⊢ q
> specialize h with t.

2.5 [∀-D]

(x : T), Γ ⊢ p   Γ ⊢ Γ : Prop* 
------------------------------ [∀-D]
       Γ ⊢ ∀(x : T). p
> intro x.

2.6 inverse de [∀-D] (règle dérivable)

			    -------------------------   ------------------
Γ ⊢ ∀(x : T). p             p[x := x], (x : T), Γ ⊢ p   (x : T), Γ ⊢ x : T
----------                  -----------------------------------
(x : T), Γ ⊢ ∀(x : T). p    ∀(x : T). p, (x : T), Γ ⊢ p   
--------------
(x : T), Γ ⊢ p
> generalize x.

3 Tactiques pour les types inductifs

Considérons un système d'inférence I de paramétrisation p et d'indexation w. Les règles d'inférence ont la forme suivante, que nous avons simplifiée, les déclarations simples valant liste.

(x : P)               prémisses non-récursives
(z : Q)               prémisses récursives (Q = I ...)
-----------------     ------------------------
(c p x z) : I p u     conclusion (indexation u variable)

La définition en Coq de l'interprétation inductive de ce système d'inférence se fait ainsi, en une notation simplifiée. Bien noter que la paramétrisation forme les paramètres de I et que l'indexation sert à quantifier la sorte du système d'inférence (et apparaît souvent sous la forme dégénérée d'un type flèche).

Inductive I p : (* paramétrisation par p *)
  forall w, S (* indexation par w, S ::= Prop | Type *) 
:=
| c : forall x : P, forall z : Q, I p u (* u : instanciation de w *)
| ... (* autres constructeurs *)
.

En calcul des séquents, il existe une règle à gauche et des règles à droite permettant de décomposer (ou détruire) un type inductif, en chaînage arrière (de la conclusion aux prémisses).

3.1 [Ind-G] TODO

((x : P), (z : Q), Γ ⊢ A[h := c p x z, v := u])_c 
-------------------------------------------------
	     (h : I p v), Γ ⊢ A

Cette règle possède une prémisse par règle, identifiée par le constructeur c. La substitution appliquée au but A remplace la variable h par le constructeur appliqué à la paramétrisation p et aux nouvelles variables x et z représentant les prémisses du constructeur c. Elle remplace aussi l'indexation v de l'hypothèse h par l'indexation u calculée en fonction de la paramétrisation p et des prémisses x et z ; comme v n'est pas une variable, mais une expression, des pertes d'information sont possibles, au sens où le remplacement de v par u produit moins d'informations que l'égalité v = u. Lorsque le système d'inférence est purement paramétré sans être indexé, aucune perte n'est possible. Lorsque le système est indexé et que des pertes sont constatées, il est possible de procéder par transfert en convertissant le système indexé en un système paramétré équivalent et d'inverser la règle dans ce système. Il est aussi possible d'utiliser une tactique exploitant l'égalité v = u. Enfin, lorsque A correpspond à une proposition (A : Prop), il est rare d'avoir une dépendance de A relativement

Sans perte d'information

> case h as [x z | ...]. (* une décomposition par règle *)
> destruct h as [x z | ...]. (* destruct étend case. *)

Avec perte d'information

  • Tactique permettant l'inversion de l'indexation

    > inversion h as [x z | ...]. (* une décomposition par règle *)
    
  • Transfert vers le système paramétré équivalent IP via les implications eq_I_IP et eq_IP_I

    > apply eq_I_IP in h. (* Passage par IP *)
    > case h as [x z | ...]. (* une décomposition par règle, sans perte dans IP *)
    > apply eq_IP_I in z. (* Retour à I pour les prémisses récursives *)
    

Exemple : Voir le TP1 et la définition inductive des opérateurs logiques, avec deux versions, l'une paramétrée, l'autre indexée. Une preuve par inversion est donnée, une autre par tranfert.

3.2 [Ind-D] - Une règle par constructeur

Γ ⊢ x : P    Γ ⊢ Q
------------------ [c]
    Γ ⊢ I p u
> apply c.

Remarque : il peut être nécessaire de préciser certains arguments de c.

4 Tactiques pour le calcul des séquents

Correspondance entre les tactiques et le calcul des séquents.

  • Les tactiques ci-dessous se déduisent facilement des définitions des opérateurs logiques.
    • Vrai (True), Faux (False), disjonction (or, notée \/), et (and, notée /\), quantification existentielle (ex, notée exists x, p) : définitions inductives
  • Non (not, notée ~), implication (->), quantification universelle (forall x, p) : définitions fonctionnelles
  • Pour chaque règle, on donne une tactique telle que si le but courant de Coq est une instance de sa conclusion, alors l'application de la tactique produit ses prémisses comme les nouveaux buts de Coq.
  • Pour certaines règles, des alternatives sont proposées : toute tactique est introduite par un chevron (>), qui ne fait pas partie de la notation des tactiques.

4.1 [Id]

 Γ ⊢ p : Prop  
------------- [Id]
(h :p), Γ ⊢ p
> assumption.
> exact h.
> auto.

4.2 [Coupure]

Γ ⊢ p   (h : p), Γ ⊢ q
---------------------- [Coupure']
       Γ ⊢ q
> assert p as h.

4.3 [F-G]

--------- [F-G]
(h : F) ⊢
> case h as []. (* But vide représenté par False.*)

4.4 [V-D]

---- [V-D]   
⊢ V
> exact I. (* seul constructeur de True. *)
> auto.

4.5 [F-D]

Γ ⊢ 
-------- [F-D]
Γ ⊢ F

Coq représentant le but vide par False, cette règle est inutile.

4.6 [V-G]

    Γ ⊢ p       
-------------- [V-G]
(h : V), Γ ⊢ p
> case h as [].

4.7 [∧-G]

(hg :p), (hd : q), Γ ⊢ q        
------------------------ [∧-G']
   (h : p ∧ q), Γ ⊢ q
> case h as [hg hd].

4.8 [∧-D]

Γ ⊢ p   Γ ⊢ q
------------- [∧-D]   
  Γ ⊢ p ∧ q
> split.  
> apply conj. (* constructeur de and. *)

4.9 [∨-G]

(hg : p), Γ ⊢ r   (hd : q), Γ ⊢ r      
--------------------------------- [∨-G]
       (h : p ∨ q), Γ ⊢ r
> case h as [hg | hd].

4.10 [∨-Dg]

Γ ⊢ p   Γ ⊢ q : Prop
-------------------- [∨-Dg]   
     Γ ⊢ p ∨ q
> left.
> apply or_introl. (* premier constructeur de or. *)

4.11 [∨-Dd]

Γ ⊢ q   Γ ⊢ p : Prop
-------------------- [∨-Dg]   
     Γ ⊢ p ∨ q
> right.
> apply or_intror. (* second constructeur de or. *)

4.12 [¬-G]

     Γ ⊢ p         
--------------- [¬-G]
 (h : ¬p), Γ ⊢
> apply h. (* but vide = False ; négation (not p) (notée ~p) définie par (p -> False). *)
  clear h. (* pour effacer h des hypothèses ; facultatif. *)

4.13 [¬-D]

(h : p), Γ ⊢ 
------------ [¬-D]   
   Γ ⊢ ¬p
> intro h.

4.14 [->-G]

Γ1 ⊢ p   (h : q), Γ2 ⊢ r         
------------------------ [->-G]  
(i : p -> q), Γ1, Γ2 ⊢ r
>   assert q as h; (apply i || idtac). (* première prémisse || seconde prémisse 
                                          apply i -> but p     idtac -> but r   *)

4.15 [->-D]

(h : p), Γ ⊢ q
-------------- [->-D]
  Γ ⊢ p -> q
> intro h.

4.16 [∀-G]

(h : p[x := t]), Γ ⊢ q   Γ ⊢ t : T       
---------------------------------- [∀-G] 
    (h : ∀(x : T). p), Γ ⊢ q
> specialize h with t; intro ht.

4.17 [∀-D]

(x : T), Γ ⊢ p   Γ ⊢ Γ : Prop* 
------------------------------ [∀-D]
       Γ ⊢ ∀(x : T). p
> intro x.

4.18 [∃-G]

(x : T), (hp : p), Γ ⊢ q   Γ ⊢ q, Γ : Prop*     
------------------------------------------- [∃-G]
	 (h : ∃(x : T). p), Γ ⊢ q
> case h as [x hp].

4.19 [∃-D]

Γ ⊢ p[x := t]    Γ ⊢ t : T 
-------------------------- [∃-D]   
      Γ ⊢ ∃(x : T). p
> exists t.
> apply (ex_intro _ t). (* unique constructeur de (ex P), noté (exists x, P x). *)

4.20 [A-G] (affaiblissement)

Γ ⊢ q   Γ ⊢ p : Prop        
-------------------- [A-G]  
   (h :p), Γ ⊢ q
> clear h.

4.21 [A-D] (affaiblissement)

Γ ⊢    Γ ⊢ p : Prop 
------------------- [A-D]   
     Γ ⊢ p
> exfalso. (* False correspondant à un but vide *)

4.22 [C-G] (contraction)

(h : p), (k : p), Γ ⊢ q               
----------------------- [C-G]         
    (h : p), Γ ⊢ q
>   assert p as k ; [ exact h | idtac]. (* première prémisse || seconde prémisse 
                                           exact h -> qed       idtac -> but q   *)

4.23 [P-G] (permutation)

   Γ ⊢ q                     
------------ [P-G] (σ : permutation)        
  Γ[σ] ⊢ q

Par défaut, l'ordre des hypothèses n'importe pas. On y accède par leurs noms.

5 Complément : Wiki/Faq de Coq

Author: Hervé Grall
Version history: v1: 2020-01-20.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.