Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.1. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.

TAPFA - Partie Coq - Preuve assistée

Auteurs:

Jean-Paul Bodeveix (resp. UE), Erik Martin-Dorel, Pierre Roux

Date:
L3 Info, Semestre 6, Année 2021-2022

Supports de ce cours :

Principe

  • Prouver une propriété P \(\equiv\) Construire un terme de type P.

Parameters (p : Prop) (q : Prop).


p -> (p -> q) -> q

p -> (p -> q) -> q
exact (fun (x : p) (f : p -> q) => f x). Qed.
  • Les tactiques aident à la construction du terme de preuve:


p -> (p -> q) -> q

p -> (p -> q) -> q
auto. Qed.
th' = fun (H : p) (H0 : p -> q) => H0 H : p -> (p -> q) -> q Arguments th' _ _%function_scope

Les principales tactiques de preuve

La tactique intro (variante : intros H_1 H_n)

h_1 : e_1                       h_1 : e_1
   ...        --> intro H -->      ...
h_n : e_n                       h_n : e_n
=========                       H : p
p -> q                          =========
                                q


h_1 : e_1                       h_1 : e_1
   ...        --> intro x -->      ...
h_n : e_n                       h_n : e_n
============                    x : t
 x : t, P x                    =========
                                P x

Cas d’utilisation de intro

Lorsque le but est une implication ou une quantification universelle \(\leadsto\) introduction de l’hypothèse dans le contexte

Preuve d’une égalité

Γ        --> reflexivity -->    si t = t'
======
t = t'

Cas d’utilisation de reflexivity

Lorsque le but est une égalité entre 2 termes identiques (modulo calcul) \(\leadsto\) fin de la preuve.

Exemple

Γ          --> reflexivity -->    (Qed)
=========
1 + 1 = 2

Réécriture (utilisation d’une égalité)

Soit E : t1 = t2 un théorème ou une hypothèse du contexte \(\Gamma\)

Γ     --> rewrite E -->   Γ
====                      ====
P t1                      P t2


Γ     --> rewrite <-E -->   Γ
====                        ====
P t2                        P t1


Γ                                   Γ
H : P t1   --> rewrite E in H -->   H : P t2
========                            ========
G                                   G


Γ                                     Γ
H : P t2   --> rewrite <-E in H -->   H : P t1
========                              ========
G                                     G

Réécriture (exemple)


forall f : nat -> nat, (forall n : nat, f n = f (S n)) -> f 2 = f 0

forall f : nat -> nat, (forall n : nat, f n = f (S n)) -> f 2 = f 0
f: nat -> nat

(forall n : nat, f n = f (S n)) -> f 2 = f 0
f: nat -> nat
H: forall n : nat, f n = f (S n)

f 2 = f 0
f: nat -> nat
H: forall n : nat, f n = f (S n)

f 1 = f 0
f: nat -> nat
H: forall n : nat, f n = f (S n)

f 0 = f 0
reflexivity. Qed.

Réécriture (cas général où le théorème E a des conditions)

Soit E : x1 ... xk, p1 x1 ... xk -> ⋅⋅⋅ -> pn x1 ... xk -> t x1 ... xk = t' x1 ... xk, un théorème ou une hypothèse du contexte \(\Gamma\)

