4
在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
中的任何一个都可能是大复杂的证明术语(然后我可以用证明无关公理排除)。
@Zimm i48对'coq-tactic'的描述是:“策略是用Ltac编写的程序,'Coq'证明助手用于转换目标和术语的非类型化语言。”在我的理解中,这意味着有关如何使用Ltac写*策略的问题,或关于一般的证明自动化的问题。但我承认这个描述有点模棱两可。 –
好吧,可以免费回滚,让我们改进描述?甚至可能将标签名称更改为ltac?它会更清晰! –
@Zimm i48我查看了完整的描述,发现如下:“这个标签应该用于与使用coq证明助手使用coq策略导出证明的问题相关的问题。”在这种情况下,我认为你的编辑非常合适。我要(1)编辑标签信息以使其用法更清晰; (2)创建一个新标签'coq-ltac'; (3)将'coq-ltac'添加到一些帖子以显示其预期用途; (4)也许我们应该经历所有“共同策略”问题(现在有56个问题),并确保它们确实涉及战术相关问题。 –