Inverser de façon récursive des hypothèses dans coq

Question

J'ai du mal à définir une tactique pour inverser récursivement des hypothèses dans un contexte de preuve. Par exemple, supposons que j'ai un contexte preuve contenant une hypothèse comme:

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 

et voudrais inverser à plusieurs reprises l'hypothèse d'obtenir un contexte preuve contenant les hypothèses

H1 : search_tree (node a (node b ll lr) (node c rl rr)) 
H2 : search_tree (node b ll lr) 
H3 : search_tree (node c rl rr) 
H4 : lt_tree a (node b ll lr) 
H5 : gt_tree a (node c rl rr) 
H6 : lt_tree b ll 
H7 : gt_tree b lr 
H8 : lt_tree c rl 
H9 : gt_tree c rr 

Bien sûr, l'obtention de cette preuve le contexte est facile en appliquant à plusieurs reprises la tactique d'inversion. Cependant, inverser parfois une hypothèse mettra différentes hypothèses en différents sous-objectifs, et si inverser chacun dépend de la nature de l'information fournie par l'inversion.

Le problème évident est que l'appariement indistinctement des formes par rapport au contexte de preuve provoquera la non-terminaison. Par exemple, ce qui suit ne fonctionnera pas si l'on veut conserver les hypothèses d'origine après leur inversion:

Ltac invert_all := 
    match goal with 
    | [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all 
    | _ => idtac 
    end. 

est-il un moyen facile de le faire? La solution évidente serait de garder une pile d'hypothèses déjà inversées. Une autre solution consiste à inverser seulement les hypothèses jusqu'à une profondeur particulière, ce qui supprimerait les appels récursifs dans Ltac.

Answer 1

Si c'est vraiment ce que vous voulez faire, je suppose que vous voulez d'abord prouver une aide Fixpoint subtreelist (st : searchtree): list (...) qui retourne une liste de tous ces sous-arbres, et une tactique qui appelle subtreelist et récursive destruct de la liste jusqu'à ce que vous avez toutes les hypothèses supplémentaires que vous voulez.

Bonne chance avec ça!