Projet Coq 2014 - L3 S1 - Lucca Hirschi

Vous pouvez lire ce document dans sa version HTML mais l'idéal est de le compiler au fur et à mesure pour lire les messages renvoyés par Coq.

Lien vers la page du projet:

http://www.lsv.ens-cachan.fr/~hirschi/enseignements/projet_coq/projet_coq.php

I : Introduction

Ce projet est constitué de deux parties pratiquement indépendantes. La première section est assez facile mais demande d'écrire pas mal de preuves. La seconde section demande plus de réflexion. Essayez de l'aborder en TP pour que je puisse vous aider.

Et, s'il vous plait, ne copiez pas les uns sur les autres: ça se verra (trop) facilement (il y a beaucoup de façon d'aborder une preuve).

II : Axiomes de la logique classique

L'axiomatisation de base de Coq ne permet que de prouver des preuves en logique intuitioniste (et non classique). La conséquence (voulue) est que toutes les preuves sont constructives (i.e., à chaque preuve correspond un terme calculant une fonction totale du type de la proposition prouvée).

Si l'on veut travailler dans une logique classique, on doit alors déclarer un "axiome classique" dans Coq. On peut ajouter le raisonnement par l'absurde, ou ajouter la loi de Peirce par exemple. L'objectif de la première partie du projet est de montrer que les logiques induites par cinq axiomes différents ont la même expressivité.

Exercice 1: preuves classiques

Question 1:

Prouvez que les logiques induites par ces propriétés ont la même expressivité. Le plus simple est de choisir un ordre (par exemple classic => peirce => implies_to_or => ... => classic) et prouvez une série de lemmes de la forme:

Lemma peirce_classic : forall P, (classic -> P) -> (peirce -> P).

Question 2:

Prouvez la dualité classique entre exists et forall.

Et le symétrique? As-t-on besoin de la logique classique?

III : Relations bien fondées

Dans cette section, on va formaliser le prédicat "relation bien fondée" et on va prouver, entre autre, l'implication et la réciproque entre:

• (i) une relation est bien fondée (selon notre formalisation),
• (ii) une relation n'admet pas de suite infinie décroissante.

Le sens direct est prouvable en logique intuitionniste. On introduira donc pas d'axiome supplémentaire. On prouvera par contre la réciproque en logique classique (avec l'un des axiomes de la section II) + un axiome magique.

1. Sens direct en logique intuitionniste

Il faut commencer par formaliser cette propriété (i) en Coq. Commençons par les relations. On se limitera dans ce projet aux relations entre un même ensemble. Le type des relations sur un ensemble A s'écrit donc R : A -> A -> Prop. Regardez par exemple la relation "<" sur les entiers:

Pour formaliser qu'une relation est bien fondée (i) on va définir un prédicat Acce sur les éléments x d'un ensemble A tel que:

• les éléments minimaux pour R vérifient le prédicat,
• si tous les éléments y plus petits que x vérifient le prédicat alors x le vérifie aussi.

Intuitivement, Acce A R x est prouvable si vous avez une preuve (et donc un objet fini mais qui peut contenir des inductions) qui explore tous les éléments plus petits que x. Ce prédicat est donc prouvable uniquement pour les éléments qui n'appartiennent à aucune chaîne infinie décroissante.

On peut donc formaliser le prédicat "bien fondée":

Cette présentation est plus effective que (ii), si vous prouvez qu'une relation est bienFondé alors vous construisez une fonction qui pour tout élément de A explore toutes les chaînes descendantes à partir de cet élément. C'est un outil essentiel pour pouvoir définir des fonctions récursives bien fondées mais non structurellement décroissantes.

Exercice 2: Préliminaires

Question 1:

Ecrivez le prédicat sur les relations "la relation n'admet pas de suite infinie décroissante". Ecrivez l'énoncé du sens direct).

Question 2:

Pour vous échauffer, prouver les deux lemmes suivants qui pourront vous servir dans la suite.

Question 3:

Prouvez maintenant le lemme suivant permettant de réaliser des inductions en exploitant une relation bien fondée (notez que c'est le but premier des relations bien fondées: permettre d'aller au delà des fonctions récursives structurellement décroissantes). Lui aussi pourra vous être utile. Pensez bien au lemme d'induction généré par la définition inductive du prédicat Acce.

Exercice 3: Preuves de bonne fondaison

Question 1:

On montre que la relation < : nat -> nat -> Prop est bien fondée (conseil: vous aurez besoin d'un lemme d'induction forte).

Question 2:

Ecrivez le prédicat lex qui prend deux relations et qui formalise la relation lexicographique sur ces deux relations. Prouvez maintenant que si deux relations sont bien fondées alors la relation lexicographique de ces deux relations l'est aussi.

Exercice 4: Le sens direct

Et maintenant, prouvez le sens direct de l'implication.

2. Réciproque en logique classique

On s'attaque maintenant à la réciproque!

Exercice 5: Préliminaires

La réciproque n'est pas prouvable en logique intuitionniste (des intuitions? écrivez-les). On introduit donc un axiome classique que l'on pourra utiliser dans la suite. La syntaxe est "Axiom [nom_axiome] : P.".

Tentez de prouver la réciproque sur papier en logique classique. De quoi avez-vous besoin ? Est-ce que c'est prouvable dans Coq (avec l'axiome classique) ?

Vous avez le droit d'ajouter un axiome tant qu'il appartient à la théorie des ensembles de Zermelo-Fraenkel (cf.Wikipedia).

Exercice 6: la réciproque

Et maintenant, muni de ces deux axiomes, prouvez la réciproque.