- Basics
- Polymorphism
- Induction Hypotheses
- More on the induction Tactic
- Induction Principles for Propositions
- Another Form of Induction Principles on Propositions (Optional)
- Formal vs. Informal Proofs by Induction
- Induction Over an Inductively Defined Set
- Induction Over an Inductively Defined Proposition
- Explicit Proof Objects for Induction (Optional)
本章：对数学归纳法进行了拓展
Basic
每当我们使用 Inductive 来声明数据类型时， Coq 就会自动为该类型生成 ' 归纳法则 (inductionPriciples)' 。这个归纳法则也是定理
如果 t 是归纳定义的，那么对应的归纳法则被称作 t_ind
举例：自然数的归纳定义
Suppose P is a property of natural numbers (that is, P n is a Prop for every n ).
To show that P n holds of all n, it suffices to show:
P holds of 0
for any n, if P holds of n, then P holds of S n.
即：
nat_ind 应用
几乎等价于
二者的区别：
在 apply nat_ind 之前我们没有在上下文中引入 n —— nat_ind 的结论 是一个带有量词的公式，apply 需要这个结论精确地匹配当前证明目标状态的形状，包括其中的量词。
相反**，induction** 策略对于上下文中的变量或目标中由量词引入的变量都适用 。
我们必须手动为 apply 提供归纳法则，而 induction 可以自己解决它。
相比于直接使用 nat_ind 这样的归纳法则，在实践中使用 induction 更加方便。
Coq 为每一个 Inductive 定义的数据类型生成了归纳法则，包括那些非递归的。 尽管我们不需要归纳，便可证明非递归数据类型的性质，但归纳原理仍可用来证明其性质； 给定类型，及关于该类型所有值的性质，归纳原理提供了证明该性质的方法。
如果我们定义了带有构造子 c1 … cn 的类型 t，那么 Coq 会生成形如下文的定理：
举例：
例子二
例子三 booltree
多态
T he main difference is that, here, the whole definition is parameterized ( 参数化 ) on a set X: that is, we are defining a family of inductive types list X, one for each X
注意归纳法则的*'所有部分'* 都被 X 所参数化。也即，list_ind 可认为是一个 多态函数，当被应用类型 X 时，返回特化在类型 list X 上的归纳法则。
归纳假设 Induction Hypotheses
它对所有的命题 P 都成立，
Each time we use this principle, we are choosing P to be a particular expression of type nat → Prop
每次使用这个原理，我们将 P 特化为一个类型为 nat → Prop 的表达式
instead of stating the theorem mul_0_r as " ∀ n, n × 0 = 0 ," we can write it as " ∀ n, P_m0r n"
P_m0r n 的定义
或者
后略