invertir recursivamente las hipótesis en coq

Question

Tengo problemas para definir una táctica para invertir recursivamente las hipótesis en un contexto de prueba. Por ejemplo, supongamos que tengo un contexto prueba que contiene una hipótesis como:

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

y me gustaría invertir en repetidas ocasiones la hipótesis de obtener un contexto prueba que contiene las hipótesis

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 

Por supuesto, la obtención de esta prueba el contexto es fácil al aplicar repetidamente la táctica de inversión. Sin embargo, a veces la inversión de una hipótesis colocará diferentes hipótesis en diferentes subgoles, y si invertir cada uno depende de la naturaleza de la información proporcionada por la inversión.

El problema obvio es que la coincidencia de patrones indiscriminadamente con el contexto de prueba causará la no determinación. Por ejemplo, lo siguiente no funcionará si se desea conservar las hipótesis originales después de invertir ellos:

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

¿Hay una manera fácil de hacer esto? La solución obvia sería mantener una pila de hipótesis ya invertidas. Otra solución es invertir hipótesis hasta una profundidad particular, lo que eliminaría las llamadas recursivas en Ltac.

Answer 1

Si eso es realmente lo que quiere hacer, sospecho que desea primero en demostrar un ayudante Fixpoint subtreelist (st : searchtree): list (...) que devuelve una lista de todos estos sub-estructuras, y luego una táctica que llama subtreelist y de forma recursiva destruct s la lista hasta que usted tiene toda la hipótesis extra que quieras.

¡Buena suerte con eso!