===== 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 ====

  * [[preuves_egalite|]] : pages 94-96
  * [[preuves_sortes|]] : pages 97

==== Avec Récursion ====

=== Les entiers de Peano ===

  - L'élément appelé zéro et noté: 0, est un entier naturel.
  - 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:

  * <jsm>plus\; O\; m \longrightarrow_{\iota}  m</jsm>
  * <jsm>plus\; \left(S\; n\right)\; m \longrightarrow_{\iota} S\left(plus\; n \; m\right)</jsm>

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