UP | HOME

Evaluation - Exercices de programmation et de démonstration avec Coq

Table of Contents

1 Consignes

  • Durée de l'évaluation : 1h30' environ
  • Outil : Coq (version 8.10)

Organisation du travail et rendu

  • Récupérer le fichier eval_sujet.v et le renommer en eval_X_Y.v, où X est votre nom, Y votre prénom (sans accents).
  • Compléter le fichier.
  • Déposer sur Moodle le fichier complété.

Remarques

2 Les suites arithmétiques

On cherche à démontrer la formule donnant la somme des premiers termes d'une suite arithmétique.

2.1 Définition et propriétés des suites arithmétiques

Une suite arithmétique \((U_n)_n\) de raison \(r\) est définie par la relation de récurrence suivante.

\begin{array}{rcl} U_0 & = & 0 \\ U_{n+1} & = & r + U_n \end{array}

Compléter la fonction récursive suiteArithmetique définissant une suite arithmétique de raison le paramètre raison.

Fixpoint suiteArithmetique(raison : nat) (n : nat) : nat.

Une suite arithmétique est un morphisme pour l'addition.

\begin{array}{rcl} U_{m + n} = U_m + U_n \end{array}

Démontrer le lemme exprimant cette propriété par induction (récurrence) sur m. On utilisera la tactique ring pour montrer toute égalité entre des expressions arithmétiques qui peut se déduire de manipulations élémentaires.

Lemma morphismeAdditif_suiteArithmetique :
  forall raison, forall m n,
      suiteArithmetique raison (m + n)
      = suiteArithmetique raison m + suiteArithmetique raison n.

Il est possible de donner une expression analytique d'une suite arithmétique de raison \(r\).

\begin{array}{rcl} U_{n} = n * r \end{array}

Démontrer cette propriété par induction sur n.

Lemma expressionAnalytique_suiteArithmetique : forall raison n,
    suiteArithmetique raison n = n * raison.

2.2 Formule de la somme

On peut définir récursivement la somme \(\sum_{i = 0}^{n} U_i\) des \(n+1\) premiers termes d'une suite \((U_n)_n\).

\begin{array}{rcl} \sum_{i = 0}^{0} U_i & = & U_0 \\ \sum_{i = 0}^{n+1} U_i & = & U_{n+1} + \sum_{i = 0}^{n} U_i \\ \end{array}

Compléter la fonction récursive sommeSuiteArithmetique définissant la somme des (n+1) premiers termes d'une suite arithmétique de raison le paramètre raison.

Fixpoint sommeSuiteArithmetique(raison : nat)(n : nat) : nat.

Il est possible de donner une expression analytique de cette somme. Voici comment on peut retrouver la formule.

\begin{array}{rclcccccc} \sum_{i = 0}^{n} U_i & & U_{0} & + & \ldots & \ldots & \ldots & + & U_n \\ + & = & + \\ \sum_{i = 0}^{n} U_i & & U_n & + & \ldots & \ldots & \ldots & + & U_0 \\ \\ \sum_{i = 0}^{n} U_i & & 0 * r & + & \ldots & i * r & \ldots & + & n * r \\ + & = & + \\ \sum_{i = 0}^{n} U_i & & n * r & + & \ldots & (n-i) * r & \ldots & + & 0 * r \\ \\ 2 * \sum_{i = 0}^{n} U_i & = & (n * r) & * & (n + 1) \end{array}

Montrer cette égalité par induction sur n. On procédera par récriture en utilisant les lemmes précédents, morphismeAdditif_suiteArithmetique et expressionAnalytique_suiteArithmetique. On utilisera la tactique ring pour montrer toute égalité entre des expressions arithmétiques qui peut se déduire de manipulations élémentaires.

Lemma expressionAnalytique_sommeSuiteArithmetique :
  forall raison n,
    suiteArithmetique 2 (sommeSuiteArithmetique raison n) = n * raison * (S n).

3 Relation d'ordre pour les entiers naturels

3.1 Une définition alternative

La relation d'ordre sur les entiers naturels est définie dans la bibliothèque standard de Coq par un prédicat inductif le ("Less than or Equal to").

(* Définition inductive paramétrée par *n* et indexée par un nat. *)
Inductive le (n : nat) : nat -> Prop :=  
| le_n : le n n 
| le_S : forall m : nat, (le n m) -> (le n (S m)).

Le terme (le m n) est noté plus simplement m <= n. Cette définition correspond au système d'inférence suivant.

		 n <= m
------ [le_n]   -------- [le_S]
n <= n          n <= S m

On peut représenter visuellement les preuves dans ce système d'inférence.

m <= n := ensemble des couples (m, n) au-dessus de la diagonale y = x

y
∧    
|                  (m, n)
|                    +
|                    |
|                    |         y = x 
|                    |         /
|                    |      /
|                    |   /         
|                    |/                 
|                  / (m, m)           
|               / 
|            /  
|         /  
|      /   
|   /    
|/     
+------------------------------------------------> x

Partant du but m <= n, la preuve s'obtient en descendant (n-m) fois suivant la verticale du point (m, n) au point (m, m), par application du constructeur le_S, puis en terminant en (m, m) avec l'application du constructeur le_n.

Notre but est de donner une définition alternative (notée ci-dessous) et de montrer l'équivalence avec celle de la bibliothèque standard. Les preuves dans ce système se construisent d'une manière différente, comme le montre le schéma suivant.

m ≤ n := ensemble des couples (m, n) au-dessus de la diagonale y = x

y
∧    
|                   (m, n)
|                     +
|                   /  
|                /             y = x 
|             /                /
|          /                /
|       /                /         
|    /                / 
| /                /
| (0, n-m)       /                                                              
|             /  
|          /                    
|       /             
|    /                       
| /                          
+------------------------------------------------> x

Partant du but m ≤ n, la preuve dans le nouveau système s'obtient en descendant m fois suivant la diagonale du point (m, n) au point (0, n - m), par application du constructeur successeurCroissant, puis en terminant en (0, n-m) avec l'application du constructeur zeroMin. Voici le système d'inférence associé.

		      m ≤ n
------ [zeroMin]    --------- [successeurCroissant]
0 ≤ n               S m ≤ S n

Compléter la définition inductive suivante, de manière à réaliser ce système d'inférence alternatif. Nous n'utilisons pas de notation particulière pour ce prédicat dans le script.

Inductive InferieurOuEgal : nat -> nat -> Prop :=
| zeroMin : ...
| successeurCroissant : ... .

3.2 Adéquation de la nouvelle définition

On cherche à montrer l'adéquation de la nouvelle définition, soit l'inclusion du nouvel ordre dans l'ordre standard <=. Il suffit de montrer la stabilité de <= pour les deux règles [zeroMin] et [successeurCroissant].

		      m <= n
------ [zeroMin']    ---------- [successeurCroissant']
0 <= n              S m <= S n

Montrer le lemme de stabilité pour la règle [zeroMin], par induction sur n.

Lemma zeroMin_le :
  forall n, 0 <= n.

Montrer le lemme de stabilité pour la règle [successeurCroissant], par induction sur la preuve de m <= n.

Lemma successeurCroissant_le :
  forall m n, m <= n -> S m <= S n.

Conclure en montrant l'inclusion de dans <=, par induction sur la preuve de m ≤ n.

Lemma equivalenceNouveauStandard_InferieurOuEgal :
  forall m n, (InferieurOuEgal m n) -> (m <= n).

3.3 Complétude de la nouvelle définition

On cherche à montrer la complétude de la nouvelle définition, soit l'inclusion de l'ordre standard <= dans le nouvel ordre . Il suffit de montrer la stabilité de pour les deux règles [le_n] et [le_S].

		  n ≤ m
------ [le_n']   ------- [le_S']
n ≤ n            n ≤ S m

Montrer le lemme de stabilité pour la règle [le_n], par induction sur n.

Lemma reflexivite_InferieurOuEgal :
  forall n, InferieurOuEgal n n.

Montrer le lemme de stabilité pour la règle [le_S], par induction sur la preuve de m ≤ n.

Lemma descenteVerticale_InferieurOuEgal :
  forall m n : nat, InferieurOuEgal m n -> InferieurOuEgal m (S n).

Conclure en montrant l'inclusion de <= dans , par induction sur la preuve de m <= n.

Lemma equivalenceStandardNouveau_InferieurOuEgal :
  forall m n, (m <= n) -> (InferieurOuEgal m n).

Adéquate et complète, la nouvelle définition est équivalente à celle standard. Noter que le raisonnement par stabilité est tout à fait classique pour montrer l'inclusion d'un type inductif dans un type : il constitue exactement l'argumentation du principe inductif associé au type inductif.

