Coq策略用于记录相等性？

Question

在Coq中，当试图证明记录的相等性时，是否有一种策略可以将其分解为所有字段的相等性？例如，

Record R := {x:nat;y:nat}.

Variables a b c d : nat.

Lemma eqr : {|x:=a;y:=b|} = {|x:=c;y:=d|}.

有没有一种策略可以将这个式子简化成a = c /\ b = d？需要注意的是，一般来说，a b c d中的任何一个都可能是复杂的证明项（我可以使用一个证明不相关公理来解决它们）。

- Ashley Yakeley

---

@Zimm i48 coq-tactic 的描述是：“策略是使用 Ltac 编写的程序，Ltac 是在 Coq 证明助手中使用的无类型语言，用于转换目标和术语。” 在我看来，这意味着关于如何使用 Ltac 编写策略或者关于证明自动化的一般问题。但我承认这个描述有点模糊不清。 - Anton Trunov

好的，随意回滚，让我们也许改进一下描述？甚至将标签名称更改为ltac？这样会更清晰明了！ - Zimm i48

@Zimm i48 我已经查看了完整的描述，并发现以下内容：“此标签应用于与使用Coq证明助手推导证明的coq策略相关的问题。” 在这种情况下，我认为您的编辑非常合适。我将（1）编辑标签信息以使其使用更清晰；（2）创建一个新的标签“coq-ltac”；（3）将“coq-ltac”添加到一些帖子中以显示其预期的使用方式；（4）也许我们应该浏览所有“coq-tactic”问题（现在有56个），确保它们确实是关于策略相关问题的。 - Anton Trunov

我认为你不必将其命名为 coq-ltac，只使用 ltac 似乎已经足够了。如果你在 SO 上搜索 ltac，你会发现只有 Coq 相关的问题。 - Zimm i48

@Zimm i48 好的！ - Anton Trunov

Answer 1

你可以使用f_equal策略，它不仅适用于记录，还适用于形式为f x1 .. xn = f y1 .. yn的任意目标，其中f是任何函数符号，构造函数是其特殊情况。

- Arthur Azevedo De Amorim

---

我曾错误地理解这是为每个 f 定义的一系列策略，例如定义 foo x y 将隐式定义 foo_equal，bar x y z 将定义 bar_equal 等等。注意对于其他被误导的人：事实并非如此，只有一个 f_equal 策略，f 不是策略名称中的元语法。 - Suzanne Soy