Commit bbb28471 authored by Samuel Ben Hamou's avatar Samuel Ben Hamou
Browse files

Suite rapport (généralité rec)

parent e599f73b
......@@ -263,9 +263,7 @@ La seconde tactique élaborée n'est pas à utiliser systématiquement. Elle per
Concrètement, cette tactique s'appuie sur une tactique auxiliaire \verb+parse+ qui prend en argument une formule $\phi$ contenant au moins une quantification universelle sous la forme non-restrictive \[ \phi_1 \Rightarrow \cdots \Rightarrow \forall x \cdot \phi_n \] avec éventuellement $n = 1$, et qui retourne $\phi_n$. Une fois la formule $\phi_n$ identifiée, \verb+rec+ l'utilise pour instancier le schéma d'axiome de récurrence et initie la preuve, de sorte que l'utilise se retrouve avec deux buts, qui correspondent à l'initialisation et à l'hérédité de la preuve par récurrence. Pour ce faire, j'ai eu besoin de prouver deux lemmes auxiliaires qui permettent essentiellement de montrer que l'instance du schéma d'axiome de récurrence choisie est bien licite, et qui proposent une forme plus facilement manipulable du principe de récurrence.
Il est à noter que, en allant chercher le premier quantificateur universel qu'elle trouve dans la formule, \verb+parse+ ne restreint pas la généralité de la tactique \verb+rec+. En effet, les quantificateurs universels commutent évidemment, et si un le théorème $\phi$ à démontrer contient un quantificateur existentiel, on peut toujours éliminer les quantificateurs qui le précèdent (avec les règles \verb+R_All_i+ et \verb+R_Ex_i+) afin d'appliquer la tactique \verb+rec+, puis les réintroduire avec \verb+R_All_e+ et \verb+R_Ex_e+. Cela revient essentiellement à utiliser les tactiques \verb+intro+ et \verb+exists+ avant de lancer un \verb+induction+ en Coq, puis d'utiliser \verb+revert+ pour rétablir le théorème initial.
% TODO
% nom de l'analogue de revert pour exists
Il est à noter que, en allant chercher le premier quantificateur universel qu'elle trouve dans la formule, \verb+parse+ ne restreint pas la généralité de la tactique \verb+rec+. En effet, les quantificateurs universels commutent évidemment, et si l'on veut faire une récurrence sur la variable qui n'est la première variable quantifiée, on peut toujours éliminer les quantificateurs qui la précèdent (avec la règle \verb+R_All_i+) afin d'appliquer la tactique \verb+rec+, puis les réintroduire avec \verb+R_All_e+. Cela revient essentiellement à utiliser la tactique \verb+intro+ avant de lancer un \verb+induction+ en Coq, puis d'utiliser \verb+revert+ pour rétablir le théorème initial.
\subsubsection{Pour raccourcir certains raisonnements}
......
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