recursion - 在 coq 中递归反转假设

Question

我无法定义一种策略来在证明上下文中递归地反转假设。例如，假设我有一个包含如下假设的证明上下文:

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

Answer 1

如果这确实是您想要做的，我怀疑您首先要证明一个助手 Fixpoint subtreelist (st : searchtree): list (...) 返回所有这些子树的列表，然后是调用 subtreelist 并递归地destruct列表的策略，直到获得所需的所有额外假设。

祝你好运!