记录平等的 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 中的任何一个可能是大而复杂的证明条款(然后我可以用证明无关公理来解除)。

Answer 1

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