Library coq2_B_A_BA_surpr

INITIATION A COQ (2) : définition interactive de fonctions

Complément à coq1_B_A_BA.v, contenant juste le nécessaire pour définir coul_suiv ; Définition de la même fonction, en mode preuve interactive pour illustrer le développement pas à pas d'une fonction au moyen de tactiques.

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

Définition d'origine
Definition coul_suiv : coulfeu → coulfeu :=
  fun c ⇒
    match c with
    | Vert ⇒ Orange
    | Orange ⇒ Rouge
    | Rouge ⇒ Vert
    end.

Définition en mode interactif
Definition coul_suiv2 : coulfeu → coulfeu.
Proof.
  intro c.
  destruct c as [ | | ].
  Show Proof.
  - exact Orange.
  - exact Rouge.
  - exact Vert.
Defined.

Print coul_suiv2.

Définition en utilisant la tactique refine
Definition coul_suiv3 : coulfeu → coulfeu.
Proof.
  intro c. Undo 1.
  refine (fun c ⇒ _).
  destruct c as [ | | ]. Undo 1.
  refine (match c with
          | Vert ⇒ _
          | Orange ⇒ _
          | Rouge ⇒ _
          end).
  Show Proof. Undo 2.
  refine (fun c ⇒
            match c with
            | Vert ⇒ _
            | Orange ⇒ _
            | Rouge ⇒ _
            end).
  Undo 1.
  refine (fun c ⇒
            match c with
            | Vert ⇒ _
            | Orange ⇒ Rouge
            | Rouge ⇒ _
            end).
  - refine Orange.
  - refine Vert.
Defined.

Et pour les théorèmes ?
  • Une preuve de P -> Q est une fonction qui fabrique une preuve de Q à partir de n'importe quelle preuve de P
  • une preuve de ∀x, P x est une fonction qui fabrique une preuve de P x à partir de n'importe quel x

Lemma coul_suiv_V_O :
  ∀ c,
    c = Vert ∨ c = Orange → coul_suiv c = Rouge ∨ coul_suiv c = Orange.
Proof.
  intros c deux_cas.
  destruct deux_cas as [cv | co].
  - rewrite cv. cbn [coul_suiv]. right. reflexivity.
  - left. rewrite co. cbn. reflexivity.
Show Proof. Qed.

Cette idée sera explorée en détail dans coq3_B_A_BA.v