通常在Coq我发现自己做了以下事情:我有证据目标,例如:
some_constructor a c d = some_constructor b c d
我真的只需要证明,a = b因为其他一切都是相同的,所以我这样做:
assert (a = b).
然后证明那个subgoal
rewrite H.
reflexivity.
完成证明.
但是,在我的证据的底部悬挂那些似乎是不必要的混乱.
在Coq中是否有一个通用的策略来获取构造函数的相等性并将其分解为构造函数参数的相等性,有点像是一个split但是对于平等而不是连接.
我要将目标从更改S x = S y为x = y。就像inversion，只是为了目标而不是假设。
这样的策略似乎是合法的，因为当我们拥有时x = y，我们可以简单地使用rewrite并reflexivity证明目标。
目前，我总是发现自己经常使用assert (x = y)新的子目标，但是编写何时x且y复杂的表达式是很繁琐的。