UP | HOME

Coq - Un aide-mémoire

Table of Contents

1 Commandes

  • Show Match T : montre les cas du filtrage pour le type inductif T.
  • Print x : affiche la valeur de l'identifiant x.
  • Check t : affiche le type du terme t.
  • Locate "n" : donne la définition de la notation n.

2 Notations

ordre sur les nat

  • <=

listes

  • [] : liste vide
  • [x] : singleton x
  • [x1 ; … ; xn] : liste x1, …, xn
  • r* : liste de tête t et de reste r (soit cons t r)
  • k ++ l : concaténation des listes k et l

logique - négation

  • ~ X := (not X) = (X -> False)

3 Tactiques

Séquent en Coq (interface classique)

(* hypothèses *) 
h1 : H1
h2 : H2
...
============================
B (* but *)

Représentation du séquent : (h1: : H1),(h2 : H2), … ⊢ B

Une tactique transforme un but (qui est un séquent) en plusieurs sous-buts, des séquents. Son effet peut donc se traduire par une règle d'inférence.

(H_i ⊢ B_i)_i
-------------
   H ⊢ B

La tactique correspond alors au passage du séquent H ⊢ B aux séquents H_i ⊢ B_i. Des règles courantes sont décrites ci-dessous, accompagnées de leurs tactiques. Les règles sont classées en grandes catégories et divisées en règles à gauche et en règles à droite, qui s'appliquent dans le séquent à gauche ou à droite respectivement.

Axiome de l'identité - Preuve par hypothèse

  • assumption
  • exact
  • auto (plus général)

Types fonctionnels

  • intro, intros
  • apply, apply with, exact

Types inductifs

  • apply, apply with, exact, constructor
  • case, destruct, inversion, induction

Egalité

  • reflexivity, ring, f_equal
  • rewrite, rewrite <-

Logique

  • split
  • left
  • right
  • exists
  • case

Simplifications des calculs

  • simpl

3.1 Axiome de l'identité - Preuve par hypothèse p ⊢ p

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

3.2 Types fonctionnels - et ->

3.2.1 ⊢ p -> q ou ⊢ ∀x.p

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

Il est possible d'introduire plusieurs hypothèses successivement avec intros.

3.2.2 p -> q ⊢ ou ∀x.p ⊢

(type fonctionnel produisant p) q ::= p (but paramétré) 
				    | ∀(x : T).q (quantification universelle)
				    | r -> q (r antécédent de p) 
(substitution) σ := 0 | (x := t).σ (vide | instanciation de x par t) 

(h : q, Γ ⊢ r[σ])*          une prémisse par antécédent de p
------------------ [∀-G]    --------------------------------
 h : q, Γ ⊢ p[σ]            but p instancié
> apply h.
> apply (h t1 ... tn). (* application partielle, avec une instanciation pour les 
                          variables ne pouvant être inférées.  *)
> exact (h t1 ... tn). (* application complète *)
> apply h with s1 ... sm. (* application partielle avec instanciation 
                             des variables n'apparaissant que dans les prémisses. *)
> apply (h t1 ... tn) with s1 ... sm. (* combinaison des deux formes d'applications partielles *)

Dans une application, un terme peut être remplacé par _ si sa valeur peut être inférée.

3.3 Types inductifs - Inductive Ind

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 = Ind ...)
-------------------     ----------------------------------
(c p x z) : Ind 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 Ind 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 Ind p : (* paramétrisation par p *)
  forall w, S (* indexation par w, S ::= Prop | Type *) 
:=
| c : forall x : P, forall z : Q, Ind p u (* u : instanciation de w *)
| ... (* autres constructeurs *)
.

3.3.1 ⊢ Ind …

Γ ⊢ x : P    Γ ⊢ Q
------------------ [c]
    Γ ⊢ Ind p u
> apply c.
> apply (c t1 ... tn). (* application partielle, avec une instanciation pour les 
                          variables ne pouvant être inférées.  *)
> exact (c t1 ... tn). (* application complète *)
> apply c with s1 ... sm. (* application partielle avec instanciation 
                             des variables n'apparaissant que dans les prémisses. *)
> apply (c t1 ... tn) with s1 ... sm. (* combinaison des deux formes d'applications partielles *)
> constructor. (* équivalent à apply c pour un constructeur inféré par Coq. *)

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

3.3.2 Ind … ⊢ - Sans induction

Règle ayant une prémisse par constructeur

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

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

3.3.3 Ind … ⊢ - Avec induction

Règle ayant une prémisse par constructeur

((x : P), (z : Q), HR : A[(h : I p v) := (z : Q)], Γ ⊢ A[h := c p x z, v := u])_c    
---------------------------------------------------------------------------------
		      (h : I p v), Γ ⊢ A
> induction h as [x z HR | ...]. (* une décomposition par règle *)

3.4 Egalité - =

3.4.1 Egalité par identité - ⊢ t = t

---------- [=-D]
Γ ⊢ t = t
> reflexivity.
> apply eq_refl. (* constructeur du type inductif eq, noté =. *)

3.4.2 Egalité d'expressions arithmétiques - Arith ⊢ t = t

La tactique ring est plus puissante que reflexivity". Elle permet de montrer des égalités évidentes entre expressions arithmétiques, précisément des égalités reposant sur les propriétés suivantes des entiers naturels mais plus généralement de toute structure algébrique ayant les propriétés suivantes :

  • commutativité et associativité de l'addition et de la multiplication,
  • distributivité de la multiplication sur l'addition.

C'est le cas des entiers naturels, plus généralement de tout semi-anneau ou anneau.

t ::= c | t + t | t * t

---------- [=-D]
Γ ⊢ t = t
> ring.

3.4.3 Egalité fonctionnelle - ⊢ (f s) = (g t)

Γ ⊢ f = g      (Γ ⊢ si = ti)_i
------------------------------ [=-D]
Γ ⊢ f s1 ... sn  = g t1 ... tn
> f_equal. (* Coq résout automatiquement les sous-buts par réflexivité ou par une tactique 
              plus puissante, congruence, et applique récursivement la décomposition. *)

3.4.4 Récriture - t1 = t2 ⊢

(h : t1 = t2), Γ ⊢ p[t1 := t2]
------------------------------ [=-G]
    (h : t1 = t2), Γ ⊢ p
> rewrite h.
(h : t1 = t2), Γ ⊢ p[t2 := t1]
------------------------------ [=-G]
    (h : t1 = t2), Γ ⊢ p
> rewrite <- h.

3.5 Logique

3.5.1 ⊢ p ∧ q

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

3.5.2 p ∧ q ⊢

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

3.5.3 ⊢ p ∨ q

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

3.5.4 p ∨ q ⊢

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

3.5.5 ⊢ ∃x.p

Γ ⊢ 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). *)

3.5.6 ∃x.p ⊢

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

3.6 Simplification des calculs

La tactique simpl permet de simplifier le but par calcul.

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