Commit 44af73af authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

le script présenté au cours 4

parent 1e1e809b
(** * Une introduction aux types dépendants *)
(** ** Un premier exemple : les n-uplets *)
(** Rappel: le type des paires *)
Check (1,2).
Print prod.
(** Coq propose du "sucre syntaxique" pour les triplets et
autres n-uplets: [nat*nat*nat] est en fait [(nat*nat)*nat],
et [(1,2,3)] est en fait [((1,2),3)]. *)
Check (1,2,3).
Check ((1,2),3).
Unset Printing Notations.
Check (1,2,3).
Set Printing Notations.
(** Comment définir un type des n-uplets ? *)
(** Premier essai, via un type inductif *)
Inductive nuplets_ind (A:Type) :=
| Nothing
| More : A -> nuplets_ind A -> nuplets_ind A.
Arguments Nothing {A}. (* Pour rendre A implicite *)
Arguments More {A}. (* Idem *)
Check (More 1 (More 2 (More 3 Nothing))).
(** On a juste réalisé un clone du type des listes...
Et le typage ne distingue pas une paire d'un triplet *)
(** Mieux : on "programme" le type voulu, à partir d'un entier.
Le type obtenu dépend de la valeur de cet entier :
c'est un type dépendant. *)
Fixpoint nuplets (A:Type) n :=
match n with
| 0 => A
| S n => ((nuplets A n) * A)%type
end.
(** NB: le [*] ci-dessus est la syntaxe du type des paires
(prod), et le [%type] indique d'utiliser la famille de
notations des types au lieu de celui par défaut des [nat]
(où [*] est la multiplication). *)
Locate "*".
Compute (nuplets nat 5). (* sextuplets d'entiers *)
(** Et on peut même réutiliser le "sucre syntaxique"
des nuplets Coq pour construire des examples *)
Check (1,2,3,4,5,6) : nuplets nat 5.
(** Plus généralement, on peut aussi programmer des nuplets *)
Fixpoint ints n : nuplets nat n :=
match n with
| 0 => 0
| S n' => ((ints n'), n)
end.
Compute ints 5.
Check ints.
(** On verra plus bas une autre solution possible pour représenter
les n-uplets : le type [vect] des "vecteurs" Coq *)
(** ** Arbres binaires complets *)
(** La même approche que précédemment nous permet de représenter
des arbres binaires parfaits de hauteur [n]. *)
Fixpoint bintree (A:Type) n :=
match n with
| 0 => A
| S n => (bintree A n * bintree A n)%type
end.
Check ((1,2),(3,4)) : bintree nat 2.
Fixpoint sumtree n : bintree nat n -> nat :=
match n with
| 0 => fun a => a
| S n => fun a => let (g,d) := a in sumtree n g + sumtree n d
end.
(** Et pour mettre les données aux noeuds au lieu des feuilles : *)
Set Universe Polymorphism. (* Sinon soucis de niveaux d'univers *)
Inductive unit : Type := Tt. (* Un type singleton pour les feuilles *)
Fixpoint bintree' (A:Type) n :=
match n with
| 0 => unit
| S n => (bintree A n * A * bintree A n)%type
end.
(** NB: on a utilisé ici des triplets Coq, qui ne sont pas
primitifs (paires de paires). On aurait plus aussi définir
un type inductif ad-hoc. *)
(** Ici encore, l'utilisation d'un [Fixpoint] n'est qu'une des
solutions possibles, on pouvait également définir un type
inductif dépendant, cf plus tard. *)
(** ** Fonctions d'arité [n] *)
(** Définition du type des fonctions à [n] arguments entiers
(et réponse entière). *)
Fixpoint narity n :=
match n with
| 0 => nat
| S n => nat -> narity n
end.
Compute narity 5.
(** Exemple d'utilisation : création d'une fonction n-aire
faisant la somme de tous ses arguments.
Attention, le premier argument est [n], qui sert à indiquer
le nombre d'arguments qui va suivre. *)
(** Dans un premier temps, c'est plus commode de supposer avoir
au moins un argument à additionner, on peut s'en servir
comme accumulateur. *)
Fixpoint narity_S_sum n : narity (S n) :=
match n with
| 0 => fun a => a
| S n => fun a b => narity_S_sum n (a+b)
end.
(** On peut ensuite s'en servir dans le cas général. *)
Definition narity_sum n : narity n :=
match n with
| 0 => 0
| S n => narity_S_sum n
end.
Compute narity_sum 4 5 1 2 3 : nat. (* 5 + 1 + 2 + 3 = 11 *)
(** ** Type des "entiers ou booléens" *)
(** On peut contrôler (via p.ex. un booléen) si un type
sera [nat] ou [bool]. *)
Definition nat_or_bool (b:bool) : Type :=
if b then nat else bool.
Definition value_nat_or_bool (b:bool) :=
match b return (nat_or_bool b) with
| true => 0
| false => false
end.
(** Tel quel, ça n'a pas un intérêt fou. Mais on peut s'en
servir p.ex. quand on écrit un interpréteur d'un langage,
dont les résultats peuvent être dans plusieurs types. *)
(** L'aternative (non-dépendante) serait un "type somme"
plus habituel, cf ci-dessous. Mais quand on veut récupérer,
disons, un entier dans ce type, que faire si on est face à
un [Bool b] ? Il faut alors gérer ce genre d'erreur.
Tandis qu'avec une solution via des types dépendants, on n'a
pas ce souci. *)
Inductive natOrbool :=
| Nat : nat -> natOrbool
| Bool : bool -> natOrbool.
(** ** Types dépendants via inductifs *)
(** Vectors *)
(** Il s'agit d'un autre codage possible des n-uplets.
On reprend la définition des listes, mais on annote par
la longueur [n].
Cf. la bibliothèque standard Coq, fichier [Vector.v] *)
Inductive vect (A:Type) : nat -> Type :=
| Vnil : vect A 0
| Vcons n : A -> vect A n -> vect A (S n).
Arguments Vnil {A}.
Arguments Vcons {A}.
(** Codage du triplet (0,2,3) : *)
Check (Vcons 2 0 (Vcons 1 2 (Vcons 0 3 Vnil))).
(** On peut même rendre implicit l'argument [n] de [Vcons],
qui sera normalement toujours clair d'après le contexte: *)
Arguments Vcons {A} {n}.
Check (Vcons 0 (Vcons 2 (Vcons 3 Vnil))).
(** Mais cet argument [n] est toujours là en interne: *)
Set Printing All.
Check (cons 0 (cons 2 (cons 3 nil))).
Unset Printing All.
(** Conversion entre vecteurs et listes usuelles *)
Require Import List.
Import ListNotations.
Fixpoint v2l {A} {n} (v : vect A n) : list A :=
match v with
| Vnil => []
| Vcons x v => x::(v2l v)
end.
Fixpoint l2v {A} (l: list A) : vect A (length l) :=
match l with
| [] => Vnil
| x :: l => Vcons x (l2v l)
end.
(** La définition suivante est inutile vu que la longueur [n]
doit déjà être donnée au début. On pourra montrer plus tard
que [forall A n (v:vect A n), length v = n]. *)
Fixpoint length {A} {n} (v: vect A n) : nat :=
match v with
| Vnil => 0
| Vcons _ v => 1 + length v
end.
(** On évite avec les vecteurs les soucis classiques
lors de la définition des fonctions telles que [head]
sur les listes. *)
Definition head {A} (l:list A) (default : A) : A :=
match l with
| [] => default
| x :: _ => x
end.
Definition head_opt {A} (l:list A) : option A :=
match l with
| [] => None
| x :: _ => Some x
end.
Definition Vhead {A} {n} (v:vect A (S n)) : A :=
match v with
| Vcons x _ => x
end.
(** En interne, il y a quand même un cas pour [Vnil], mais
rempli avec du code arbitraire: on sait qu'il ne sera pas
utilisé *)
Print Vhead.
Compute Vhead ((Vcons 0 (Vcons 2 (Vcons 3 Vnil)))).
Fail Compute Vhead Vnil.
(** Concaténation de vecteurs
Tout se passe bien, vu qu'on respecte les équations
qui définissent l'addition des [nat].
*)
Print Nat.add.
Fixpoint Vapp {A} {n m} (v:vect A n) (v':vect A m) : vect A (n+m) :=
match v with
| Vnil => v'
| Vcons x v => Vcons x (Vapp v v')
end.
(** Par contre le renversement d'un vecteur n'est pas
définissable directement. Il faudrait qu'un [n+1] soit
convertible à un [S n] à l'intérieur. Or on peut prouver
que n+1 = S n, mais ce n'est pas un simple calcul (mais une
récurrence).
*)
Fail Fixpoint Vrev {A} {n} (v:vect A n) : vect A n :=
match v with
| Vnil => Vnil
| Vcons x v => Vapp (Vrev v) (Vcons x Vnil)
end.
(** Solution: utilisation de lgalité Coq pour "caster"
les annotations de longueur de nos vecteurs. *)
Print eq.
Definition Vcast {A} {n} {m} (v: vect A n)(h : n = m) : vect A m :=
match h with
| eq_refl => v
end.
Require Import Arith.
SearchPattern (_ + 1 = _). (* C'est [Nat.add_1_r] qu'il nous faut *)
Fixpoint Vrev {A} {n} (v:vect A n) : vect A n :=
match v with
| Vnil => Vnil
| Vcons x v => Vcast (Vapp (Vrev v) (Vcons x Vnil)) (Nat.add_1_r _)
end.
(** Souci: la présence de [Nat.add_1_r] bloque le calcul
(on dit qu'il s'agit d'une preuve "opaque"). *)
Compute Vrev (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).
(** Solution : faire une preuve "transparente", ou s'embeter
un peu plus lors de la définition du [Vcast]. *)
Lemma add_1_r n : n + 1 = S n.
Proof.
induction n; simpl; trivial. now f_equal.
Defined. (** Et pas Qed ! *)
Fixpoint Vrev' {A} {n} (v:vect A n) : vect A n :=
match v with
| Vnil => Vnil
| Vcons x v => Vcast (Vapp (Vrev' v) (Vcons x Vnil)) (add_1_r _)
end.
Compute Vrev' (Vcons 1 (Vcons 2 (Vcons 3 Vnil))).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment