递归地反转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列表的策略,直到你拥有你想要的所有额外假设.

祝你好运!