标准库中inl和inr的内射性
标准库中inl和inr的内射性
提问于 2015-09-10 14:00:33
在Coq标准库中，我可以找到一个引理，说明inl和inr是注入吗？也就是，forall (A B : Type)(x y : A), inl B x = inl B y -> x = y，类似于右边的情况.我自己证明这一点没有问题，但这些似乎是非常有用和重要的引理，我不得不想象它们已经在标准库的某个地方了。
回答 1
Stack Overflow用户
回答已采纳
发布于 2015-09-10 17:06:29
由于归纳类型的所有构造函数都是内射的，因此定义所有这些引理是很麻烦的。可以说，它们可以按照归纳原则的定义方式自动定义，但是，它们可以从它们派生出来。
不管怎么说，如果你对引理的需要是用不同的证明来表示，你应该知道战术注入，它为你检索所有必要的等式。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/32503986
复制相关文章
相似问题
腾讯云开发者
