如何解决添加 ltac 表达式作为自动重写的提示?
我正在尝试使用 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.
这样我们在第一个模式中捕获 []
并跳过重写,否则执行重写。也许这需要一个falltrough案例,但这不是重点:我如何向autorewrite
提供(类似)这个提示?我试图将上述定义为一个单独的策略(也许我可以将 normalize 定义为 (norm_cons; autorewrite with blablabla).
),但它随后抱怨 match
中没有任何分支与我的目标匹配。这是否进行递归搜索?或者我必须自己添加这个(即匹配 ?XS ++ ?YS
并递归重写 lhs 和 rhs?)
解决方法
似乎您只想重写包含至少两个元素的列表。也许你可以用
重写forall x y xs,x :: y :: xs = [x] ++ y::xs
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。