\documentclass[a4paper]{article} \usepackage{epsfig} \psfigdriver{dvips} \usepackage[francais]{babel} \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{vmargin} % redéfinir les marges \setmarginsrb{2cm}{2cm}{2cm}{2cm}{0cm}{0cm}{0cm}{1cm} % Marge gauche, haute, droite, basse; espace entre la marge et le texte à % gauche, en haut, à droite, en bas \usepackage{verbatim} \usepackage{url} \usepackage{amsmath,amssymb} \title{Tactique réflexive de dérivation formelle\thanks{Mastère Parisien de Recherche en Informatique (MPRI, \protect\url{http://mpri.master.univ-paris7.fr}), année 2005--2006, cours 2-7-2~: «Assistants de preuve»}} \author{Tahina \textsc{Ramananandro} \\ École Normale Supérieure -- \textsc{Paris}} \date{16 février 2006} \newtheorem{defin}{Définition}[section] \newtheorem{theo}{Théorème}[section] \begin{document} \maketitle \section{Objectifs} On veut écrire une fonction de dérivation formelle, \texttt{deriv}, dans un langage restreint de fonctions de R dans R, puis prouver la correction du dérivateur formel, i.e. qu'il est conforme avec la définition. \begin{defin}[Correction de l'algorithme \texttt{deriv}] On dit que l'algorithme \texttt{deriv} est correct sur le langage de fonctions $\mathcal L$ si, et seulement si, pour tout $f$ terme du langage de fonctions $\mathcal L$, on a : \[ \forall x \in \mathbb R, \forall \epsilon > 0, \exists \delta > 0, \forall h \in \rbrack 0, \delta \lbrack : \\ \frac { \mathbb \lbrack f \mathbb \rbrack (x + h) - \mathbb \lbrack f \mathbb \rbrack (x) }{ h } - \mathbb{\lbrack} \texttt{deriv} f \mathbb \rbrack (x) < \epsilon \] où $\mathbb \lbrack . \mathbb \rbrack$ est une fonction d'interprétation du langage $\mathcal L$ vers les fonctions de $\mathbb R$ dans $\mathbb R$, vérifiant $\lbrack f + g \rbrack := \lbrack f \rbrack + \lbrack g \rbrack$, etc. \end{defin} On utilise pour cela le système d'aide à la preuve (ou \emph{assistant de preuve}) Coq\footnote{\url{http://coq.inria.fr}}. Le but de ce projet est non seulement de nous familiariser avec la preuve de théorèmes en Coq (avec en particulier l'utilisation de la \emph{librairie standard} de Coq, contenant une formalisation des réels dans les modules \texttt{Reals} et associés), mais aussi avec le langage de \emph{tactiques} $\mathcal L _{tac}$ du système Coq. On se reportera au sujet du projet, par Bruno \textsc{Barras}\footnote{\url{http://pauillac.inria.fr/~barras/mpri/projet.ps}}, pour les objectifs détaillés. ~ Les fichiers source Coq constituant le travail que j'ai réalisé pour ce projet sont disponibles sur mon site web\footnote{\url{http://www.eleves.ens.fr/home/ramanana/travail/coqderiv/}}. \section{Fonctions infiniment dérivables en tout point (\texttt{derivation\_formelle.v})} Dans un premier temps, on considère un langage décrivant les fonctions que l'on peut obtenir avec : \begin{itemize} \item l'identité, les fonctions constantes, le sinus, le cosinus, l'exponentielle \item somme, différence, produit, composition et élévation à une puissance constante (au sens du produit $\times$)\footnote{Dans le sujet, on parle de «puissance de fonctions». Cette notion est ambiguë \emph{a priori}, car elle peut être vue de trois façons : \begin{itemize} \item la puissance $f^g$ de deux fonctions est définie comme $x \mapsto \exp (g(x) \ln f(x))$. Cette quantité n'est pas toujours définie (que se passe-t-il si $f(x) < 0$ ?) \item la puissance $f^n$ en tant qu'itérée $n$-ième de fonctions (i.e. au sens de la composition $\circ$) est définie sur tout $\mathbb R$ si $f$ l'est. Cependant, la dérivée d'une telle fonction est $x \mapsto \prod_{i=0}^{n-1}{f'(f^i(x))}$ (notation puissance toujours au sens de $\circ$, mais produit $\Pi$ au sens de $\times$), formule dont la preuve ne serait pas aisée ne serait-ce qu'à cause de sa représentation en Coq \item en revanche, la puissance $f^n$ au sens du produit $\times$, dont la dérivée est $x \mapsto n f'(x) f^{n-1}(x)$, est un objet beaucoup plus courant et la preuve est beaucoup plus simple, c'est pourquoi nous avons choisi cette interprétation de la puissance. \end{itemize}} de telles fonctions \end{itemize} Cela nous conduit à la définition suivante du type informatif inductif \texttt{fonction}, qui décrit donc en quelque sorte la \emph{grammaire} donnant la \emph{syntaxe} des termes du langage de fonctions considéré : \begin{verbatim} Inductive fonction : Set := | Id : fonction | Const : R -> fonction | Exp : fonction | Sin : fonction | Cos : fonction | Plus : fonction -> fonction -> fonction | Moins : fonction -> fonction -> fonction | Fois : fonction -> fonction -> fonction | Compo : fonction -> fonction -> fonction | Puiss : fonction -> nat -> fonction . \end{verbatim} Qui dit syntaxe dit \emph{sémantique}, et donc \emph{interprétation} des termes de ce langage vers les fonctions de $\mathbb R$ dans $\mathbb R$. Cette fonction d'interprétation est définie par récurrence sur la structure du terme du langage de fonctions : \begin{verbatim} Fixpoint interp (f : fonction) : R -> R := match f with | Id => fun x => x | Const k => fun _ => k | Exp => exp | Sin => sin | Cos => cos | Plus g h => fun x => interp g x + interp h x | Moins g h => fun x => interp g x - interp h x | Fois g h => fun x => interp g x * interp h x | Compo g h => fun x => interp g (interp h x) | Puiss f n => fun x => pow (interp f x) n end. \end{verbatim} L'algorithme de dérivation formelle est également défini par récurrence structurelle : \begin{verbatim} Fixpoint deriv (f : fonction) : fonction := match f with | Id => Const 1 | Const _ => Const 0 | Exp => Exp | Sin => Cos | Cos => Moins (Const 0) Sin | Plus g h => Plus (deriv g) (deriv h) | Moins g h => Moins (deriv g) (deriv h) | Fois g h => Plus (Fois (deriv g) h) (Fois g (deriv h)) | Compo g h => Fois (Compo (deriv g) h) (deriv h) | Puiss f O => Const 0 | Puiss f (S n) => Fois (Fois (Const (INR (S n))) (deriv f)) (Puiss f n) end. \end{verbatim} Le théorème de correction s'énonce alors très simplement : \begin{verbatim} Theorem deriv_correcte : forall (f : fonction) (x : R), derivable_pt_lim (interp f) x (interp (deriv f) x). \end{verbatim} On le prouve par induction sur la structure du terme $f$ du langage de fonctions. Les cas du sinus, cosinus,\dots sont déjà montrés, en quelque sorte, dans la librairie standard (théorèmes \texttt{derivable\_pt\_lim\_sin}, \texttt{derivable\_pt\_lim\_cos}\dots qu'il suffit d'appliquer immédiatement). Ceux des constantes et de l'identité aussi, mais j'ai choisi de traiter ces deux cas à la main. Pour les termes plus complexes comme la somme, on se ramène à appliquer des théorèmes comme \texttt{derivable\_pt\_lim\_plus} et on utilise l'hypothèse d'induction. La puissance constitue un cas particulier : comme le théorème n'est prédéfini que pour la fonction puissance elle-même, $x \mapsto x^n$, je suis obligé de dire que $f^n$ est en fait la composée $(x \mapsto x^n) \circ f$, et d'utiliser alors les deux théorèmes prédéfinis, celui pour la fonction puissance et celui pour la composée. ~ Ce \emph{background} théorique sur la correction de la fonction de dérivation formelle étant jeté, il s'agit maintenant d'écrire une tactique permettant d'\emph{automatiser} le calcul de la dérivée $f'$ d'une fonction $f$ \emph{a priori} quelconque (de $\mathbb R \rightarrow \mathbb R$) et l'ajout direct en cours de démonstration (sans avoir aucune preuve supplémentaire à faire) d'une hypothèse correspondante. Il s'agit donc de traduire $f$ en un terme $h$ du langage de fonctions s'interprétant sur $f$, afin de calculer la dérivée de $f$ de manière automatique en utilisant l'algorithme de dérivation formelle dont on a montré la correction. J'ai choisi de distinguer la tactique d'«inversion» d'une fonction $f$, cette étape étant \emph{a priori} indépendante de la dérivation (elle pourrait être intéressante pour d'autres manipulations) : \begin{verbatim} Ltac inversion_fonction f := match constr:f with | (comp ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Compo g1 g2) | (plus_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Plus g1 g2) | (minus_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Moins g1 g2) | (mult_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Fois g1 g2) | (pow_fct ?f ?m) => let g := inversion_fonction f in constr:(Puiss g m) | exp => constr:Exp | sin => constr:Sin | cos => constr:Cos | id => constr:Id | (fun x => x) => constr:Id | (fun _ => ?y) => constr:(Const y) | fct_cte ?x => constr:(Const x) | (fun x => ?f x) => inversion_fonction f end. \end{verbatim} \noindent\textbf{Remarque : } L'intérêt de $\mathcal L_{tac}$ est de pouvoir analyser la structure de n'importe quel terme \emph{a priori} (plus familièrement, «faire du \emph{pattern-matching}»). Cependant, à l'heure actuelle (2006 : Coq 8.0), ce langage de tactiques n'est pas assez puissant car l'analyse «sous les \verb+fun+» est très limitée. Par exemple, si j'écris directement la fonction que je veux analyser comme ceci : \verb-fun x => cos x + sin (x + Pi)-, alors je n'aurai aucun moyen de reconnaître des «sous-termes sous le contexte [\verb+x+]», c'est-à-dire qu'en pratique je ne pourrai pas isoler les deux parties \verb-cos x- et \verb-sin (x + Pi)-.\footnote{Il ressort d'une discussion avec Jean-Christophe \textsc{Filliâtre} (\url{http://www.lri.fr/~filliatr}), que l'on pourrait éventuellement étendre les capacités de $\mathcal L_{tac}$ en en écrivant «des bouts en ML», c'est-à-dire en intégrant du code OCaml (\url{http://caml.inria.fr/ocaml}) qui pourrait effectuer une telle analyse sous les \texttt{fun} en manipulant les termes à plus bas niveau. Mais par manque de temps, je n'ai pas pu développer cette approche.} Je dois donc entrer cette fonction sous une forme moins lisible : \texttt{plus\_fct cos (comp sin (plus\_fct id (fct\_cte Pi)))}. ~ J'intègre ensuite cette étape d'«interprétation à l'envers» dans la tactique de dérivation, qui, moyennant quelques réécritures, rajoute une hypothèse sur $f$ et sa dérivée, grâce à l'application du théorème de correction : \begin{verbatim} Ltac derive f := let f0 := inversion_fonction f in let h := fresh "h" in ( assert (h: forall y, derivable_pt_lim f y (interp (deriv f0) y)); [ apply (deriv_correcte f0) | simpl in h ] ). \end{verbatim} \section{Fonctions dérivables sur un sous-ensemble de $\mathbb R$ \\ (\texttt{derivation\_formelle\_avec\_domaine.v})} ~ L'objectif de cette partie est d'intégrer au développement (c'est-à-dire, en l'occurrence, de dériver) des fonctions non dérivables en tout point : logarithme, valeur absolue, division, inverse. Il faut donc définir, en plus d'un algorithme de dérivation formelle, un algorithme de «dérivabilité», en fait de détermination d'une condition \emph{suffisante} de dérivabilité. ~ Alors que dans le développement précédent, j'avais défini le terme \texttt{Moins} dans la grammaire, ici je considère plutôt des termes \texttt{Oppose} et \texttt{Inverse}, et je redéfinis \texttt{Moins} et \texttt{Sur} comme du \emph{sucre syntaxique} : \begin{verbatim} Inductive fonction : Set := | Const : R -> fonction | Id : fonction | Exp : fonction | Sin : fonction | Cos : fonction | Log : fonction | Valeur_absolue : fonction | Racine : fonction | Oppose : fonction -> fonction | Inverse : fonction -> fonction | Plus : fonction -> fonction -> fonction | Fois : fonction -> fonction -> fonction | Compo : fonction -> fonction -> fonction | Puiss : fonction -> nat -> fonction . Definition Moins f g := Plus f (Oppose g). Definition Sur f g := Fois f (Inverse g). \end{verbatim} Ce choix pour \texttt{Moins} et \texttt{Sur} est d'ailleurs proche de la méthode que l'on rencontre dans la librairie standard de Coq, pour la définition par exemple de \texttt{Rminus} et \texttt{Rdiv}, fondée sur les préexistants \texttt{Ropp} et \texttt{Rinv}. Alors, la fonction d'interprétation est définie par récurrence sur la structure des termes de la grammaire, et je montre, \emph{à côté} de cette définition, les propriétés immédiates que l'on attend pour les sucres syntaxiques \texttt{Moins} et \texttt{Sur}. \begin{verbatim} Fixpoint interp (f : fonction) : R -> R := match f with | Id => id | Const k => fct_cte k | Exp => exp | Sin => sin | Cos => cos | Racine => sqrt | Valeur_absolue => Rabs | Log => ln | Oppose f => opp_fct (interp f) | Inverse f => inv_fct (interp f) | Plus g h => plus_fct (interp g) (interp h) | Fois g h => mult_fct (interp g) (interp h) | Compo g h => comp (interp g) (interp h) | Puiss g n => fun x => pow (interp g x) n end. Theorem interp_moins : forall f g, interp (Moins f g) = minus_fct (interp f) (interp g). auto with real. Qed. Theorem interp_sur : forall f g, interp (Sur f g) = div_fct (interp f) (interp g). auto with real. Qed. \end{verbatim} \noindent\textbf{Remarque : } contrairement au développement précédent, j'ai choisi d'utiliser les fonctions prédéfinies \texttt{plus\_fct}, etc. au lieu des structures \texttt{fun}. En effet, ce choix m'a permis d'alléger la preuve du théorème de correction de l'algorithme de dérivation : moins de réécritures, car c'est sous cette forme que sont formulés les théorèmes de dérivation dans la librairie standard. ~ Alors, l'algorithme de dérivation formelle s'écrit à nouveau par récurrence sur la structure du terme du langage de fonctions : \begin{verbatim} Fixpoint deriv (f : fonction) : fonction := match f with | Id => Const 1 | Const _ => Const 0 | Exp => Exp | Sin => Cos | Cos => Oppose Sin | Racine => Inverse (Fois (Const 2) Racine) | Log => Inverse Id | Valeur_absolue => Sur Id Valeur_absolue | Oppose g => Oppose (deriv g) | Inverse g => Oppose (Sur (deriv g) (Fois g g)) | Plus g h => Plus (deriv g) (deriv h) | Fois g h => Plus (Fois (deriv g) h) (Fois g (deriv h)) | Compo g h => Fois (Compo (deriv g) h) (deriv h) | Puiss f O => Const 0 | Puiss f (S n) => Fois (Fois (Const (INR (S n))) (deriv f)) (Puiss f n) end. \end{verbatim} Avec l'arrivée de fonctions comme la valeur absolue, il faut parler des \emph{domaines de dérivabilité} des fonctions considérées. La connaissance de ces domaines, bien qu'inutile pour l'algorithme de dérivation lui-même, est en revanche nécessaire pour montrer sa correction. C'est pourquoi ces domaines sont exprimés par des prédicats $P$ d'une variable réelle (\texttt{R -> Prop}). Ils sont définis par induction sur la structure du terme de fonction. \begin{verbatim} Inductive derivable : fonction -> R -> Prop := | derivable_id : forall (x : R), derivable Id x | derivable_const : forall (x y : R), derivable (Const y) x | derivable_exp : forall (x : R), derivable Exp x | derivable_cos: forall (x:R), derivable Cos x | derivable_sin : forall (x : R), derivable Sin x | derivable_log : forall (x : R), x > 0 -> derivable Log x | derivable_racine : forall (f : fonction) (x : R), x > 0 -> derivable Racine x | derivable_valeur_absolue : forall (x : R), x <> 0 -> derivable Valeur_absolue x | derivable_oppose : forall (f : fonction) (x: R), derivable f x -> derivable (Oppose f) x | derivable_inverse : forall (f : fonction) (x: R), derivable f x -> interp f x <> 0 -> derivable (Inverse f) x | derivable_plus : forall (f g : fonction) (x : R), derivable f x -> derivable g x -> derivable (Plus f g) x | derivable_fois : forall (f g : fonction) (x : R), derivable f x -> derivable g x -> derivable (Fois f g) x | derivable_compo : forall (f g : fonction) (x : R), derivable f (interp g x) -> derivable g x -> derivable (Compo f g) x | derivable_puiss_O : forall (f : fonction) (x : R), derivable (Puiss f O) x | derivable_puiss_S : forall (f : fonction) (x : R) (n : nat), derivable f x -> derivable (Puiss f (S n)) x . \end{verbatim} Il s'agit là de \emph{conditions suffisantes} de dérivabilité : pour $x$ réel, si $P(x)$ est vraie, alors la fonction est dérivable en $x$. Mais ces conditions ne sont pas toujours également nécessaires. En effet, dans le cas général la fonction $f \times g$ est dérivable en $x$ dès que $f$ et $g$ le sont en $x$, condition que l'on trouvera algorithmiquement avec l'aide de la définition ci-dessus. En revanche, des fonctions comme $x \mapsto 0 \times |x|$ sont dérivables en tout point (alors que $|.|$ n'est pas dérivable en 0), mais pour le découvrir algorithmiquement, il aurait peut-être fallu raffiner la définition de \texttt{derivable} en «poussant» un petit peu plus l'analyse. ~ La correction de l'algorithme de dérivation formelle s'énonce donc simplement en intégrant ces conditions suffisantes de dérivabilité : \begin{verbatim} Theorem deriv_correcte : forall (f : fonction) (x : R), derivable f x -> derivable_pt_lim (interp f) x (interp (deriv f) x). \end{verbatim} On le prouve également par induction sur la structure du terme $f$. Lorsque j'ai besoin d'utiliser l'hypothèse d'induction, j'ai besoin de connaître l'hypothèse de dérivabilité pour un sous-terme de $f$. Je peux obtenir cette hypothèse grâce à la tactique \texttt{inversion} appliquée à l'hypothèse \texttt{derivable f x}. Moyennant la prise en compte de cette nouvelle hypothèse de dérivabilité, la preuve s'effectue comme avant grâce aux théorèmes de la librairie standard, sauf pour l'inverse d'une fonction, pour laquelle il n'existe pas de théorème prédéfini : je suis obligé de me ramener à la division en passant de \texttt{inv\_fct h} à \texttt{div\_fct (fct\_cte 1) h} (qui ne sont pas convertibles car il faut un théorème\footnote{En l'occurrence : le fait que 1 soit neutre pour $\times$\dots} en plus d'un dépliage de définition pour aller de l'un à l'autre), afin d'utiliser le théorème existant \texttt{derivable\_pt\_lim\_div}. ~ L'arrivée des fonctions supplémentaires étend la définition de la tactique de traduction («interprétation inverse») des fonctions de \texttt{R -> R} : \begin{verbatim} Ltac inversion_fonction f := match constr:f with | (plus_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Plus g1 g2) | (minus_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Moins g1 g2) | (mult_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Fois g1 g2) | (pow_fct ?f ?m) => let g := inversion_fonction f in constr:(Puiss g m) | (div_fct ?f1 ?f2) => let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Sur g1 g2) | (inv_fct ?f) => let g := inversion_fonction f in constr:(Inverse g) | (opp_fct ?f) => let g := inversion_fonction f in constr:(Oppose g) | exp => constr:Exp | sin => constr:Sin | cos => constr:Cos | ln => constr:Log | Rabs => constr:Valeur_absolue | sqrt => constr:Racine | (fun x => x) => constr:Id | id => constr:Id | (fun _ => ?x) => constr:(Const x) | fct_cte ?x => constr:(Const x) | (fun x => ?f x) => inversion_fonction f (* eta-conversion *) end. \end{verbatim} Si cette extension est simple, en revanche, l'introduction des prédicats de dérivabilité corse le problème de la dérivation automatique. Certes, si la tactique est quasi inchangée : \begin{verbatim} Ltac eta_contraction f := match f with | (fun x => ?g x) => eta_contraction g | _ => constr:f end. Ltac derive f p := let f1 := eta_contraction f in let f0 := inversion_fonction f1 in let g0 := constr:(interp (deriv f0)) in let h := fresh "h" in ( assert (h: forall x : R, p x -> derivable_pt_lim f1 x (g0 x)) ; [ intro x ; intro ; apply (deriv_correcte f0 x) ; auto | simpl in h] ). \end{verbatim} La dérivation automatique n'est plus guère possible. Si par exemple on exécute la tactique : \begin{verbatim} derive (div_fct (fct_cte 2) (fct_cte 2)) (fun _:R => True). \end{verbatim} alors on se retrouve avec le but à prouver : \begin{verbatim} derivable (Sur (Const 2) (Const 2) x) \end{verbatim} qui, avec l'utilisation de la définition inductive de \texttt{derivable}, amène à prouver que $2 \neq 0$\dots \section{Variables de fonctions (\texttt{derivation\_formelle\_varmap.v})} Cette fois-ci, on veut étendre notre langage de fonctions avec des variables\footnote{Il ne s'agit pas des variables de Coq, mais d'un concept de variables au sein du langage de fonctions}. Donc, lorsque l'on voudra interpréter ces termes de fonctions avec variables, il faudra joindre à notre terme une \emph{valuation}. Cette valuation prend la forme d'un \emph{arbre} (le type \texttt{varmap}) dont les noeuds sont étiquetés par des fonctions de \texttt{R -> R}. Dans les termes, les variables (type \texttt{index}) sont en fait les \emph{chemins} qu'il faudra suivre dans l'arbre lors de l'interprétation, pour trouver la fonction correspondante. \begin{verbatim} Inductive fonction : Set := ... | Var : index -> fonction . \end{verbatim} Du coup, un problème majeur s'est posé : que se passe-t-il si je tente d'interpréter une fonction dans une valuation incomplète ? En d'autres termes, si une variable représente un chemin inexistant dans l'arbre ? J'ai d'abord souhaité écrire une fonction d'interprétation partielle, en considérant plusieurs solutions : \begin{itemize} \item \emph{La fonction d'interprétation renvoie un type somme : la fonction interprétée, ou bien une variable dans le terme qui n'a pas pu être instanciée (en guise d'indication d'erreur).} Cette solution alourdit considérablement les preuves ; en outre, elle aboutit au problème grave suivant. Considérons que j'applique une transformation $T$ aux variables d'un terme $f$ (par exemple, rajouter un pas vers la gauche), et que l'arbre de valuation $A$ initial subisse une transformation $T'$ compatible avec $T$ (c'est-à-dire telle que pour toute variable $i$, l'élément de chemin $T(i)$ dans $T'(A)$ soit le même que l'élément de chemin $i$ dans $A$). Alors je souhaite que l'interprétation de $T(f)$ sous la valuation $T'(A)$ soit la même que l'interprétation de $f$ sous $A$. Mais ceci est faux si $f$ a des variables non instanciées sous $A$, car les variables renvoyées en indication d'erreur ne sont pas les mêmes. \item \emph{La fonction d'interprétation renvoie un type option : la fonction interprétée, ou rien si une variable dans le terme n'a pas pu être instanciée.} Cette solution alourdit tout autant les preuves. Certes, elle permet de contourner le problème posé par la solution précédente, mais elle nécessite d'écrire les théorèmes de la forme \texttt{interp v f = Some h -> \dots}, ce qui pose des problèmes de convertibilité (que je n'ai pas vu venir, alors qu'ils auraient aussi été soulevés par la solution précédente) : j'ai abouti à \texttt{Some h = Some (-f) -> Some f = Some (-h)}, ce qui est bien sûr indémontrable. Introduire alors une notion d'équivalence de fonctions (égalité en tout point) rend le développement rigoureusement illisible à ce niveau. \item \emph{La fonction d'interprétation dépend d'un prédicat inductif dit d'«interprétabilité» (i.e. toutes les variables de la fonction sont instanciées sous la valuation considérée), et est construite par induction sur la structure de la preuve de ce prédicat pour la fonction à interpréter.} Cette solution alourdit les preuves encore plus que les deux précédentes (ne serait-ce que la définition de la fonction d'interprétation, avec \texttt{Definition \dots Defined} et en mode preuve plutôt qu'avec \texttt{Fixpoint}), et les raisonnements font apparaître les fonctions d'induction et de récursion \texttt{interpretable\_rec}, etc. ce qui est très malcommode. \end{itemize} J'ai donc revu mes ambitions à la baisse, et j'ai préféré définir une fonction d'interprétation \emph{a priori} totale, associant la fonction nulle à toute variable non instanciée. Pourquoi la fonction nulle ? Car, supposant (généreusement) que si une variable n'est pas instanciée sous une certaine valuation, sa «dérivée» ne l'est pas non plus dans la valuation où on va interpréter la dérivée de la fonction, il faut trouver une fonction dont la dérivée soit elle-même\footnote{Les fonctions $k \exp$ conviennent donc --tiens, même en informatique on doit résoudre des équations différentielles !--, mais il est extrêmement peu naturel de prendre $k \neq 0$ ; voir par exemple les langages BASIC qui instancient par défaut à 0 toutes les variables numériques non définies.}. \begin{verbatim} Fixpoint interp (v : varmap (R -> R)) (f : fonction) {struct f} : (R -> R) := match f with | Id => id | Const k => (fct_cte k) | Exp => exp | Sin => sin | Cos => cos | Racine => sqrt | Valeur_absolue => Rabs | Log => ln | Oppose g => opp_fct (interp v g) | Inverse g => inv_fct( interp v g ) | Plus g h => plus_fct (interp v g) (interp v h) | Fois g h => mult_fct (interp v g) (interp v h) | Compo g h => comp (interp v g) (interp v h) | Puiss g n => fun x => pow (interp v g x) n | Var x => varmap_find (fct_cte 0) x v end. \end{verbatim} On veut que si $f$ s'interprète dans une valuation $v$, alors sa dérivée $f'$ s'interprète dans une valuation $V = \texttt{Node\_vm} ~ \alpha ~ v ~ v'$, où $\alpha$ est arbitraire et $v'$ est une valuation telle que pour toute variable $i$, une fonction de chemin $i$ dans $v$ soit interprétée avec une fonction de chemin $i$ dans $v'$. Fixons deux telles valuations $v$ et $v'$. Considérons deux variables $i$ et $j$ instanciées dans $v$ et $v'$. Alors la fonction $i \times j$ admet une interprétation dans $v$. Dériver cette fonction naïvement donnerait alors $i' \times j + i \times j'$, avec encore les variables $i$ et $j$ présentes, mais à interpréter dans $V$ et non dans $v$. C'est absurde. En fait, on aurait voulu remplacer $i$ par $\texttt{Left\_idx} ~ i$, c'est-à-dire rajouter un pas vers la gauche devant le chemin représenté par $i$, ce pas vers la gauche permettant de passer de $V$ à son sous-arbre gauche $v$ où on pourra instancier la variable représentée par le reste du chemin, à savoir $i$. Cela nécessite donc que, avant de dériver formellement $f$, on modifie toutes ses variables en leur rajoutant un pas vers la gauche. On dit que l'on va «gauchir» f : \begin{verbatim} Fixpoint gauchir (f : fonction) : fonction := match f with | Var v => Var (Left_idx v) | Oppose g => Oppose (gauchir g) | Inverse g => Inverse (gauchir g) | Plus g h => Plus (gauchir g) (gauchir h) | Fois g h => Fois (gauchir g) (gauchir h) | Compo g h => Compo (gauchir g) (gauchir h) | Puiss g n => Puiss (gauchir g) n | e => e end. \end{verbatim} Alors, je montre que si j'interprète une fonction $f$ dans une varmap $v$, j'obtiens le même résultat qu'en interprétant $\texttt{gauchir} ~ f$ dans une varmap $\texttt{Node\_vm} ~ \alpha ~ v ~ z$, avec $\alpha$ et $z$ arbitraires. Cette égalité me servira plusieurs fois dans la suite. \begin{verbatim} Theorem gauchir_correcte : forall f v bidon_f bidon_v, interp v f = interp (Node_vm bidon_f v bidon_v) (gauchir f). \end{verbatim} On notera que cette égalité est vraie même si $f$ contient des variables non instanciées dans $v$. ~ Revenant au cas général, on veut alors que $i'$ renvoie, dans $V$, à la dérivée de la fonction de chemin $i$ dans $v$. Or, cette dérivée admet un chemin $i$ dans $v'$, et $v'$ est le sous-arbre droit de $V$. Donc on a $i' = \texttt{Right\_idx} ~ i$. C'est-à-dire que, dans $\texttt{gauchir} ~ f$, où $i$ est remplacée par $\texttt{Left\_idx} ~ i$ , il suffit de modifier toutes les variables en changeant leur premier pas, qui est un pas vers la gauche, en un pas vers la droite. D'où la définition suivante de la dérivation formelle \texttt{deriv}, qui s'appuie sur \texttt{derivg}, fonction supposant que son entrée est «gauche» (i.e. a toutes ses variables commençant par un pas vers la gauche) et effectuant l'opération ci-dessus ainsi que toutes les autres dérivations formelles «classiques». \begin{verbatim} Fixpoint derivg (f : fonction) : fonction := match f with | Id => Const 1 | Const _ => Const 0 | Exp => Exp | Sin => Cos | Cos => Oppose Sin | Racine => (Inverse (Fois (Const 2) Racine)) | Log => Inverse Id | Valeur_absolue => Sur Id Valeur_absolue | Oppose g => Oppose (derivg g) | Inverse g => Oppose (Sur (derivg g) (Fois g g)) | Plus g h => Plus (derivg g) (derivg h) | Fois g h => Plus (Fois (derivg g) h) (Fois g (derivg h)) | Compo g h => Fois (Compo (derivg g) h) (derivg h) | Puiss _ O => Const 0 | Puiss g (S n) => Fois (Fois (Const (INR (S n))) (derivg g)) (Puiss g n) | Var (Left_idx i) => Var (Right_idx i) | Var v => Var v end. Definition deriv f := derivg (gauchir f). \end{verbatim} On ne s'occupe pas du comportement de \texttt{derivg} sur une variable qui ne commencerait pas par un pas vers la gauche. ~ Les domaines de dérivabilité posent également problème. L'arrivée des variables exige que la condition suffisante de dérivabilité dépende non pas d'une mais de \emph{deux} valuations : \begin{itemize} \item la valuation $v$ pour pouvoir instancier les variables : en effet, par exemple pour exprimer la condition de dérivabilité de l'inverse d'une fonction, on a besoin de son interprétation. Plus simplement, si $i$ est une variable quelconque, la dérivabilité de $1/i$ dépend de la valeur de $i$, et donc de la valuation $v$ \item une valuation $u$ de prédicats ($u$ de type \texttt{varmap (R -> Prop)}), telle que pour tout chemin $i$, si le prédicat de chemin $i$ dans $u$ est vrai en $x$ réel, alors la fonction de chemin $i$ dans $v$ est dérivable en $x$ \end{itemize} Ayant introduit une nouvelle valuation $u$, il faut s'attacher à ce qui peut arriver si $i$ n'est pas un chemin valide dans $u$. En fait, dans ce cas, on considère que le prédicat de dérivabilité est \texttt{False}. En effet, c'est la condition suffisante la plus faible dont on dispose ; elle convient toujours. \begin{verbatim} Inductive derivable (v : varmap (R -> Prop)) (w : varmap (R -> R)) : fonction -> R -> Prop := | derivable_id : forall (x : R), derivable v w Id x | derivable_const : forall (x y : R), derivable v w (Const y) x | derivable_exp : forall (x : R), derivable v w Exp x | derivable_cos: forall (x:R), derivable v w Cos x | derivable_sin : forall (x : R), derivable v w Sin x | derivable_log : forall (x : R), x > 0 -> derivable v w Log x | derivable_racine : forall (f : fonction) (x : R), x > 0 -> derivable v w Racine x | derivable_valeur_absolue : forall (x : R), x <> 0 -> derivable v w Valeur_absolue x | derivable_oppose : forall (f : fonction) (x: R), derivable v w f x -> derivable v w (Oppose f) x | derivable_inverse : forall (f : fonction) (x: R), derivable v w f x -> interp w f x <> 0 -> derivable v w (Inverse f) x | derivable_plus : forall (f g : fonction) (x : R), derivable v w f x -> derivable v w g x -> derivable v w (Plus f g) x | derivable_fois : forall (f g : fonction) (x : R), derivable v w f x -> derivable v w g x -> derivable v w (Fois f g) x | derivable_compo : forall (f g : fonction) (x : R), derivable v w f (interp w g x) -> derivable v w g x -> derivable v w (Compo f g) x | derivable_puiss_O : forall (f : fonction) (x : R), derivable v w (Puiss f O) x | derivable_puiss_S : forall (f : fonction) (x : R) (n : nat), derivable v w f x -> derivable v w (Puiss f (S n)) x | derivable_var : forall (i : index) (x : R), varmap_find (fun _=>False) i v x -> derivable v w (Var i) x . \end{verbatim} Le théorème de correction de l'algorithme de dérivation formelle s'écrit alors (les noms des variables ayant changé, $v$ désignant la valuation des prédicats de dérivabilité, $w$ la valuation des fonctions et $w'$ celle des dérivées) : \begin{verbatim} Theorem deriv_correcte : forall (f : fonction) (w w' : varmap (R->R)) (v : varmap (R -> Prop)) (x : R), derivable v w f x -> (forall (i:index), forall x : R, varmap_find (fun _=>False) i v x -> derivable_pt_lim (interp w (Var i)) x (interp w' (Var i) x)) -> forall (bidon_fonct : R -> R), derivable_pt_lim (interp w f) x (interp (Node_vm bidon_fonct w w') (deriv f) x). \end{verbatim} Il exige les hypothèses suivantes : \begin{itemize} \item $f$ est dérivable sous la valuation $v$ des prédicats de dérivabilité et la valuation $w$ d'interprétation des fonctions \item pour tout chemin $i$, toute fonction de chemin $i$ dans $w$ se dérive, en $x$ réel, en la valeur en $x$ de la fonction de chemin $i$ dans $w'$, sous la condition suffisante indiquée par le prédicat de chemin $i$ dans $v$ \end{itemize} La preuve (par induction sur la structure de $f$) n'est guère plus compliquée que dans les développements précédents, si ce n'est quelques réécritures supplémentaires. Il se rajoute le cas de la variable, qui somme toute est vite traité : grâce à la tactique \texttt{inversion} sur l'hypothèse $f$ dérivable, j'obtiens que la condition suffisante indiquée par la valuation $v$ est vérifiée, ce qui me permet d'utiliser l'autre hypothèse du théorème. Il est à noter que ce théorème reste vrai même si les variables ne sont pas instanciées dans les valuations considérées. ~ L'introduction des variables permet le traitement automatique de \emph{toutes} les fonctions. En effet, jusque-là, les tactiques d'inversion de fonctions échouaient lorsque l'on indiquait des fonctions non reconnues : elles ne passaient pas le \emph{pattern-matching}. Maintenant, il est possible de les prendre en compte en les intégrant aux valuations au fur et à mesure que l'on analyse la structure de la fonction. ~ On voudrait construire des arbres «équilibrés». À première vue, cette notion n'a pas grand sens, s'agissant d'arbres de fonctions, éléments dépourvus d'ordre total. Mais on veut simplement construire les arbres de façon à assurer un accès indexé \emph{logarithmique} en la taille de l'arbre (i.e. en le nombre de fonctions dans la valuation). Voilà ce qui motive le choix de l'arbre plutôt que de la liste, dont le temps d'accès est linéaire.\footnote{En Coq, il n'existe pas de «tableau», dont l'accès serait constant.} On voudrait remplir l'arbre «ligne par ligne». En programmation pratique, on peut écrire des algorithmes efficaces de construction en mémorisant un pointeur vers la prochaine «case libre». Mais n'oublions pas que $\mathcal L_{tac}$ est purement fonctionnel\footnote{C'est pourquoi la tactique \texttt{auto}, utilisant les bases de \texttt{Hint}, n'est pas exprimable en $\mathcal L_{tac}$.}. On pourrait prendre une approche «monadique» (i.e. prendre l'ancien pointeur en entrée et renvoyer le nouveau en sortie), mais ce serait plutôt lourd à écrire. Mon algorithme de construction par ajouts successifs n'utilise donc ni pointeurs ni monades. Pour ajouter un objet $o$ à un arbre $A$ : \begin{enumerate} \item si $A$ est vide, je le rajoute à sa racine \item sinon, soient $g$ et $d$ ses sous-arbres gauche et droit. Je regarde si $g$ est complet. \item si $g$ n'est pas complet, alors j'ajoute récursivement $o$ à $g$ \item sinon, je regarde si $d$ est complet. S'il ne l'est pas, alors j'ajoute récursivement $o$ à $d$ \item sinon, $g$ et $d$ sont complets. Dans ce cas, je compare la taille de $g$ et de $d$, en mesurant leur hauteur, et j'ajoute récursivement $o$ au plus petit des deux. \end{enumerate} Or, vérifier qu'un arbre est complet est linéaire en la taille de l'arbre (en gros, on compte ses éléments). Donc, mon algorithme est clairement sous-optimal : chaque ajout est linéaire. On sacrifie donc la construction, linéaire, à l'accès, logarithmique. \begin{verbatim} Ltac gauche_plus_grand g d := match constr:g with | Empty_vm _ => constr:False | Node_vm _ ?g2 _ => match constr:d with | Empty_vm _ => constr:True | Node_vm _ ?d2 _ => gauche_plus_grand g2 d2 end end. Ltac complet v := match constr:v with | Empty_vm _ => constr:True | Node_vm _ ?g ?d => match complet g with | True => complet d | False => constr:False end end. Ltac ajouter o v := match constr:v with | Empty_vm _ => constr:(Node_vm o (Empty_vm _) (Empty_vm _)) | Node_vm ?r ?g ?d => match complet g with | True => match complet d with | True => match gauche_plus_grand g d with | True => let d' := ajouter o d in constr:(Node_vm r g d') | False => let g' := ajouter o g in constr:(Node_vm r g' d) end | False => let d' := ajouter o d in constr:(Node_vm r g d') end | False => let g' := ajouter o g in constr:(Node_vm r g' d) end end. \end{verbatim} \noindent\textbf{Remarque : } il est possible de modifier légèrement la fonction d'ajout en rajoutant un cas de filtrage : \begin{verbatim} Ltac ajouter_sans_doublon o v := match constr:v with | Empty_vm _ => constr:(Node_vm o (Empty_vm _) (Empty_vm _)) | Node_vm o _ _ => constr:v | Node_vm ?r ?g ?d => ... \end{verbatim} \noindent En effet, $\mathcal L_{tac}$ permet de faire du \emph{pattern-matching} plus fort que ce que l'on pourrait faire par exemple en OCaml (sans les clauses \texttt{when}), puisqu'il nous permet de tester, en même temps que le filtrage, l'égalité de deux termes non constants désignés par des variables. En l'occurrence, on rajoute la clause permettant de filtrer un arbre dont la racine serait étiquetée par l'objet que l'on voudrait ajouter (et qui est donc déjà présent). ~ Disposant de primitives pour ajouter un élément dans un arbre, on peut alors écrire la fonction qui permet de compléter un arbre avec les fonctions non reconnues que l'on trouve dans la fonction $f$. L'idée est de rajouter dans l'arbre, systématiquement mais sans doublon, toute fonction inconnue : \begin{verbatim} Ltac completer v f := match constr:f with | (comp ?f1 ?f2) => let w := completer v f1 in completer w f2 | (plus_fct ?f1 ?f2) => let w := completer v f1 in completer w f2 | (minus_fct ?f1 ?f2) => let w := completer v f1 in completer w f2 | (mult_fct ?f1 ?f2) => let w := completer v f1 in completer w f2 | (pow_fct ?f ?m) => completer v f | (div_fct ?f1 ?f2) => let w := completer v f1 in completer w f2 | (inv_fct ?f) => completer v f | (opp_fct ?f) => completer v f | exp => constr:v | sin => constr:v | cos => constr:v | ln => constr:v | Rabs => constr:v | sqrt => constr:v | (fun x => x) => constr:v | id => constr:v | (fun _ => ?x) => constr:v | fct_cte ?x => constr:v | (fun x => ?f (?g x)) => let w := completer v f in completer w g (* eta-conversion avec composition *) | (fun x => ?f x) => completer v f (* eta-conversion simple *) | _ => ajouter_sans_doublon f v (* autres cas *) end. \end{verbatim} L'arbre des fonctions étant ainsi construit, il est alors possible d'étendre la tactique de traduction («interprétation inverse») en intégrant cet arbre. Cette tactique, s'appuie sur une tactique qui permet de rechercher une fonction dans l'arbre et de construire son index (i.e. le chemin qui y mène). \begin{verbatim} Ltac trouver f v := match constr:v with | Node_vm f _ _ => constr:End_idx | Node_vm _ ?g _ => let i := trouver f g in constr:(Left_idx i) | Node_vm _ _ ?d => let i := trouver f d in constr:(Right_idx i) | _ => fail "Une fonction n'a pu être trouvée dans la varmap. Complétez d'abord la varmap avant d'inverser la fonction." end. Ltac inversion_fonction v f := match constr:f with | (comp ?f1 ?f2) => let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Compo g1 g2) | (plus_fct ?f1 ?f2) => let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Plus g1 g2) | (minus_fct ?f1 ?f2) => let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Moins g1 g2) | (mult_fct ?f1 ?f2) => let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Fois g1 g2) | (pow_fct ?f ?m) => let g := inversion_fonction v f in constr:(Puiss g m) | (div_fct ?f1 ?f2) => let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Sur g1 g2) | (inv_fct ?f) => let g := inversion_fonction v f in constr:(Inverse g) | (opp_fct ?f) => let g := inversion_fonction v f in constr:(Oppose g) | exp => constr:Exp | sin => constr:Sin | cos => constr:Cos | ln => constr:Log | Rabs => constr:Valeur_absolue | sqrt => constr:Racine | (fun x => x) => constr:Id | id => constr:Id | (fun _ => ?x) => constr:(Const x) | fct_cte ?x => constr:(Const x) | (fun x => ?f (?g x)) => let k := constr:(comp f g) in inversion_fonction v k (* eta-conversion avec composition *) | (fun x => ?f x) => inversion_fonction v f (* eta-conversion simple *) | _ => let i := trouver f v in constr:(Var i) (* autres cas *) | _ => fail "Une fonction n'a pu être trouvée dans la varmap. Complétez d'abord la varmap avant d'inverser la fonction." end. \end{verbatim} Ces deux tactiques présentent la particularité suivante de posséder plusieurs branches filtrant exactement les mêmes termes. Elles ne sont pas redondantes, mais au contraire, exploitent une particularité de $\mathcal L_{tac}$, attrayante pour certains, déroutante pour d'autres, à savoir le \emph{backtracking} dans un filtrage : sachant qu'une séquence de tactiques peut échouer, si une branche de filtrage échoue, alors au lieu de faire échouer toute la tactique, on passe à la prochaine branche du filtrage, jusqu'à réussir, ou bien à épuiser toutes les branches, auquel cas toute la tactique échoue. Cet aspect pourrait être rapproché du fonctionnement de PROLOG. Cette particularité, que je trouve personnellement séduisante, devrait toutefois être doublée d'un mécanisme de \texttt{fail} (tactique pour faire échouer la séquence) plus «ergonomique», qui permettrait de placer des «points d'arrêt» dans les tactiques pour les déboguer (en les faisant échouer à des points précis). En l'état actuel des choses (2006, Coq 8.0), le contrôle des échecs, et donc du \emph{backtracking}, est encore difficile. ~ On remarque également que la structure de \texttt{inversion\_fonction} est très voisine de celle de \texttt{completer}, ce qui laisse penser que ces deux opérations auraient pu s'effectuer en même temps : \begin{verbatim} (* On a besoin d'un produit dans Type *) Inductive prod2 (A B : Type) : Type := | pair2 : A -> B -> prod2 A B. Implicit Arguments pair2. Ltac deux_en_un v f := match constr:f with | (comp ?f1 ?f2) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in match constr:k2 with | pair2 ?x ?g2 => constr:(pair2 x (Compo g1 g2)) end end | (plus_fct ?f1 ?f2) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in match constr:k2 with | pair2 ?x ?g2 => constr:(pair2 x (Plus g1 g2)) end end | (minus_fct ?f1 ?f2) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in match constr:k2 with | pair2 ?x ?g2 => constr:(pair2 x (Moins g1 g2)) end end | (mult_fct ?f1 ?f2) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in match constr:k2 with | pair2 ?x ?g2 => constr:(pair2 x (Fois g1 g2)) end end | (pow_fct ?f1 ?m) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => constr:(pair2 w (Puiss g1 m)) end | (div_fct ?f1 ?f2) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in match constr:k2 with | pair2 ?x ?g2 => constr:(pair2 x (Sur g1 g2)) end end | (inv_fct ?f1) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => constr:(pair2 w (Inverse g1)) end | (opp_fct ?f1) => let k1 := deux_en_un v f1 in match constr:k1 with | pair2 ?w ?g1 => constr:(pair2 w (Oppose g1)) end | exp => constr:(pair2 v Exp) | sin => constr:(pair2 v Sin) | cos => constr:(pair2 v Cos) | ln => constr:(pair2 v Log) | Rabs => constr:(pair2 v Valeur_absolue) | sqrt => constr:(pair2 v Racine) | (fun x => x) => constr:(pair2 v Id) | id => constr:(pair2 v Id) | (fun _ => ?x) => constr:(pair2 v (Const x)) | fct_cte ?x => constr:(pair2 v (Const x)) | (fun x => ?f (?g x)) => let k := constr:(comp f g) in deux_en_un v k (* eta-conversion avec composition *) | (fun x => ?f x) => deux_en_un v f (* eta-conversion simple *) | _ => (* sous-optimal : tenter d'ajouter f sans doublon puis séparément trouver son index dans la varmap obtenue *) let w := ajouter_sans_doublon f v in let i := trouver f w in constr:(pair2 w (Var i)) end. \end{verbatim} Certes, grâce à la construction de l'arbre des fonctions non reconnues, on arrive à capturer l'ensemble de toutes les fonctions réelles. Cependant, avec l'indétermination soulevée par l'apparition de valuations supplémentaires coup sur coup, l'automatisation du calcul s'arrête là : le calcul automatique de la dérivée est clairement impossible, puisque cela reviendrait à calculer les dérivées des fonctions ajoutées dans l'arbre, c'est-à-dire les fonctions que \emph{précisément} l'on n'a pas pu reconnaître et réécrire dans notre langage de fonctions, \emph{langage hors duquel on ne sait pas dériver}. Le mieux que l'on puisse faire, c'est d'instancier le théorème de correction de la dérivée avec l'arbre de valuation des fonctions et le terme dans le langage de fonctions, et de le «laisser en plan», c'est-à-dire de laisser à la charge de l'utilisateur le soin de fournir l'arbre de valuation des prédicats de dérivabilité, et l'arbre des dérivées. On voudrait quand même évincer autant que possible \texttt{interp} : j'utilise alors \texttt{simpl}, qui est pourtant un peu violent car il déplie d'autres définitions, rendant le but moins lisible : \begin{verbatim} Ltac derive v f := let f1 := eta_contraction f in let w := completer v f in let f0 := inversion_fonction w f1 in ( generalize (deriv_correcte f0 w) ; unfold Moins ; unfold Sur ; simpl interp ; unfold_fct ). \end{verbatim} \section*{Conclusion} Ce projet m'a permis d'approfondir mes connaissances en Coq, sous son aspect de prouveur de théorèmes : j'ai découvert de nombreuses astuces de preuve. Mais il m'a aussi permis de mieux étudier l'automatisation de manipulation de termes \emph{via} le langage de tactiques $\mathcal L_{tac}$.\footnote{Ce projet m'a aussi permis de réviser mes théorèmes sur les dérivées\dots} ~ Il est vrai que $\mathcal L_{tac}$ est assez difficile à maîtriser, car son comportement n'est pas bien spécifié, et la documentation est plutôt obscure. Certes, il admet des caractéristiques très intéressantes comme le \emph{backtracking} -- de plus, son pouvoir d'expression est très étonnant, par le fait qu'il soit (presque) non typé ; mais également des limitations dans le filtrage (impossibilité d'analyser sous les \texttt{fun}), ou des limitations plus conceptuelles comme l'impossibilité d'accéder aux bases de \texttt{Hint}. Enfin, l'automatisation de la réécriture n'est pas très satisfaisante en pratique : les tactiques sont trop ou pas assez puissantes selon le contexte, au point qu'il est difficile de cerner le comportement d'un \texttt{simpl} ou d'un \texttt{auto with real}. On aimerait bien, par exemple, effectuer un pas de $\beta$-réduction à un endroit précis du terme considéré, ou bien réécrire une égalité à un endroit précis en spécifiant le moins d'informations possibles (car sinon, cela reviendrait à utiliser \texttt{change}, par exemple)\dots \end{document}