Library prog

Dans ce fichier nous introduisons les définitions de types inductifs en Coq, ainsi que la programmation de fonctions simples manipulant ces types.

Dans tout l'exercice on utilisera l'axiom suivant, analogue du Obj.magic d'OCaml, quand on n'a pas (encore) d'expression du bon type, par exemple dans les trous laissés en exercice. Votre mission est de supprimer toute utilisation de TODO dans la feuille.

Axiom TODO : ∀ x:Type, x.

Entiers naturels

Coq dispose d'une librairie standard définissant les entiers naturels, mais pour s'entraîner nous définissons les nôtres.

Cette déclaration est analogue à la déclaration OCaml type nat = Zero | Succ of nat. Nous ne déclarons pas de sucre syntaxique pour ce type, mais en commentaire on se permet d'écrire par exemple 2 pour Succ (Succ Zero).

Inductive nat : Type :=
| Zero : nat
| Succ : nat → nat.

On définit récursive la fonction d'addition, de façon analogue à la définition OCaml let rec plus m n = ....

Fixpoint plus (m:nat) (n:nat) : nat :=
  match m with
  | Zero ⇒ n
  | Succ p ⇒ Succ (plus p n)
  end.

On peut demander à Coq de réaliser quelques calculs pour vérifier. En Coq, une expression est identifiée avec le résultat de son évaluation.

Compute Zero.
Compute (Succ Zero).
Compute (plus (Succ Zero) Zero).
Compute (plus Zero (Succ Zero)).

Fixpoint double (m:nat) : nat := TODO _.

Compute double (Succ Zero).

Prédicat de parité

On définit inductivement un prédicat sur nat, c'est à dire un ensemble d'entiers.

Inductive even : nat → Type :=
  | EZ : even Zero
  | ES : ∀ n, even n → even (Succ (Succ n))

Le constructeur ES prend un entier n et une dérivation attestant que l'entier est pair (une expression de type even n) et construit une dérivation indiquand que 2+n est lui aussi pair. Le type du résultat dépend de la valeur n; ceci est noté via le mot clé ∀. En Coq, le type flèche est un cas particulier particulier de cette construction: A→B est ∀ _:A, B.

On vérifie ici que des termes sont bien typés. Prenez le temps de comprendre leurs types.

Check EZ.
Check (ES Zero EZ).
Check (ES _ EZ).

L'expression laissée vide _ est inférée par Coq.

Les type ∀ sont une généralisation des types flèches usuels, ils sont habités par des fonctions, notées avec fun comme pour les types flèches usuels. Attention à bien comprendre les deux applications faites sur ES.

Check (fun n e ⇒ ES n e).

On utilise ici Definition plutôt que Fixpoint car il n'y a pas besoin de récursion.

Definition even_4 : even (Succ (Succ (Succ (Succ Zero)))) := TODO _.

On voit ci-dessous que Coq identifie 2+2 et 4.

Definition deux := Succ (Succ Zero).
Definition even_2_plus_2 : even (plus deux deux) := even_4.

Implémentez une fonction qui prouve que les entiers pairs sont stables par quadruple successeur.

Definition even_succ : ∀ n, even n → even (Succ (Succ (Succ (Succ n)))) :=
TODO _.

Implémentez la fonction suivante qui construit pour tout entier n une dérivation attestant que le double de n est pair.

Fixpoint even_double (n:nat) : even (double n) := TODO _.

Entiers naturels en binaire

On peut représenter les entiers positifs en binaire, en partant de zéro et avec les opérations _*2 et _*2+1.

Inductive bin : Type :=
  | BZ : bin
  | B0 : bin → bin
  | B1 : bin → bin.

L'intention derrière cette représentation est que BZ représente le zéro, B0 est l'opération _*2 et B1 est _*2+1.

Implémentez la fonction de conversion vers nat correspondant à cette intention.

Fixpoint convert (b:bin) : nat := TODO _.

Définition du successeur sur bin.

Fixpoint bsucc (b:bin) : bin := TODO _.

Relation d'égalité entre bin et nat

On définit inductivement une relation entre des entiers bin et nat.

Inductive equal : bin → nat → Type :=
  | EQZ : equal BZ Zero
  | EQ0 : ∀ b n, equal b n → equal (B0 b) (double n)
  | EQ1 : ∀ b n, equal b n → equal (B1 b) (Succ (double n)).

Quelques exemples.

Definition eq_0 : equal BZ Zero :=
EQZ.

Definition eq_1 : equal (B1 BZ) (Succ Zero) := TODO _.

TODO: définir eq_2, eq_3.

Preuve d'égalité entre un entier binaire et sa conversion.

Fixpoint equal_convert (b:bin) : equal b (convert b) := TODO _.

Implémentez les fonctions suivantes: deux préliminaires et un gros morceau...

Definition conv_succ_bz : equal (bsucc BZ) (Succ (convert BZ)) := TODO _.

Definition conv_succ_b0 :
  ∀ c, equal (bsucc (B0 c)) (Succ (convert (B0 c))) := TODO _.

Fixpoint conv_succ (b:bin) : equal (bsucc b) (Succ (convert b)) := match b with
  | BZ ⇒ TODO _
  | B0 c ⇒ TODO _
  | B1 c ⇒ TODO _
end.