inverti ricorsivamente le ipotesi in coq

Question

Ho difficoltà a definire una tattica per invertire ricorsivamente le ipotesi in un contesto di prova. Per esempio, supponiamo di avere un contesto prova contenente un'ipotesi simile:

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

e vorrei invertire ripetutamente l'ipotesi di ottenere un contesto prova contenente le ipotesi

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 

Naturalmente, ottenendo questa dimostrazione il contesto è facile applicando ripetutamente la tattica di inversione. Tuttavia, a volte invertendo un'ipotesi si mettono diverse ipotesi in diversi sotto-obiettivi, e se invertire ognuno dipende dalla natura delle informazioni fornite dall'inversione.

Il problema ovvio è che la corrispondenza del modello indiscriminato con il contesto di prova causerà il non completamento. Per esempio, il seguente non funziona se si vuole mantenere le ipotesi originali dopo averli invertendo:

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

C'è un modo semplice per fare questo? La soluzione ovvia sarebbe mantenere una pila di ipotesi già invertite. Un'altra soluzione è di invertire le ipotesi solo fino a una particolare profondità, che rimuoverebbe le chiamate ricorsive in Ltac.

Answer 1

Se questo è davvero quello che vuoi fare, ho il sospetto che si desidera primo a dimostrare un aiutante Fixpoint subtreelist (st : searchtree): list (...) che restituisce un elenco di tutte queste sottostrutture, e poi una tattica che chiama subtreelist e ricorsivamente destruct s la lista fino a che non hai tutte le ipotesi extra che vuoi

Buona fortuna!