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 typeP
.
Parameters (p : Prop) (q : Prop).p -> (p -> q) -> qexact (fun (x : p) (f : p -> q) => f x). Qed.p -> (p -> q) -> q
Les tactiques aident à la construction du terme de preuve:
p -> (p -> q) -> qauto. Qed.p -> (p -> q) -> q
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 0forall f : nat -> nat, (forall n : nat, f n = f (S n)) -> f 2 = f 0f: nat -> nat(forall n : nat, f n = f (S n)) -> f 2 = f 0f: nat -> nat
H: forall n : nat, f n = f (S n)f 2 = f 0f: nat -> nat
H: forall n : nat, f n = f (S n)f 1 = f 0reflexivity. Qed.f: nat -> nat
H: forall n : nat, f n = f (S n)f 0 = f 0
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)
(documentation de la commande Search)
forall n : nat, n <= S (S n)forall n : nat, n <= S (S n)n: natn <= S (S n)n: natn <= S (S n)Abort.n: natn <= S n
La tactique induction
: applique le théorème d’induction
forall n m : nat, n + m = m + nforall n m : nat, n + m = m + nAbort.forall m : nat, 0 + m = m + 0n: nat
IHn: forall m : nat, n + m = m + nforall m : nat, S n + m = m + S n
La tactique destruct
: preuve par cas
forall n : nat, n + 1 <> 0forall n : nat, n + 1 <> 00 + 1 <> 0n: natS n + 1 <> 0
La tactique simpl
: simplification du but
Abort.1 <> 0n: natS n + 1 <> 0
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 -> Cforall A B C : Prop, (A -> B -> C) -> A /\ B -> CA, B, C: Prop(A -> B -> C) -> A /\ B -> CA, B, C: Prop
hABC: A -> B -> CA /\ B -> CA, B, C: Prop
hABC: A -> B -> C
hAB: A /\ BCapply hABC; auto. Qed.A, B, C: Prop
hABC: A -> B -> C
H: A
H0: BC
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.
où ++
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 deapp
,[] = []
. CQFD.Cas inductif (si
l
est de la formex :: l'
). Fixons unx : T
et unl' : list T
, supposons quel' = l' ++ []
et appelons cette hypothèse d'inductionIHl
. Montrons qu'alorsx :: l' = (x :: l') ++ []
. En simplifiant la définition deapp
on doit donc prouver quex :: l' = x :: (l' ++ [])
, soit après avoir utiliséIHl
, quex :: 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[] = [] ++ []reflexivity.T: Type[] = []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.T: Type
a: T
l: list T
IHl: l = l ++ []a :: l = a :: l
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 ++ []reflexivity.T: Type[] = []T: Type
a: T
l: list T
IHl: l = l ++ []a :: l = a :: l ++ []reflexivity. Qed.T: Type
a: T
l: list T
IHl: l = l ++ []a :: l = a :: l
Deuxième lemme
forall (T : Type) (l1 l2 l3 : list T), l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3forall (T : Type) (l1 l2 l3 : list T), l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3T: Type
a: T
l1: list T
IHl1: forall l2 l3 : list T, l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3
l2, l3: list Ta :: l1 ++ l2 ++ l3 = a :: (l1 ++ l2) ++ l3reflexivity. Qed.T: Type
a: T
l1: list T
IHl1: forall l2 l3 : list T, l1 ++ l2 ++ l3 = (l1 ++ l2) ++ l3
l2, l3: list Ta :: (l1 ++ l2) ++ l3 = a :: (l1 ++ l2) ++ l3
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 l1forall (T : Type) (l1 l2 : list T), rev (l1 ++ l2) = rev l2 ++ rev l1T: Type
l2: list Trev l2 = rev l2 ++ []T: Type
a: T
l1: list T
IHl1: forall l2 : list T, rev (l1 ++ l2) = rev l2 ++ rev l1
l2: list Trev (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 Trev (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]reflexivity. Qed.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]
Le théorème visé
forall (T : Type) (l : list T), rev (rev l) = l(* exercice ! *) (* Qed. *)forall (T : Type) (l : list T), rev (rev l) = l