coq - 添加 ltac 表达式作为自动重写的提示？

Question

我正在尝试使用autorewrite. 为简单起见，我们可以假设它是一个列表（但实际上该类型更复杂，具有多个 cons 构造函数，并且重写规则使用等价而不是相等）。

我想要得到的正常形式是变量或单例列表的串联，x1 :: x2 :: xs ++ y :: ys即[x1] ++ [x2] ++ xs ++ [y] ++ ys. 到目前为止，我通过为autorewrite. 但是，提示forall x xs, xs :: x = xs ++ [x]不起作用，因为[x] = x : []它可以被重写，[x] ++ []从而产生一个无限循环。

我在编写自定义 Ltac 表达式方面没有太多经验，但似乎我可以定义如下内容：

Ltac norm_cons :=
  match goal with
  | H: ?X : [] => idtac
  | H: ?X : ?XS => (* actual rewrite *)
  end.

这样我们[]在第一个模式中捕获并跳过重写，否则执行重写。也许这需要一个失败的案例，但这不是重点：我如何给出（类似的）这个作为提示autorewrite？我试图将上述定义为一个单独的策略（也许我可以将 normalize 定义为(norm_cons; autorewrite with blablabla).），但它随后抱怨没有与match我的目标匹配的分支。这会进行递归搜索吗？还是我必须自己添加这个（即匹配?XS ++ ?YS并递归地重写 lhs 和 rhs？）

标签： coq

Answer 1

似乎您只想用至少两个元素重写列表。也许你可以重写

forall x y xs, x :: y :: xs = [x] ++ y::xs