Bonjour,
J’espère que vous allez bien ?
J’essayais pour un projet de faire une fonction récursive imbriquée non structurelle et selon mes recherches les options qui me sont possibles sont Program Fixpoint, Equations et Function.
Avec Program Fixpoint j’arrive bien à donner les preuves de terminaison mais lorsque je veux les utiliser dans des preuves je n’arrive pas à faire les inductions correctement. J’aimerais savoir si pour les Program Fixpoint il existe un équivalent de la tactique “functional induction”.
Avec Equations, la preuve de terminaison a un soucis car toutes les hypothèses ne sont pas générées comme dans Program Fixpoint.
Avec Function, je n’arrive pas à faire de la récursion imbriquée car cela n’est pas géré par la définition de Function.
En vous remerciant d’avance,
Je serais aussi curieux de connaître la réponse. Je ne la connais pas moi-même malheureusement.
Dans l’idéal, Equations devrait remplacer les autres solutions, donc on pourrait aussi essayer de te débloquer par là sur un exemple concret.