4 Préfixes et facteurs d'une liste

On s'intéresse aux listes sur un type A quelconque. Comme une liste peut être vue comme un mot sur l'alphabet A, il est usuel d'utiliser la terminologie propre aux mots :

  • un préfixe d'une liste l est une liste k commençant l,
  • un suffixe d'une liste l est une liste k terminant l,
  • un facteur d'une liste l est le préfixe d'un suffixe de l, soit encore le suffixe d'un préfixe de l, ou encore une liste prolongeable à gauche et à droite en l.

Notre but est de formaliser les notions de préfixe et de facteur.

4.1 Préfixe d'une liste

Donner un système d'inférence définissant inductivement la notion de préfixe. Le système doit avoir la même structure que celui définissant la nouvelle relation d'ordre :

  • un axiome exprimant que la liste vide est le minimum pour la relation d'ordre "être préfixe" - règle [videMin] ;
  • une règle d'inférence exprimant que le constructeur de liste est croissant (pour la relation d'ordre "être préfixe") - règle [consCroissant].
			  ???
--------- [videMin]  ------------ [consCroissant]
  ???                     ???

Implémenter ce système par un prédicat inductif.

Inductive Prefixe{A : Type} : list A -> list A -> Prop :=
| videMin : ...
| consCroissant : ... .

Montrons que ce prédicat est équivalent à la proposition logique affirmant que le préfixe commence la liste.

Montrer l'adéquation de la définition.

  • Par induction sur la preuve de Prefixe k l.
  • Indication : pour exploiter l'hypothèse de récurrence HR : exists k' : list A, …, utiliser case HR as [k' eg].
Lemma decomposition_Prefixe :
  forall A, forall k l : list A, Prefixe k l -> exists k', k ++ k' = l.

Montrer la complétude de la définition.

  • Par induction sur k.
  • Indication : l'hypothèse de récurrence doit être quantifiée universellement sur l (forall l : list A, …).
Lemma Prefixe_decomposition :
  forall A, forall k k' l : list A, k ++ k' = l -> Prefixe k l.

4.2 Facteur d'une liste

Donner un système d'inférence définissant inductivement la notion de facteur :

  • k est un facteur de l si k est un préfixe de l - règle [prefixeFacteur] ;
  • l* si k est un facteur de l - règle [facteurInterne].
				???
-------- [prefixeFacteur]   ------------ [facteurInterne]
  ???                           ???

Implémenter ce système par un prédicat inductif.

Inductive Facteur{A : Type}(k : list A) : list A -> Prop :=
| prefixeFacteur : forall l, Facteur k l (* à modifier *)
| facteurInterne : forall l, Facteur k l. (* à modifier *)

Montrons que ce prédicat est équivalent à la proposition logique affirmant que le facteur est prolongeable à gauche et à droite en la liste.

Montrer l'adéquation de la définition.

  • Par induction sur la preuve de Facteur k l.
  • Indication : exploiter l'hypothèse Hp : Prefixe k l en appliquant le lemme decomposition_Prefixe, soit apply decomposition_Prefixe in Hp.
Lemma decomposition_Facteur :
  forall A, forall k l : list A, Facteur k l -> exists k' k'', k' ++ k ++ k'' = l.

Montrer la complétude de la définition.

  • Par induction sur k'.
  • Indications : l'hypothèse de récurrence doit être quantifiée universellement sur l (forall l : list A, …). Utiliser le lemme Prefixe_decomposition pour traiter un cas.
Lemma Facteur_decomposition :
  forall A, forall k' k k'' l : list A, k' ++ k ++ k'' = l -> Facteur k l.

5 Quelques lois logiques

On cherche à montrer deux lois de de Morgan :

  • la négation d'une disjonction est la conjonction des négations,
  • une disjonction de négations implique la négation de la conjonction.

Indication : utiliser la correspondance entre les règles logiques et les tactiques, donnée dans le guide.

Notation : ~X, négation de X, s'interprète comme (X -> False).

Loi 1 - Une équivalence.

  • Indication : une équivalence (<->) est définie comme une conjonction de deux implications.
Proposition negation_disjonction :
  forall P Q : Prop, ~(P \/ Q) <-> ~P /\ ~Q.

Loi 2 - Une implication. La réciproque ne peut pas être montrée en logique intuitionniste : il est nécessaire de recourir au tiers exclus.

Proposition disjonction_negations :
  forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).

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