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:rekursywnie odwracaj hipotezy w coq
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.