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 - Modules et Types Abstraits

Auteurs:

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

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

Supports de ce cours :

Modules en Coq et application aux TAD

1. Spécification de modules (types de modules)

Déclaration d’identificateurs.

On distingue :

  • des identificateurs de types

  • des identificateurs de constantes ou d’opérations

  • des identificateurs de propriétés (axiomes)

Exemple

Module Type Monoide.
  Parameter T : Type.           (* une sorte *)
  Parameter un : T.             (* une constante *)
  Parameter prod : T -> T -> T. (* une opération *)

  Axiom assoc :
    forall x y z : T, prod x (prod y z) = prod (prod x y) z.
  Axiom neutre_g : forall x, prod un x = x.
  Axiom neutre_d : forall x, prod x un = x.
End Monoide.

2. Modules réalisant une spécification

Définition des identificateurs déclarés dans la spécification

Implantations possibles du monoide :

  • entiers avec \(0\) et \(+\)

  • entiers avec \(1\) et \(*\)

  • listes avec concaténation

  • type singleton

  • …

2. Modules réalisant une spécification

Exemple : monoide des listes avec concaténation

Require Import List. Import ListNotations.
Set Implicit Arguments.

Module MonoList <: Monoide. (* vérification sans masquage *)
  Definition T := list nat.
  Definition un : T := [].
  Definition prod (x y : T) := x ++ y.

  
forall x y z : T,
prod x (prod y z) = prod (prod x y) z

  
forall x y z : T,
prod x (prod y z) = prod (prod x y) z
 apply app_assoc. Qed.

  
forall x : T, prod un x = x

  
forall x : T, prod un x = x
 reflexivity. Qed.

  
forall x : T, prod x un = x

  
forall x : T, prod x un = x
 
a: nat
x: list nat
IHx: prod x un = x
prod (a :: x) un = a :: x
 
a: nat
x: list nat
IHx: prod x un = x
a :: prod x un = a :: x
 
a: nat
x: list nat
IHx: prod x un = x
a :: x = a :: x
 reflexivity. Qed.
End MonoList.

3. Utilisation indépendante de l’implantation (foncteur)

Exemple : unicité de l’élément neutre

Module Use(M : Monoide).
  
forall u : M.T,
(forall x : M.T, M.prod x u = x) -> u = M.un

  
forall u : M.T,
(forall x : M.T, M.prod x u = x) -> u = M.un

  
u: M.T
Hu: forall x : M.T, M.prod x u = x
u = M.un

  
u: M.T
Hu: forall x : M.T, M.prod x u = x
u = M.prod M.un u

  
u: M.T
Hu: forall x : M.T, M.prod x u = x
u = u

  reflexivity.
  Qed.
End Use.

4. Instantiation du foncteur (a.k.a. module paramétré)

Exemple

Module Inst := Use(MonoList).
  
Inst.unicite
     : forall u : MonoList.T,
       (forall x : MonoList.T, MonoList.prod x u = x) ->
       u = MonoList.un


  
MonoList.un = []
     : MonoList.T

  
MonoList.T = list nat
     : Set

Exemple autour de la structure de pile

Signature d’un TAD Pile

Ecrire la spécification du type abstrait tPile introduisant un type Elem, un type P, et les opérations habituelles sur les piles. On essaiera d’étendre au maximum le domaine des fonctions partielles (par ex. en retournant la pile vide), ou si besoin en utilisant le type option :

Inductive option {T : Type} := None | Some (valeur : T).

Module Type Pile.
  Parameter Elem : Type.
  Parameter P : Type.
  Parameter vide : P.
  Parameter push : Elem -> P -> P.
  Parameter estVide : P -> bool.
  Parameter top : P -> @option Elem.
  Parameter pop : P -> P.
  (* et pas "P -> option P" :
   * choix de conception pour simplifier les preuves *)

  Axiom estVide_vide : estVide vide = true.
  Axiom estVide_push : forall p e, estVide (push e p) = false.
  Axiom top_vide : top vide = None.
  Axiom top_push : forall p e, top (push e p) = Some e.
  Axiom pop_vide : pop vide = vide.
  Axiom pop_push : forall p e, pop (push e p) = p.
End Pile.

Implémentation du TAD Pile

Implémentez un TAD Pile d’entiers naturels, en vous appuyant sur la bibliothèque des listes.

Module Pile_Liste <: Pile.
  Definition Elem := nat.
  Definition P := list nat.
  Definition vide : P := [].
  Definition push (e : Elem) (p : P) := e :: p.
  Definition estVide (p : P) :=
    match p with [] => true | _ => false end.
  Definition top (p : P) :=
    match p with [] => None | x :: _ => Some x end.
  Definition pop (p : P) :=
    match p with [] => [] | _ :: l => l end.

  
estVide vide = true

  
estVide vide = true
 reflexivity. Qed.

  
forall (p : P) (e : Elem), estVide (push e p) = false

  
forall (p : P) (e : Elem), estVide (push e p) = false
 
p: P
e: Elem
estVide (push e p) = false
 reflexivity. Qed.

  
top vide = None

  
top vide = None
 reflexivity. Qed.

  
forall (p : P) (e : Elem), top (push e p) = Some e

  
forall (p : P) (e : Elem), top (push e p) = Some e
 
p: P
e: Elem
top (push e p) = Some e
 reflexivity. Qed.

  
pop vide = vide

  
pop vide = vide
 reflexivity. Qed.

  
forall (p : P) (e : Elem), pop (push e p) = p

  
forall (p : P) (e : Elem), pop (push e p) = p
 
p: P
e: Elem
pop (push e p) = p
 reflexivity. Qed.
End Pile_Liste.

Autre exemple d’implémentation

Peut-on implémenter le même TAD avec des listes, mais en empilant et dépilant en queue ?

Module Pile_QListe <: Pile.
  Definition Elem := nat.
  Definition P := list nat.
  Definition vide : P := [].
  Definition push (e : Elem) (p : P) := p ++ [e].
  Definition estVide (p : P) :=
    match p with [] => true | _ => false end.
  Fixpoint top (p : P) :=
    match p with [] => None | [e] => Some e | x:: l => top l end.
  Fixpoint pop (p : P) :=
    match p with [] => [] | [e] => [] | x :: l => x :: pop l end.

  
estVide vide = true

  
estVide vide = true
 reflexivity. Qed.

  
forall (p : P) (e : Elem), estVide (push e p) = false

  
forall (p : P) (e : Elem), estVide (push e p) = false
 induction p; simpl; auto. Qed.

  
top vide = None

  
top vide = None
 reflexivity. Qed.

  
forall (p : P) (e : Elem), top (push e p) = Some e

  
forall (p : P) (e : Elem), top (push e p) = Some e
 induction p; auto; destruct p; auto. Qed.

  
pop vide = vide

  
pop vide = vide
 reflexivity. Qed.

  
forall (p : P) (e : Elem), pop (push e p) = p

  
forall (p : P) (e : Elem), pop (push e p) = p

  
a: nat
p: list nat
IHp: forall e : Elem, pop (push e p) = p
forall e : Elem, pop (push e (a :: p)) = a :: p

  
a, n: nat
p: list nat
IHp: forall e : Elem, pop (push e (n :: p)) = n :: p
forall e : Elem,
pop (push e (a :: n :: p)) = a :: n :: p

  intros e; rewrite <-(IHp e) at 2; auto.
  Qed.
End Pile_QListe.