Types inductifs

Coq est basé sur un formalisme appelé Calcul des Constructions avec types Inductifs.

Deux points de vue possibles:

• On se donne les entiers.
• On se donne les types inductifs en général (les entiers sont un cas particulier).

Inductive mois : Set :=
| Janvier : mois
| Février : mois
| Mars : mois
| Avril : mois
| Mai : mois
| Juin : mois
| Juillet : mois
| Aout : mois
| Septembre : mois
| Octobre : mois
| Novembre : mois
| Décembre : mois.

C'est une déclaration par énumération des éléments d'un ensembles (Set). Chaque nom de mois est un constructeur. Pour définir une fonction, il faut traiter chaque constructeur. Voici un exemple de définition d'une fonction par filtrage. Par convention commune avec langages, etc., | signifie “ou”.

Definition mois_suivant (m:mois) : mois :=
match m with
| Janvier => Février | Février => Mars
| Mars => Avril | Avril => Mai
| Mai => Juin | Juin => Juillet
| Juillet => Aout | Aout => Septembre
| Septembre => Octobre | Octobre => Novembre
| Novembre => Décembre | Décembre => Janvier
end.

Pour “exécuter” cette fonction, on utilise eval compute in:

eval comput in (mois_suivant Mars).

Pour revoir le code de cette fonction, Print mois_suivant..

Définissons une autre fonction sur cet ensemble, puis prouvons que les de fonctions s'annulent mutuellement.

Definition mois_precedent (m:mois) : mois :=
match m with
| Janvier => Decembre | Fevrier => Janvier
| Mars => Fevrier | Avril => Mars
| Mai => Avril | Juin => Mai
| Juillet => Juin | Aout => Juillet
| Septembre => Aout | Octobre => Septembre
| Novembre => Octobre | Decembre => Novembre
end.

Lemma mois_prec_suiv : forall m:mois,
mois_precedent (mois_suivant m)=m.
Proof.
intros m.
elim m;
simpl;
reflexivity.
Qed.

Lorsqu'on fait elim m. Cog décompose la preuve en autant de sous-preuves que de constructeurs, ici les 12 mois. Lorsque ensuite on commande simpl. il tente de simplifier l'expression en appliquant des évaluations des fonctions; mois_precedent (mois_suivant Janvier) = Janvier est transformé (simplifié) en Janvier = Janvier, ce qui peut être prouvé par réflexivité.

Ceci manque de commentaires. Ca sert à quoi?

mois_ind : forall P : mois -> Prop,
P Janvier -> P Fevrier -> P Mars ->
P Avril -> P Mai -> P Juin ->
P Juillet -> P Aout -> P Septembre ->
P Octobre -> P Novembre -> P Decembre ->
forall m : mois, P m

• L'égalité en Coq : pages 94-96
• Les sortes : pages 97

1. L'élément appelé zéro et noté: 0, est un entier naturel.
2. Si n est un entier naturel alors son successeur noté S(n) est un entier naturel.

Autre notation: P ::= O | S P

forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n

• Quantification universelle sur une propriété P: nat → Prop
• Conclusion : forall n : nat, P n
• 2 cas:
  • 1 cas de base
  • 2 récurrence

En Coq, un principe d'induction est automatiquement associé à chaque définition inductive.

Check list ind.
list_ind
: forall P : list -> Prop,
P Nil ->
(forall (n : nat) (l : list), P l -> P (Cons n l)) ->
forall l : list, P l

Pour cela, on dispose d'une tactique spécique discriminate.

Lemma Mars_Fev : Mars<>Fevrier.
intro H; discriminate.
Qed.

Lemma zero_succ : forall n:nat, ~(S n)=O.
intros n H; discriminate H.
Qed.

Pour cela, on dispose d'une tactique spécifique injection.

Lemma test_injection: forall x y, S x = S y -> x=y.
Proof.
intros.
injection H.
intro.
assumption.
Qed.

Maintenant qu'on a des structures de données on veut écrire des fonctions qui les manipulent.

Définition non récursive par filtrage:

Definition is_zero : nat -> bool :=
fun (n:nat) => match n with
O => true
| S _ => false
end.

ou bien

Definition is_zero (n:nat) :=
match n with
O => true
| S _ => false
end.

Exemple. Addition des entiers naturels:

Fixpoint plus (n m : nat) {struct n} : nat :=
match n with
| O => m
| S p => S (plus p m)
end.

Eval compute in (plus O 56).
Eval compute in (plus 12 67).
Eval compute in (plus 67 12).

En Coq les fonctions doivent toujours terminer ! L'annotation {struct n} indique l'argument qui décroit à chaque appel récursif. Cela est nécessaire pour pouvoir garantir la terminaison de la fonction.

Fixpoint bidon (n:nat) : nat := bidon n.

Cette définition est refusée par le système et conduit à une erreur

Error: Recursive definition of bidon is ill-formed.

La profondeur du filtrage peut être supérieur à 1. On peut par exemple définnir une fonction pour tester la parité :

Fixpoint pair (n:nat) : Prop :=
match n with O => True
| (S O) => False
| (S (S p)) => pair p
end.

Eval compute in (pair 8789).
Eval compute in (pair 8790).

Fixpoint fib n {struct n} :=
match n with
O => 1
| S O => 1
| S ((S n) as n1) => fib n + fib n1
end.

A la suite d'une définition par point-fixe un certain nombre de règles de calcul (une par cas du filtrage) sont ajoutées dans le système.

• tactiques compute, simpl pour faire des réductions dans le but courant.
• simpl in H, pour faire la même chose dans une hypothèse plutôt que pour le but courant.

Exemple : Les réductions pour plus:

• plus\; O\; m \longrightarrow_{\iota} m
• plus\; \left(S\; n\right)\; m \longrightarrow_{\iota} S\left(plus\; n \; m\right)

Associativité de l'opération d'addition:

forall n m p : nat, (plus (plus n m) p) =
(plus n (plus m p))

Croissance de la fonction Fibonacci:

forall n : nat, fib n <= fib (S n)

Associativité de +

Démonstration par induction: intros n m p; elim n.

• Cas de base : 0 + (m + p) = 0 + m + p
  • étape de simplification : on utilise les règles de calcul pour les fonctions mises en jeu (ici, uniquement +).
  • conclusion de la démonstration : introductions, puis reflexivity de l'égalité
• Cas de recurrence.

Fibonacci croissante I

Lemma fib_croissante : forall n : nat, fib n <= fib (S n).
Proof.
intros n.
assert (fib n <= fib (S n) /\ fib (S n) <= fib (S (S n))).
induction n.
(* cas de base *)
simpl;auto.
(* recurrence *)
assert (forall n : nat, fib (S (S n)) = fib n + fib (S n)).
simpl; trivial.
rewrite H.

Fibonacci croissante II

rewrite H.
split.
decompose [and] IHn; clear IHn.
assumption.
decompose [and] IHn; clear IHn.
apply (plus_le_compat).
assumption.
assumption.
(* fin assert *)
decompose [and] H; clear H.
assumption.
Qed.