9
我在定義證明上下文中遞歸顛倒假設的策略時遇到了困難。舉例來說，假設我有包含類似的假設證明背景：遞歸地逆轉coq中的假設
H1 : search_tree (node a (node b ll lr) (node c rl rr))
，並想反覆反轉的假設，得到含假設
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
當然的證據情況下，獲得這方面的證據通過反覆應用反演策略，上下文很容易。然而，有時將假設倒置會將不同的假設置於不同的子目標中，並且是否倒置取決於倒置提供的信息的性質。
一個明顯的問題是，對證明上下文不加區分地進行模式匹配將導致非終止。例如，下面的不會，如果人們想保留原來的工作假設它們翻轉後：
Ltac invert_all :=
match goal with
| [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all
| _ => idtac
end.
是否有一個簡單的方法來做到這一點？顯而易見的解決方案是保留一堆已經被顛倒的假設。另一種解決方案是隻能將假設逆轉到特定的深度，這將消除Ltac中的遞歸調用。