Γ                 --> rewrite E -->   Γ
===============                       ================
P (t u1 ... uk)                       P (t' u1 ... uk)

                                      Γ
                                      ============
                                      p1 u1 ... uk

                                      ...

                                      Γ
                                      ============
                                      pn u1 ... uk

                                      (* n conditions requises par le théorème E *)

Réécriture (exemple avec une condition)

pred : nat -> nat                             pred : nat -> nat
E :  x : nat, O < x ->                       E :  x : nat, O < x ->
    S (pred x) = x                                S (pred x) = x
n : nat                   --> rewrite E -->   n : nat
=======================                       =======================
S (pred (2 * (n + 1)))                        2 * (n + 1) = 2 * n + 2
= 2 * n + 2
                                              pred : nat -> nat
                                              E :  x : nat, O < x ->
                                                  S (pred x) = x
                                              n : nat
                                              ===============
                                              O < 2 * (n + 1)

La tactique apply (variante : apply H with (x_i:=v_i) …)

Soit H : x1 ... xk, p1 x1 ... xk -> ⋅⋅⋅ -> pn x1 ... xk -> q x1 ... xk, un théorème ou une hypothèse du contexte \(\Gamma\)

Γ             --> apply H -->   Γ
===========                     ============
q u1 ... uk                     p1 u1 ... uk

                                ...

                                Γ
                                ============
                                pn u1 ... uk

                                (* n conditions requises pour appliquer H *)

La tactique apply (exemple)

le_S: forall n m : nat, n <= m -> n <= S m
le_n_S: forall n m : nat, n <= m -> S n <= S m
le_S_n: forall n m : nat, S n <= S m -> n <= m

(documentation de la commande Search)


forall n : nat, n <= S (S n)

forall n : nat, n <= S (S n)
n: nat

n <= S (S n)
le_S : forall n m : nat, n <= m -> n <= S m
n: nat

n <= S (S n)
n: nat

n <= S n
Abort.

La tactique induction : applique le théorème d’induction


forall n m : nat, n + m = m + n

forall n m : nat, n + m = m + n

forall m : nat, 0 + m = m + 0
n: nat
IHn: forall m : nat, n + m = m + n
forall m : nat, S n + m = m + S n
Abort.

La tactique destruct : preuve par cas


forall n : nat, n + 1 <> 0

forall n : nat, n + 1 <> 0

0 + 1 <> 0
n: nat
S n + 1 <> 0

La tactique simpl : simplification du but


1 <> 0
n: nat
S n + 1 <> 0
Abort.

Détail : réduction des expressions 0+n, 1+n, n+0, n+1

Étant donnée que la fonction (fun a b : nat => a + b) est définie récursivement par rapport à son premier argument :

  • 0 + n se réduit par calcul à n

  • 1 + n se réduit par calcul à S n

  • \(\leadsto\) donc on peut prouver trivialement 1 + n = S n (par réflexivité)

  • mais on a besoin d’une preuve par induction pour montrer que

     n : nat, n + 0 = n
     n : nat, n + 1 = S n

Autres tactiques non détaillées dans ces transparents :

  • exact

  • symmetry, transitivity

  • constructor, split, left, right, exists, discriminate, injection

  • unfold

  • lia (Linear Integer Arithmetic), tauto, firstorder

Pour plus de détails, voir l’Aide-mémoire des tactiques de preuve Coq

Retour sur la correspondance "preuve-programme" (Curry-Howard)

Coq fournit un langage de tactiques qui permet de construire interactivement et incrémentalement, un programme fonctionnel (le "terme de preuve"). Lorsque la construction de ce programme est terminée, son type est vérifié par Coq au moment du Qed par rapport au type attendu (c.-à-d. par rapport à la formule logique qui devait être démontrée).

L'exemple qui suit, qui peut être joué dans la dernière version de ProofGeneral en activant deux fonctionnalités spécifiques dans l'IDE, illustre ce principe :

  • Menu Coq > Show Proof (M-x coq-show-proof-stepwise-toggle RET)

  • Menu Coq > Diffs > On (ESC ` c D O)

(en utilisant aussi si besoin, le menu Coq > Toggle 3 Windows mode ainsi que le raccourci C-c C-l C-c C-p)


forall A B C : Prop, (A -> B -> C) -> A /\ B -> C

forall A B C : Prop, (A -> B -> C) -> A /\ B -> C
A, B, C: Prop

(A -> B -> C) -> A /\ B -> C
A, B, C: Prop
hABC: A -> B -> C

A /\ B -> C
A, B, C: Prop
hABC: A -> B -> C
hAB: A /\ B

C
A, B, C: Prop
hABC: A -> B -> C
H: A
H0: B

C
apply hABC; auto. Qed.

Exemples et exercices autour des listes

Préliminaires

Pour charger la bibliothèque des listes (et les notations à la OCaml) puis activer les arguments implicites pour vos définitions, ajoutez au début de votre fichier :

Require Import List.
Import ListNotations.
Set Implicit Arguments.

Quelques preuves (de théorèmes de la stdlib) sur les listes

But Prouver que la double inversion d’une liste renvoie la liste inchangée :

 T (l : list T), rev (rev l) = l

La fonction List.rev est définie comme suit :

Fixpoint rev (T : Type) (l : list T) :=
  match l with
  | [] => []
  | x :: l => rev l ++ [x]
  end.

++ est une notation Coq qui équivaut à @ en OCaml.

Méthode On part du théorème à prouver et on identifie au fur et à mesure les lemmes intermédiaires qui méritent d’être prouvés à part.

Premier lemme

Prouver (par induction sur la liste l1) que l’on a :

Lemma app_nil : forall (T : Type) (l : list T), l = l ++ [].

Rappel: la fonction (fun l1 l2 => l1 ++ l2) est définie comme suit :

Fixpoint app (T : Type) (l1 l2 : list T) :=
  match l1 with
  | [] => l2
  | x1 :: l1 => x1 :: app l1 l2
  end.

Sauriez vous l'écrire en OCaml ?

Premier lemme – preuve par induction

À la main :

Prouvons le lemme app_nil par induction structurelle sur la liste l.

  • Cas de base (si l est la liste vide []). On doit montrer que [] = [] ++ [], soit, après simplification de la définition de app, [] = []. CQFD.

  • Cas inductif (si l est de la forme x :: l'). Fixons un x : T et un l' : list T, supposons que l' = l' ++ [] et appelons cette hypothèse d'induction IHl. Montrons qu'alors x :: l' = (x :: l') ++ []. En simplifiant la définition de app on doit donc prouver que x :: l' = x :: (l' ++ []), soit après avoir utilisé IHl, que x :: l' = x :: l'. CQFD.

Premier lemme – preuve par induction (version Coq)


forall (T : Type) (l : list T), l = l ++ []

forall (T : Type) (l : list T), l = l ++ []
T: Type

[] = [] ++ []
T: Type
a: T
l: list T
IHl: l = l ++ []
a :: l = (a :: l) ++ []
T: Type

[] = [] ++ []
T: Type

[] = []
reflexivity.
T: Type
a: T
l: list T
IHl: l = l ++ []

a :: l = (a :: l) ++ []
T: Type
a: T
l: list T
IHl: l = l ++ []

a :: l = a :: l ++ []
T: Type
a: T
l: list T
IHl: l = l ++ []

a :: l = a :: l
reflexivity. Qed.

Pour appliquer simpl à chaque sous-but généré il suffit d’écrire la tactique une fois après ";"


forall (T : Type) (l : list T), l = l ++ []

forall (T : Type) (l : list T), l = l ++ []
T: Type

[] = []
T: Type
a: T
l: list T
IHl: l = l ++ []
a :: l = a :: l ++ []
T: Type

[] = []
reflexivity.
T: Type
a: T
l: list T
IHl: l = l ++ []

a :: l = a :: l ++ []
T: Type
a: T
l: list T
IHl: l = l ++ []

a :: l = a :: l
reflexivity. Qed.

Deuxième lemme


forall (T : Type) (l1 l2 l3 : list T), l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3

forall (T : Type) (l1 l2 l3 : list T), l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3
T: Type
a: T
l1: list T
IHl1: forall l2 l3 : list T, l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3
l2, l3: list T

a :: l1 ++ l2 ++ l3 = a :: (l1 ++ l2) ++ l3
T: Type
a: T
l1: list T
IHl1: forall l2 l3 : list T, l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3
l2, l3: list T

a :: (l1 ++ l2) ++ l3 = a :: (l1 ++ l2) ++ l3
reflexivity. Qed.

auto essaie d’appliquer récursivement les hypothèses (et certains lemmes standard, comme la réflexivité) pour prouver le sous-but ; sinon la tactique ne fait rien.

Troisième lemme


forall (T : Type) (l1 l2 : list T), rev (l1 ++ l2) = rev l2 ++ rev l1

forall (T : Type) (l1 l2 : list T), rev (l1 ++ l2) = rev l2 ++ rev l1
T: Type
l2: list T

rev l2 = rev l2 ++ []
T: Type
a: T
l1: list T
IHl1: forall l2 : list T, rev (l1 ++ l2) = rev l2 ++ rev l1
l2: list T
rev (l1 ++ l2) ++ [a] = rev l2 ++ rev l1 ++ [a]
T: Type
a: T
l1: list T
IHl1: forall l2 : list T, rev (l1 ++ l2) = rev l2 ++ rev l1
l2: list T

rev (l1 ++ l2) ++ [a] = rev l2 ++ rev l1 ++ [a]
T: Type
a: T
l1: list T
IHl1: forall l2 : list T, rev (l1 ++ l2) = rev l2 ++ rev l1
l2: list T

(rev l2 ++ rev l1) ++ [a] = rev l2 ++ rev l1 ++ [a]
T: Type
a: T
l1: list T
IHl1: forall l2 : list T, rev (l1 ++ l2) = rev l2 ++ rev l1
l2: list T

(rev l2 ++ rev l1) ++ [a] = (rev l2 ++ rev l1) ++ [a]
reflexivity. Qed.

Le théorème visé


forall (T : Type) (l : list T), rev (rev l) = l

forall (T : Type) (l : list T), rev (rev l) = l
(* exercice ! *) (* Qed. *)