Projet Coq

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é.

Definition peirce := forall P Q:Prop, ((P->Q)->P)->P.
Definition classic := forall P:Prop, ~~ P -> P.
Definition excluded_middle := forall P:Prop, P \/ ~P.
Definition de_morgan_not_and_not := forall P Q:Prop, ~(~P/\~Q)->P\/Q.
Definition implies_to_or := forall P Q:Prop, (P->Q)->(~P\/Q).

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).

Je choisis l'ordre de définition.

Lemma ax_peirce_classic : peirce -> classic.
  unfold peirce; unfold classic.
  intros H P.
  intro NNP.
  apply (H (P) False).
  intros NP.
  apply False_ind.
  apply NNP.
  unfold not.
  apply NP.
Qed.

J'écris une fois le lemme qui prouve qu'on obtient la même expressivité et ensuite je ne prouve que les lemmes qui prouvent que les 5 axiomes s'impliquent mutuellement.

Lemma peirce_classic : forall P, (classic -> P) -> (peirce -> P).
  intros P HP C.
  apply HP.
  apply ax_peirce_classic;auto.
Qed.

Lemma ax_peirce_emd : peirce -> excluded_middle.
intro PE.
unfold excluded_middle. intros P.
unfold peirce in *.
apply (PE (P\/~P) False).
intro PONP.
right. intro.
apply PONP.
left.
auto.
Qed.

Lemma emd_morgan : excluded_middle -> de_morgan_not_and_not.
intro.
unfold excluded_middle in *.
unfold de_morgan_not_and_not in *.
intros P Q NNPQ.
destruct (H (P\/ Q)); auto.
apply False_ind.
apply NNPQ.
split;intro; apply H0;tauto.

joli ;)

Qed.

Lemma morgan_imp : de_morgan_not_and_not -> implies_to_or.
unfold de_morgan_not_and_not in *.
unfold implies_to_or in *.
intros MOR P Q PIQ.
apply MOR.
intro.
destruct H.
apply H.
intro.
tauto.
Qed.

Lemma imp_peirce : implies_to_or -> peirce.
unfold implies_to_or.
unfold peirce.
intros IMP P Q H.
destruct (IMP P P);tauto.
Qed.

Question 2:

Prouvez la dualité classique entre exists et forall.

Theorem forallExists : forall A, forall P : A -> Prop,
                         peirce -> (~ (forall x : A, P x) <-> (exists x : A, ~ P x)).
  intros A P CL; split; intro H.
  assert ((~(exists x:A, ~P x) -> (exists x:A, ~P x)) -> (exists x:A, ~P x)).
  apply CL.
  apply H0.
  intro NE.
  apply False_ind.
  apply H.
  intro x.
  assert (((~P x) -> (P x)) -> P x).
  apply CL.
  apply H1; intro NP.
  apply False_ind.
  apply NE.
  exists x; auto.

  intro F.
  destruct H.
  apply H.
  apply F.
Qed.

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

Theorem existsForall : forall A, forall P : A -> Prop,
(~ (exists x : A, P x) <-> (forall x : A, ~ P x)).
intros A P. split.
intros NE x Px.
apply NE.
exists x; auto.
intro Fx.
intro Ex.
destruct Ex.
apply (Fx x);auto.
Qed.

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:

Check (lt: nat -> nat -> Prop).

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.

Inductive Acce (A:Set) (R:A->A->Prop) : A->Prop :=
Accessible : forall x:A, (forall y:A, R y x -> Acce A R y) -> Acce A R x.

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":

Definition bienFonde (A:Set) (R:A->A->Prop) : Prop := forall a:A, Acce A R a.

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).

Lemma bienFonde_pasDecr : forall (A:Set) (R:A -> A -> Prop), bienFonde A R -> forall suite:nat->A, ~(forall n:nat, R (suite (S n)) (suite n)).

Voir l'énoncé dans la preuve plus bas.

Question 2:

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

Lemma nonAcce_uneEtape : forall (A:Set) (R : A -> A -> Prop) (a b:A),
                           R a b -> ~ Acce A R a -> ~ Acce A R b.
  intros A R a b H H0 H1.
  absurd (Acce A R a); auto.
  generalize a H.
  elim H1; auto.
Qed.

Lemma acce_uneEtape : forall (A:Set) (R : A -> A -> Prop) (a b:A),
                        R a b -> Acce A R b -> Acce A R a.
  intros A R a b H H0.
  generalize a H.
  elim H0; auto.
Qed.

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.

Lemma bienFonde_ind : forall (A : Set) (R : A -> A -> Prop),
                   bienFonde A R ->
                   forall P : A -> Prop,
                     (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
                     forall a : A, P a.
  intros.
  Check Acce_ind.
  apply (Acce_ind A R).
  intros.
  apply H0.
  auto.
  apply H.
Qed.

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).

