我在定义在证明上下文中递归反转假设的策略时遇到了麻烦。例如，假设我有一个包含如下假设的证明上下文：
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 中的递归调用。