rekursywnie odwracaj hipotezy w coq

Question

Mam problem z określeniem taktyki rekurencyjnie odwracającej hipotezy w kontekście próbnym. Na przykład, przypuśćmy, że ma dowodu kontekst zawierający hipotezę, takich jak:

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

i chciałby wielokrotnie odwrócić hipotezę uzyskać dowód kontekst zawierający hipotezy

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 

oczywiście uzyskanie takiego dowodu Kontekst jest łatwy dzięki wielokrotnemu stosowaniu taktyki inwersji. Czasami jednak odwrócenie hipotezy spowoduje wprowadzenie różnych hipotez do różnych podpoziomów i czy odwrócenie każdej z nich zależy od natury informacji dostarczanych przez inwersję.

Oczywistym problemem jest to, że bezkrytyczne porównywanie wzorców z kontekstem dowodzenia spowoduje nieterminację. Na przykład, następujące nie będzie działać, jeśli chce się zachować oryginalne hipotezy po ich odwróceniu:

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

Czy istnieje prosty sposób to zrobić? Oczywistym rozwiązaniem byłoby zachowanie stosu już odwróconych hipotez. Innym rozwiązaniem jest tylko odwrócenie hipotez na określoną głębokość, co usunie rekurencyjne wywołania w Ltac.

Answer 1

Jeśli to jest naprawdę to, co chcesz zrobić, podejrzewam chcesz najpierw udowodnić pomocnika Fixpoint subtreelist (st : searchtree): list (...) która zwraca listę wszystkich tych poddrzew, a następnie taktykę, która wywołuje subtreelist i rekurencyjnie destruct s listę transferowy masz wszystkie dodatkowe hipotezy, które chcesz.

Życzymy powodzenia!