问Coq：(a :：L1) = (b :：L2)⇒a=b∧L1 = L2？
EN

Stack Overflow用户

提问于 2018-11-10 19:20:32

回答 1查看 52关注 0票数 1

这句话在我看来是显而易见的，除非我忽略了一些反例，但我在Coq库中找不到任何这样做的东西。有这样的命令吗？

回答已采纳

发布于 2018-11-10 19:36:39

这通常可以通过使用injection策略来获得。重写引理的一个版本可以在数学-comp中找到：

eqseq_cons (T : eqType) (x1 x2 : T) (s1 s2 : seq T) :
   (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2).

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/53242574

复制

相似问题

问Coq：(a :：L1) = (b :：L2)⇒a=b∧L1 = L2？EN