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中的递归调用。