INDPROP.归纳定义命题.案例研究：改进反思
Case Study: Improving Reflection
我们在逻辑一章中看到，我们经常需要将布尔计算与Prop中的语句相关联。但是，在那里执行这种转换可能会导致冗长的验证脚本。考虑下面定理的证明：
【学习】函数语言程序设计 文章被收录于专栏
函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】