Definition induction_forte : forall P : nat -> Prop,
                               (forall n, (forall k, k < n -> P k) -> P n) -> forall n, P n.
Proof. Require Import Arith.
  intros P IH n.
  cut (forall k, k <= n -> P k).
  intros stronger; apply stronger; auto.
  induction n; intros k Hk.
  inversion Hk; apply IH; intros ? H0; inversion H0.
  destruct (le_lt_eq_dec _ _ Hk).
  apply IHn; auto with arith.
  subst; apply IH; intros p Hp; apply IHn; auto with arith.
Qed.

Lemma lt_bienFonde : bienFonde nat lt.
  unfold bienFonde.
  apply induction_forte; apply Accessible; intros y H;inversion H.
Qed.

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.

Lemma pas_decroissante : forall (A:Set) (R:A -> A -> Prop),
bienFonde A R ->
forall suite:nat->A, ~(forall n:nat, R (suite (S n)) (suite n)).

Todo: des commentaires pour les étaps principales.

  intros A R WF suite.
  unfold not; intro dec.
  cut (forall a:A, (exists i:nat, suite i = a) -> ~ Acce A R a).
  intro H.
  absurd (Acce A R (suite 0)).
  apply H.
  exists 0; trivial.
  apply WF.
  intro a; pattern a in |- *.
  apply (bienFonde_ind A R);auto.
  intros x Hx H.
  elim H.
  intros i egi.
  cut (R (suite (S i)) (suite i)).
  intro H1.
  rewrite <- egi.
  apply nonAcce_uneEtape with (suite (S i)); auto.
  apply Hx.
  rewrite <- egi; auto.
  exists (S i); auto.
  auto.
Qed.

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.".

Axiom classique: forall P Q:Prop, ((P->Q)->P)->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).

Axiom axiomeChoix : forall (A:Set)(R:A->A->Prop),
(forall x, exists y, R x y )->
exists f, forall x, R x (f x).

Exercice 6: la réciproque

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

Lemma bienfonde : forall (A:Set) (R:A -> A -> Prop) ,
                    ~ bienFonde A R ->
                    exists suite:nat->A, forall n:nat, R (suite (S n)) (suite n).
  intros A R NWF.

1. >>> En invoquant l'axiome du choix, on montre que si x n'est pas accessible alors il existe une fonction de A vers A qui choisit un prédécesseur y de x qui n'est pas accessible (ce y existe car sinon x serait accessible).

  assert (exists f:A->A, forall x, ~Acce A R x -> ~ Acce A R (f x) /\ R (f x) x).
  destruct (axiomeChoix A (fun x y => Acce A R x \/ R y x /\ ~ Acce A R y)) as [f].
  intro x.

Deux cas: soit x est accessible (et alors on conclut avec left) soit x ne l'est pas et dans ce cas on sait qu'il existe un élément plus petit qui ne l'est pas non plus (par contraposée) et on conclut avec right.

  assert (MD: Acce A R x \/ ~ Acce A R x).
  apply ax_peirce_emd.
  unfold peirce;apply classique.
  destruct MD as [Ax | NAx].

a) >> x est accessible

exists x.
left;auto.

b) >> x n'est pas accessible

  assert (Pred: exists y, ~ Acce A R y /\ R y x).
  assert(Contra: ~~ exists y : A, ~ Acce A R y /\ R y x).
  intro NE.
  apply NAx.
  apply Accessible.
  intros y Ryx.
  assert (Contra: ~~ Acce A R y).
  intro NAy.
  apply NE.
  exists y.
  tauto.
  apply ax_peirce_classic.
  unfold peirce; apply classique;auto. auto.
  apply ax_peirce_classic.
  unfold peirce. apply classique;auto. auto.
  destruct Pred.
  exists x0. right. tauto.

  exists f. intros x NAx.
  destruct (H x) as [HA | [Rfx NAx2]].
  tauto.
  tauto.

  destruct H as [f].

2. >>> On montre qu'il existe un élément non accessible puisque la relation n'est pas bien fondée.

  assert (ENA : exists a:A, ~ Acce A R a).
  Check forallExists.
  apply -> forallExists;auto.
  unfold peirce; apply classique.
  destruct ENA as [x0].

3. >>> On construit une suite de points de A en itérant la fonction f en partant de x0. (cette suite sera notre candidat).

  pose (F := (fix F (n:nat) : A :=
                match n with
                  | 0 => x0
                  | S p => f (F p)
                end)).
  exists F.
  assert (forall n : nat, R (F (S n)) (F n) /\ ~ Acce A R (F (S n))).
  induction n.

On montre que la suite est un bon candidat par induction sur n.

  simpl.
  destruct (H x0);tauto.
  destruct IHn as [RE NAFSn].
  change (F (S (S n))) with (f (F (S n))).
  destruct (H (F (S n)));auto.
  intro n; apply H1.
Qed.

This page has been generated by coqdoc