Library coq1_B_A_BA

INITIATION A COQ (1)

Le début de ce fichier a été présenté en cours. Il est demandé de le réviser à la maison et de le terminer en préparation du TD suivant.

Lire attentivement les commentaires explicatifs
sous emacs/Proof-general,
- pour avancer d'une étape, faire C-c C-n
- pour reculer, C-c C-p
- pour aller d'un coup à la position du curseur, C-c RET.
D'autres raccourcis sont disponibles, regarder les menus Proof-General et Coq.

Généralités

Coq est primitivement un langage de programmation particulier. Comme OCaml, c'est un langage fonctionnel typé. Son système de types est beaucoup plus riche que celui de OCaml, ce qui permet en particulier d'énoncer des formules logiques, et éventuellement de les démontrer.

Dans un premier temps, on se focalise sur l'aspect programmation, et les formules logiques considérées sont de simples égalités.

Un script Coq est une suite de déclarations de types, de valeurs, (très souvent : des fonctions), d'énoncés de théorèmes suivis de leur preuve.

On a également des requêtes pour obtenir des informations, calculer des expressions.

À RETENIR : EN COQ, TOUT FINIT PAR UN POINT '.'

Types énumérés

Le type qui s'écrirait en OCaml type coulfeu = | Vert | Orange | Rouge

se définit en Coq presque de la même façon.

Inductive coulfeu : Set :=
  | Vert : coulfeu
  | Orange : coulfeu
  | Rouge : coulfeu
.

Comme en OCaml, blabla : machin se lit "blabla a pour type machin". Ainsi la déclaration précédente indique que Vert, Orange et Rouge sont de type coulfeu. Par ailleurs, en Coq tout a un type ; la déclaration ci-dessus indique que le type de coulfeu est Set, cf. notes de cours.

Définition d'une valeur fonctionnelle

Definition coul_suiv : coulfeu → coulfeu :=
  fun c ⇒
    match c with
    | Vert ⇒ Orange
    | Orange ⇒ Rouge
    | Rouge ⇒ Vert
    end.

La commande Check permet d'obtenir le type d'une expression. Elle vérifie que l'expression est bien typée.

Check coul_suiv.
Check (coul_suiv Vert).

La commande Eval permet de calculer une expression.

Eval compute in (coul_suiv Vert).

Raccourci

Compute (coul_suiv Vert).

Premier théorème, tactiques cbn et reflexivity

Theorem ex1_coul_suiv : coul_suiv (coul_suiv Vert) = Rouge.
Proof. cbn [coul_suiv]. reflexivity. Qed.

Remarque : on peut énoncer une théorème à prouver au moyen d'autres mots-clé, notamment Lemma (pour un résultat auxiliaire) ou Example (pour un théorème très simple servant à tester le résultat d'une fonction sur une entrée particulière. Ces mots-clé sont équivalents, le choix de l'un ou l'autre est affaire de convention ou d'usage. Ici on aurait donc plutôt utilisé Example. Example ex1_coul_suiv : coul_suiv (coul_suiv Vert) = Rouge.

Une *tactique* est une commande permettant de faire progresser une preuve

On a utilisé ci-dessus les tactiques suivantes :

cbn nom_de_fonction : évaluation (partielle) de nom_de_fonction
reflexivity : reconnaissance que les deux membres de l'égalité à prouver sont identiques (preuve de x = x).

ATTENTION À BIEN TERMINER PAR "Qed."

Variables

Les preuves par réflexivité fonctionnent non seulement entre des expressions constantes identiques, mais aussi entre des expressions comportant des variables.

On a la possibilité en Coq (mais pas en OCaml) de déclarer des variables : ce sont des noms dont on connaît simplement le type. Il faut que ces noms soient déclarés dans une portée (domaine de visibilité) définie par une section.

Ouverture d'une section dans laquelle on va faire quelques preuves par réflexivité.

Section sec_refl.
Variable c : coulfeu.

Signification intuitive : "soit c une coulfeu inconnue".

Theorem th1_refl_simple : c = c.

Remarquer que le but contient un environnement comportant l'hypothèse c : coulfeu.

Proof. reflexivity. Qed.

Check c.

Fermeture de la section, ce qui clôt la portée des variables, ici c : coulfeu.

End sec_refl.

Fail Check c.
Fail Definition x := Vert + 2.

Vu jusqu'ici dans ls CM1 2020, en fait juste avant le End sec_refl.

Principe de Leibniz : tactique rewrite

Section sec_reec.
Variable c : coulfeu.
Hypothesis crou : c = Rouge.

Signification intuitive, par analogie avec la ligne d'avant : "soit crou une preuve inconnue de c = Rouge".

  Theorem coul_suiv_Rouge : coul_suiv c = Vert.
  Proof.
    rewrite crou.
    cbn [coul_suiv].
    reflexivity.
  Qed.

End sec_reec.

Raisonnement par cas : tactique destruct

Section sec_cas.
  Variable c : coulfeu.

  Theorem th3_coul_suiv : coul_suiv (coul_suiv (coul_suiv c)) = c.
  Proof.

