在 Coq 中,我经常发现自己在做以下事情:我有证明目标,例如:
some_constructor a c d = some_constructor b c d
而且我真的只需要证明a = b
,因为无论如何其他一切都是相同的,所以我这样做:
assert (a = b).
然后证明那个子目标,然后
rewrite H.
reflexivity.
完成证明。
但是,让那些在我的证明底部徘徊似乎只是不必要的混乱。
Coq 中是否有一个通用策略来获取构造函数的相等性并将其拆分为构造函数参数的相等性,有点像 asplit
但用于等式而不是连词。