記錄平等的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策略？

回答

相關問題