[征集题目]Coq的induct对应什么数学证明方法

[Michael1015198808]

主题: 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表示勾选):

• [ ] 习题
• [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语法中，永远无法定义这样的类型呢？

[hengxin]

目前来看, 多数学生没有足够的精力学习 Coq。我需要再考虑以什么方式在课程中引入 Coq。