reflexivity ne fonctionne pas.

Fail reflexivity.

Il faut raisonner par cas sur les trois valeurs de c possibles Cela va donner lieu à trois sous-buts, un pour chaque cas. Ils se traitent de manière identique, on montre ci-dessous quelques raccourcis possibles qui seront expliqués en cours.

    destruct c as [ | | ].
    - cbn [coul_suiv]. reflexivity.
    - cbn. reflexivity.
    - reflexivity.
  Qed.

Remarque : la tactique destruct fonctionne comme un match dont les constructeurs, non nommés, sont traités dans l'ordre indiqué dans la déclaration du type concenré, ici coulfeu. En fait, destruct *fabrique* un match, ce que l'on peut voir en affichant le contenu de la preuve (par Print, comme vu en cours ; mais attention, ce qui est affiché est compliqué, se contenter à ce stade de voir la forme générale.)

End sec_cas.

Raisonnement universel : tactique intro

Il est possible d'énoncer des formules quantifiées universellement. Par exemple : ∀ c : coulfeu, c = c.

Theorem th_refl_gen : ∀ c : coulfeu, c = c.
Proof.

Pour la démontrer, la première étape consiste à dire "soit c0 une couleur arbitraire, démontrons c0 = c0."

intro c0.

Remarquer que intro a introduit l'hypothèse c0 : coulfeu. On a déjà vu que reflexivity fonctionne dans cette situation.

reflexivity.
Qed.

La tactique intro sert également à démontrer une implication.

Theorem th_crou_gen : ∀ c : coulfeu, c = Rouge → coul_suiv c = Vert.
Proof.
intro c0.

Pour démontrer c0 = Rouge → coul_suiv c0 = Vert, on suppose c0 = Rouge et on doit alors prouver coul_suiv c0 = Vert sous cette hypothèse supplémentaire ; lorsque l'on introduit une hypothèse, on lui donne un nom.

intro c0rou.

Le raisonnement sous-jacent est : soit c0rou une preuve arbitraire (inconnue) de c0 = Rouge, on peut s'en servir pour démontrer coul_suiv c0 = Vert.

rewrite c0rou. cbn [coul_suiv]. reflexivity.
Qed.

Remarque : on est souvent amené à effectuer plusieurs introductions successives. On emploie alors le raccourci intros (au pluriel). Sur l'exemple précédent cela donne ceci :

Theorem th_crou_gen_bis : ∀ c : coulfeu, c = Rouge → coul_suiv c = Vert.
Proof.
intros c0 c0rou.
rewrite c0rou. cbn [coul_suiv]. reflexivity.
Qed.

Début du travail à faire à la maison

Exercice: Variante du précédent avec section

Section sec_variante_th_crou_gen.
  Variable c : coulfeu.
  Theorem th_crou_demi_gen : c = Rouge → coul_suiv c = Vert.
  Proof.

à compléter

Admitted.

End sec_variante_th_crou_gen.

Exercice: Preuve par cas d'un théorème avec forall

Lemma suivsuivsuiv_id : ∀ c:coulfeu, coul_suiv (coul_suiv (coul_suiv c))=c.
Proof.

à compléter ici

Admitted.

Type inductif et récurrence structurelle : arbres binaires tricolores

Inductive arbin : Set :=
| F : coulfeu → arbin
| N : arbin → arbin → arbin.

Pour définir une fonction récursive (l'équivalent de let rec en OCaml) on utilise le mot clé Fixpoint.

Fixpoint renva a : arbin :=
  match a with
  | F c ⇒ F c
  | N g d ⇒ N (renva d) (renva g)
  end.

Exercice: prouver que renverser deux fois un arbre rend le même arbre

Theorem renva_renva : ∀ a, renva (renva a) = a.
Proof.
intro a.

Tentative de raisonnement par cas sur a Les noms mis dans chaque cas (c pour le premier, a2 a2 pour le second) désignent les composantes des constructeurs respectivement F puis N

  destruct a as [ c
                | a1 a2 ].
  - cbn [renva]. reflexivity.
  - cbn [renva].

Il apparaît qu'un simple raisonnement par cas est insuffisant, donc on arrete tout...

Abort.

... et on recommence en raisonnant par récurrence structurelle

Theorem renva_renva : ∀ a, renva (renva a) = a.
Proof.
intro a.

récurrence structurelle sur le type inductif arbin Remarquer l'analogie avec l'utilisation de la tactique destruct : les noms mis dans chaque cas (c pour le premier, a2 a2 pour le second) désignent les composantes des constructeurs respectivement F puis N mais en complément, on ajoute deux noms pour les hypothèses de récurrence, Hrec_a1 pour celle sur a1 et Hrec_a2 pour celle sur a2

  induction a as [ c
                 | a1 Hrec_a1 a2 Hrec_a2 ].
  - cbn [renva]. reflexivity.
  - cbn [renva].

Admitted.

Fin du travail à faire à la maison.