根据这个课程,所有构造函数(对于归纳类型)都是单射的和不相交的:
...类似的原则适用于所有归纳定义的类型:所有构造函数都是单射的,并且由不同构造函数构建的值永远不会相等.对于列表,cons构造函数是单射的,nil与每个非空列表不同.对于布尔,真假都是不平等的.
(以及inversion基于这种假设的策略)
我只是想知道我们怎么知道这个假设成立了？
我们怎么知道,例如,我们不能基于定义自然数
1)一个继承者,也许是像这样的"双"构造函数:
Inductive num: Type :=
| O : num
| S : num -> num
| D : num -> num.
和
2)一些plus功能,以便2通过两个不同的序列/路由构造函数可以达到一个数字,S (S O)并且D (S O)？
Coq的机制是什么,以确保上述内容永远不会发生？
PS我不是建议上面的num例子是可能的.我只是想知道是什么让它变得不可能.
谢谢