记录平等的Coq策略？

在Coq中，当试图证明记录的平等时，是否有策略将其分解为所有字段的平等？例如，记录平等的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中的任何一个都可能是大复杂的证明术语（然后我可以用证明无关公理排除）。

来源

2014-07-06 Ashley Yakeley

@Zimm i48对'coq-tactic'的描述是：“策略是用Ltac编写的程序，'Coq'证明助手用于转换目标和术语的非类型化语言。”在我的理解中，这意味着有关如何使用Ltac写*策略的问题，或关于一般的证明自动化的问题。但我承认这个描述有点模棱两可。 –

好吧，可以免费回滚，让我们改进描述？甚至可能将标签名称更改为ltac？它会更清晰！ –

@Zimm i48我查看了完整的描述，发现如下：“这个标签应该用于与使用coq证明助手使用coq策略导出证明的问题相关的问题。”在这种情况下，我认为你的编辑非常合适。我要（1）编辑标签信息以使其用法更清晰; （2）创建一个新标签'coq-ltac'; （3）将'coq-ltac'添加到一些帖子以显示其预期用途; （4）也许我们应该经历所有“共同策略”问题（现在有56个问题），并确保它们确实涉及战术相关问题。 –

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

来源

2014-07-06 09:59:45

记录平等的Coq策略？

回答

相关问题