coq - 记录平等的 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是任何函数符号，其中构造函数是一种特殊情况。