Structures de données

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

Premier exemple (sans récursion)

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

Diapo 93

Raisonnement par cas

FIXME 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

Apartés

Avec Récursion

Les entiers de Peano

  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

Coq vs OCaml

Coq Caml
Inductive nat : Set := type nat =
O : nat O
| S : nat → nat. | S of nat

Récursion/Induction sur ''nat''

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.

Autre exemple: les listes

Coq Caml
Inductive list : Set := type list =
Nil : list Nil
| Cons : nat → list → list. | Cons of int*list

Principe d'induction : les listes

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

Les constructeurs sont distincts

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.

Les constructeurs sont injectifs

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.

Définition de fonctions

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

Caml Coq
let De finition
let rec Fixpoint

Fonction non récursive

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.

Fonction récursive: point fi xe

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.

Exemple

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.

Profondeur de filtrage

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

Exemple: Fibonacci

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

Évaluation des fonctions

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)

Preuve de propriétés de programmes

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.
 
m1ilc/preuves_4.txt · Dernière modification: 2010/05/19 10:54 par suitable
 
Sauf mention contraire, le contenu de ce wiki est placé sous la licence suivante :CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki