URL: https://linuxfr.org/forums/programmationautre/posts/question-sur-coq-et-la-tactique-induction Title: Question sur Coq et la tactique induction Authors: PyroTokyo Date: 2019年10月24日T08:10:34+02:00 License: CC By-SA Tags: coq Score: 2 Bonjour à tous Récemment, j'ai décidé de m'intéresser un peu à la théorie des types et de la démonstration. Quelques vieilles dépêches y sont pour un peu, et le sujet m'avait toujours un peu intrigué. Après quelques recherches, j'ai trouvé et commencé l'excellent [Logic Foundations](https://softwarefoundations.cis.upenn.edu/). J'en suis arrivé lentement mais sûrement au chapitre sur les propositions inductives (IndProp). Et là j'ai un petit soucis... ```coq Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o. Proof. intros m n o H1. generalize dependent o. ``` Là j'aimerais faire une induction sur H1. En regardant la définition de la relation : ```coq Inductive le : nat -> nat -> Prop := | le_n n : le n n | le_S n m (H : le n m) : le n (S m). Notation "m <= n" := (le m n). ``` Si j'ai bien compris, lorsque l'on fait une induction sur une hypothèse, on sépare les cas en fonction du "constructeur". Dans mon cas, je devrais avoir 2 possibilités, une pour le_n, et une pour le_S. Je devrais donc pouvoir faire quelque chose du genre ```coq induction H1 as [n' | n' m' H' IH]. ``` Seulement, il semblerait que n ne rentre pas dans le pattern. L'écriture correcte semble être ```coq induction H1 as [| m' H' IH]. ``` mais j'avoue ne pas savoir pourquoi. En allant plus loin dans le cours, dans la partie sur les regexp, je tombe sur une autre relation inductive : ```coq Inductive exp_match {T} : list T -> reg_exp -> Prop := | MEmpty : exp_match [] EmptyStr | MChar x : exp_match [x] (Char x) | MApp s1 re1 s2 re2 (H1 : exp_match s1 re1) (H2 : exp_match s2 re2) : exp_match (s1 ++ s2) (App re1 re2) | MUnionL s1 re1 re2 (H1 : exp_match s1 re1) : exp_match s1 (Union re1 re2) | MUnionR re1 s2 re2 (H2 : exp_match s2 re2) : exp_match s2 (Union re1 re2) | MStar0 re : exp_match [] (Star re) | MStarApp s1 s2 re (H1 : exp_match s1 re) (H2 : exp_match s2 (Star re)) : exp_match (s1 ++ s2) (Star re). ``` et lors de l'appel à induction, on a bien tous les arguments des constructeurs qui sont mappés. ```coq induction Hmatch as [| x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2]. ``` Du coup, je ne comprends pas pourquoi mon premier argument est sauté. Est-ce que j'aurais loupé quelque chose ??? Mis à part ça, j'aime bien le Coq ! C'est très chronophage, et on arrive facilement à passer des heures sur une démonstration... PS : dans la foulée, rien à voir, mais pourquoi ce calcul me renvoie un stack overflow ? La limite me semble très basse. J'ai essayé avec un accumulateur aussi, au cas où la TCO serait prise en charge, mais on dirait que non... ```coq Require Import Coq.Arith.Factorial. Compute fact 10. ```