分解构造函数coq的相等性

Question

通常在Coq我发现自己做了以下事情:我有证据目标,例如:

some_constructor a c d = some_constructor b c d

我真的只需要证明,a = b因为其他一切都是相同的,所以我这样做:

assert (a = b).

然后证明那个subgoal

rewrite H.
reflexivity.

完成证明.

但是,在我的证据的底部悬挂那些似乎是不必要的混乱.

在Coq中是否有一个通用的策略来获取构造函数的相等性并将其分解为构造函数参数的相等性,有点像是一个split但是对于平等而不是连接.

Answer 1

特别是，标准 Coq 提供了这种f_equal策略。

Inductive u : Type := U : nat -> nat -> nat -> u.

Lemma U1 x y z1 z2 : U x y z1 = U x y z2.
f_equal

此外，ssreflect 还提供了一种通用的同余策略congr。