主题:
Coq
数学归纳法

题目:
Coq的induct的归纳对应什么样的数学归纳法？
在Coq中，如果我们定义了
Inductive arith : Set :=
| Const (n : nat)
| Variable (x : string)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

那么，如果我们在证明forall a : arith, P(a)
的时候，如果我们使用intros. induct a.
我们会得到5个sbugoals.
其中，在证明Plus时，我们要证明的东西类似于
IHa1 : P(a1)
IHa2 : P(a2)
subgoal : P(Plus a1 a2)
问题来了，我们在证明Plus的时候，并没有证明过归纳法对于Minus和Times成立呀？如果a1和a2是Minus或者Times怎么办呢？
更进一步，如果因为Coq的这个“疏忽”，我们在证Plus时用到了Minus的性质，在证Minus时用到了Plus的性质，不就变成循环论证了吗？这该怎么办呢？

习题 还是 OT (在[]中填入x表示勾选):

• 习题
• OT

推荐理由:
Coq的induct中提到的rank概念在很多计算机领域中有所涉及，很多时候我们用一些比较模糊的rank函数对一类东西进行排序，可以得到很好的结果
题解:
Coq对于递归类型是非常严格的。Coq中可以定义的递归类型的每一个成员，都是可以通过有限个constructor构成的。
那么，这意味着什么呢？
意味着我们可以给每个成员赋一个值，不妨记作rank（秩）
所有不通过递归得到的成员，rank设为1.（如例子中的Const和Variable）
所有通过递归得到的表达式a，必然可以写作Constructor(subterm1 subterm2 ... subtermN)
我们定义rank(a) = max(rank(subterm1), rank(subterm2), ... rank(subtermN)) + 1
然后再回到这题。我们其实是在对表达式的秩（它的构造函数的最大深度）做递归！我们在证明Plus的时候，可以尽情使用Minus, Times的性质，因为我们真正在证明的，是如果所有秩为k的表达式如果都有P性质，那么所有秩为k+1的表达式也都有P性质！
这样一来，就不会出现交叉论证啦！

参考资料:

其它:
可延展内容（附简答）：
在考虑秩的定义时，如果涉及多个递归类型，能不能只考虑自己？
比如有两个递归类型Recur1, Recur2
Recur1有一个constructor是
Combine Recur1 Recur1 Recur2
如果我们定义a = Combine r1 r2 r3的秩为max(rank(r1), rank(r2)) + 1

• 这种定义和定义max(rank(r1), rank(r2), rank(r3) ) + 1有没有区别呢？（显然是有区别的）
• 这样定义秩会不会有问题呢？（在Coq语法内不会）
• 会不会影响我们在草稿纸上的证明过程呢？（不会）
• {简单介绍}这样定义秩其实和我们把rank(nat)认为是1一样是一种无伤大雅的简化。

有什么样的递归类型，会让我们无法使用秩来做归纳呢？（我还没想到，但应该是存在的）
如果存在这样的递归类型，有没有办法证明Coq语法中，永远无法定义这样的类型呢？