lf-current/toc.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>目录</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<script>

$(document).ready(function() {

    $("#accordion").show().accordion({
        autoHeight: false
    });

    $("#accordion div").css({ 'height': 'auto' });
});      


$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };
    
    $( "#accordion" ).accordion({
      icons: icons
    });
    $("#accordion").accordion({collapsible : true, active : 'none'});

    $( "#toggle" ).button().on( "click", function() {
      if ( $( "#accordion" ).accordion( "option", "icons" ) ) {
        $( "#accordion" ).accordion( "option", "icons", null );
      } else {
        $( "#accordion" ).accordion( "option", "icons", icons );
      }
    });
  } );
  </script>
<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</div>
</a></div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">前言&nbsp;&nbsp;&nbsp;&nbsp;(<b>Preface</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html">页首</a>
<li><a href="Preface.html#lab1">欢迎</a>

</li>
<li><a href="Preface.html#lab2">概览</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">逻辑学</a>

</li>
<li><a href="Preface.html#lab4">证明助理</a>

</li>
<li><a href="Preface.html#lab5">函数式编程</a>

</li>
<li><a href="Preface.html#lab6">扩展阅读</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab7">实践指南</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab8">章节依赖</a>

</li>
<li><a href="Preface.html#lab9">系统要求</a>

</li>
<li><a href="Preface.html#lab10">练习</a>

</li>
<li><a href="Preface.html#lab11">下载 Coq 文件</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab12">资源</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab13">模拟题</a>

</li>
<li><a href="Preface.html#lab14">课程视频</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab15">对授课员的要求</a>

</li>
<li><a href="Preface.html#lab16">译本</a>

</li>
<li><a href="Preface.html#lab17">鸣谢</a>

</li>
</ul>
</div>
<h2><a href="Basics.html">Coq 函数式编程&nbsp;&nbsp;&nbsp;&nbsp;(<b>Basics</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Basics.html">页首</a>
<li><a href="Basics.html#lab18">引言</a>

</li>
<li><a href="Basics.html#lab19">数据与函数</a>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab20">枚举类型</a>

</li>
<li><a href="Basics.html#lab21">一周七日</a>

</li>
<li><a href="Basics.html#lab22">作业提交指南</a>

</li>
<li><a href="Basics.html#lab23">布尔值</a>

</li>
<li><a href="Basics.html#lab26">类型</a>

</li>
<li><a href="Basics.html#lab27">由旧类型构造新类型</a>

</li>
<li><a href="Basics.html#lab28">Tuples</a>

</li>
<li><a href="Basics.html#lab29">模块</a>

</li>
<li><a href="Basics.html#lab30">数值</a>

</li>
</ul>
</div>

</li>
<li><a href="Basics.html#lab33">基于化简的证明</a>

</li>
<li><a href="Basics.html#lab34">基于改写的证明</a>

</li>
<li><a href="Basics.html#lab37">利用情况分析来证明</a>

</li>
<li><a href="Basics.html#lab40">关于记法的更多内容 (可选)</a>

</li>
<li><a href="Basics.html#lab41">不动点 <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span> 和结构化递归 (可选)</a>

</li>
<li><a href="Basics.html#lab43">更多练习</a>

</li>
</ul>
</div>
<h2><a href="Induction.html">归纳证明&nbsp;&nbsp;&nbsp;&nbsp;(<b>Induction</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Induction.html">页首</a>
<li><a href="Induction.html#lab48">归纳法证明</a>

</li>
<li><a href="Induction.html#lab53">证明里的证明</a>

</li>
<li><a href="Induction.html#lab54">形式化证明 vs. 非形式化证明</a>

</li>
<li><a href="Induction.html#lab57">更多练习</a>

</li>
</ul>
</div>
<h2><a href="Lists.html">使用结构化的数据&nbsp;&nbsp;&nbsp;&nbsp;(<b>Lists</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Lists.html">页首</a>
<li><a href="Lists.html#lab64">数值序对</a>

</li>
<li><a href="Lists.html#lab67">数值列表</a>
<div>
<ul class="doclist">
<li><a href="Lists.html#lab75">用列表实现口袋（Bag）</a>

</li>
</ul>
</div>

</li>
<li><a href="Lists.html#lab79">有关列表的论证</a>
<div>
<ul class="doclist">
<li><a href="Lists.html#lab80">一点点说教</a>

</li>
<li><a href="Lists.html#lab81">对列表进行归纳</a>

</li>
<li><a href="Lists.html#lab84"><span class="inlinecode"><span class="id" type="var">Search</span></span> 搜索</a>

</li>
<li><a href="Lists.html#lab85">列表练习，第一部分</a>

</li>
<li><a href="Lists.html#lab88">列表练习, 第二部分</a>

</li>
</ul>
</div>

</li>
<li><a href="Lists.html#lab93">Options 可选类型</a>

</li>
<li><a href="Lists.html#lab96">偏映射（Partial Maps）</a>

</li>
</ul>
</div>
<h2><a href="Poly.html">多态与高阶函数&nbsp;&nbsp;&nbsp;&nbsp;(<b>Poly</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Poly.html">页首</a>
<li><a href="Poly.html#lab101">多态</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab102">多态列表</a>

</li>
<li><a href="Poly.html#lab111">多态序对</a>

</li>
<li><a href="Poly.html#lab114">多态候选</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab116">函数作为数据</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab117">高阶函数</a>

</li>
<li><a href="Poly.html#lab118">过滤器</a>

</li>
<li><a href="Poly.html#lab119">匿名函数</a>

</li>
<li><a href="Poly.html#lab122">映射</a>

</li>
<li><a href="Poly.html#lab127">折叠</a>

</li>
<li><a href="Poly.html#lab129">用函数构造函数</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab130">附加练习</a>

</li>
</ul>
</div>
<h2><a href="Tactics.html">更多基本策略&nbsp;&nbsp;&nbsp;&nbsp;(<b>Tactics</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Tactics.html">页首</a>
<li><a href="Tactics.html#lab139"><span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略</a>

</li>
<li><a href="Tactics.html#lab143"><span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> 策略</a>

</li>
<li><a href="Tactics.html#lab145">The <span class="inlinecode"><span class="id" type="tactic">injection</span></span> and <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> Tactics</a>

</li>
<li><a href="Tactics.html#lab148">对前提使用策略</a>

</li>
<li><a href="Tactics.html#lab150">变换归纳法则</a>

</li>
<li><a href="Tactics.html#lab154">展开定义</a>

</li>
<li><a href="Tactics.html#lab155">对复合表达式使用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span></a>

</li>
<li><a href="Tactics.html#lab158">复习</a>

</li>
<li><a href="Tactics.html#lab159">附加练习</a>

</li>
</ul>
</div>
<h2><a href="Logic.html">Coq 中的逻辑系统&nbsp;&nbsp;&nbsp;&nbsp;(<b>Logic</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Logic.html">页首</a>
<li><a href="Logic.html#lab166">逻辑联结词</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab167">合取</a>

</li>
<li><a href="Logic.html#lab171">析取</a>

</li>
<li><a href="Logic.html#lab174">假命题与否定</a>

</li>
<li><a href="Logic.html#lab180">真值</a>

</li>
<li><a href="Logic.html#lab181">逻辑等价</a>

</li>
<li><a href="Logic.html#lab184">存在量化</a>

</li>
</ul>
</div>

</li>
<li><a href="Logic.html#lab187">使用命题编程</a>

</li>
<li><a href="Logic.html#lab192">对参数应用定理</a>

</li>
<li><a href="Logic.html#lab193">Coq vs. 集合论</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab194">函数的外延性</a>

</li>
<li><a href="Logic.html#lab196">命题与布尔值</a>

</li>
<li><a href="Logic.html#lab202">经典逻辑 vs. 构造逻辑</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="IndProp.html">归纳定义的命题&nbsp;&nbsp;&nbsp;&nbsp;(<b>IndProp</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndProp.html">页首</a>
<li><a href="IndProp.html#lab206">归纳定义的命题</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab207">偶数性的归纳定义</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab209">在证明中使用证据</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab210">对证据进行反演</a>

</li>
<li><a href="IndProp.html#lab213">对证据进行归纳</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab218">归纳关系</a>

</li>
<li><a href="IndProp.html#lab227">案例学习：正则表达式</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab231"><span class="inlinecode"><span class="id" type="var">remember</span></span> 策略</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab234">案例学习：改进互映</a>

</li>
<li><a href="IndProp.html#lab237">额外练习</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab245">扩展练习：经验证的正则表达式匹配器</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Maps.html">全映射与偏映射&nbsp;&nbsp;&nbsp;&nbsp;(<b>Maps</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Maps.html">页首</a>
<li><a href="Maps.html#lab254">Coq 标准库</a>

</li>
<li><a href="Maps.html#lab255">标识符</a>

</li>
<li><a href="Maps.html#lab256">全映射</a>

</li>
<li><a href="Maps.html#lab264">偏映射</a>

</li>
</ul>
</div>
<h2><a href="ProofObjects.html">柯里-霍华德对应&nbsp;&nbsp;&nbsp;&nbsp;(<b>ProofObjects</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html">页首</a>
<li><a href="ProofObjects.html#lab265">证明脚本</a>

</li>
<li><a href="ProofObjects.html#lab267">量词，蕴含式，函数</a>

</li>
<li><a href="ProofObjects.html#lab268">使用策略编程</a>

</li>
<li><a href="ProofObjects.html#lab269">逻辑联结词作为归纳类型</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab270">合取</a>

</li>
<li><a href="ProofObjects.html#lab272">析取</a>

</li>
<li><a href="ProofObjects.html#lab274">存在量化</a>

</li>
<li><a href="ProofObjects.html#lab276"><span class="inlinecode"><span class="id" type="var">True</span></span>和<span class="inlinecode"><span class="id" type="var">False</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="ProofObjects.html#lab277">相等关系</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab280">再论反演</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="IndPrinciples.html">归纳法则&nbsp;&nbsp;&nbsp;&nbsp;(<b>IndPrinciples</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html">页首</a>
<li><a href="IndPrinciples.html#lab281">基础</a>

</li>
<li><a href="IndPrinciples.html#lab287">多态</a>

</li>
<li><a href="IndPrinciples.html#lab292">归纳假设</a>

</li>
<li><a href="IndPrinciples.html#lab293">深入 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略</a>

</li>
<li><a href="IndPrinciples.html#lab295"><span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 中的归纳法则</a>

</li>
<li><a href="IndPrinciples.html#lab296">形式化 vs. 非形式化的归纳证明</a>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html#lab297">对归纳定义的集合进行归纳</a>

</li>
<li><a href="IndPrinciples.html#lab298">对归纳定义的命题进行归纳</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Rel.html">关系的性质&nbsp;&nbsp;&nbsp;&nbsp;(<b>Rel</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Rel.html">页首</a>
<li><a href="Rel.html#lab299">关系</a>

</li>
<li><a href="Rel.html#lab300">基本性质</a>

</li>
<li><a href="Rel.html#lab317">自反传递闭包</a>

</li>
</ul>
</div>
<h2><a href="Imp.html">简单的指令式程序&nbsp;&nbsp;&nbsp;&nbsp;(<b>Imp</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Imp.html">页首</a>
<li><a href="Imp.html#lab320">算术和布尔表达式</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab321">语法</a>

</li>
<li><a href="Imp.html#lab322">求值</a>

</li>
<li><a href="Imp.html#lab323">优化</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab324">Coq 自动化</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab325">泛策略</a>

</li>
<li><a href="Imp.html#lab332">定义新的策略记法</a>

</li>
<li><a href="Imp.html#lab333"><span class="inlinecode"><span class="id" type="tactic">omega</span></span> 策略</a>

</li>
<li><a href="Imp.html#lab334">更多方便的策略</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab335">求值作为关系</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab336">推理规则的记法</a>

</li>
<li><a href="Imp.html#lab338">定义的等价关系</a>

</li>
<li><a href="Imp.html#lab340">计算式定义与关系式定义</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab341">带变量的表达式</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab342">状态</a>

</li>
<li><a href="Imp.html#lab343">语法</a>

</li>
<li><a href="Imp.html#lab344">记法</a>

</li>
<li><a href="Imp.html#lab345">求值</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab346">指令</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab347">语法</a>

</li>
<li><a href="Imp.html#lab348">脱糖记法</a>

</li>
<li><a href="Imp.html#lab349"><span class="inlinecode"><span class="id" type="var">Locate</span></span> 命令</a>

</li>
<li><a href="Imp.html#lab352">更多示例</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab355">求值指令</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab356">求值作为函数（失败的尝试）</a>

</li>
<li><a href="Imp.html#lab357">求值作为一种关系</a>

</li>
<li><a href="Imp.html#lab361">求值的确定性</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab362">对 Imp 进行推理</a>

</li>
<li><a href="Imp.html#lab367">附加练习</a>

</li>
</ul>
</div>
<h2><a href="ImpParser.html">用 Coq 实现词法分析和语法分析&nbsp;&nbsp;&nbsp;&nbsp;(<b>ImpParser</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpParser.html">页首</a>
<li><a href="ImpParser.html#lab375">内部结构</a>
<div>
<ul class="doclist">
<li><a href="ImpParser.html#lab376">词法分析</a>

</li>
<li><a href="ImpParser.html#lab377">语法分析</a>

</li>
</ul>
</div>

</li>
<li><a href="ImpParser.html#lab381">示例</a>

</li>
</ul>
</div>
<h2><a href="ImpCEvalFun.html">Imp 的求值函数&nbsp;&nbsp;&nbsp;&nbsp;(<b>ImpCEvalFun</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpCEvalFun.html">页首</a>
<li><a href="ImpCEvalFun.html#lab382">一个无法完成的求值器</a>

</li>
<li><a href="ImpCEvalFun.html#lab383">一个计步的求值器</a>

</li>
<li><a href="ImpCEvalFun.html#lab386">关系求值 vs. 计步求值</a>

</li>
<li><a href="ImpCEvalFun.html#lab389">再论求值的确定性</a>

</li>
</ul>
</div>
<h2><a href="Extraction.html">从 Coq 中提取 ML&nbsp;&nbsp;&nbsp;&nbsp;(<b>Extraction</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Extraction.html">页首</a>
<li><a href="Extraction.html#lab390">基本的提取方式</a>

</li>
<li><a href="Extraction.html#lab391">控制提取特定的类型</a>

</li>
<li><a href="Extraction.html#lab392">一个完整的示例</a>

</li>
<li><a href="Extraction.html#lab393">讨论</a>

</li>
<li><a href="Extraction.html#lab394">更进一步</a>

</li>
</ul>
</div>
<h2><a href="Auto.html">更多的自动化&nbsp;&nbsp;&nbsp;&nbsp;(<b>Auto</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Auto.html">页首</a>
<li><a href="Auto.html#lab395"><span class="inlinecode"><span class="id" type="tactic">auto</span></span> 策略</a>

</li>
<li><a href="Auto.html#lab396">搜索前提</a>
<div>
<ul class="doclist">
<li><a href="Auto.html#lab397">变体 <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">eauto</span></span></a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Postscript.html">后记&nbsp;&nbsp;&nbsp;&nbsp;(<b>Postscript</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Postscript.html">页首</a>
<li><a href="Postscript.html#lab398">回顾一下</a>

</li>
<li><a href="Postscript.html#lab399">继续前行</a>

</li>
<li><a href="Postscript.html#lab400">其它资源</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">参考文献&nbsp;&nbsp;&nbsp;&nbsp;(<b>Bib</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Bib.html">页首</a>
<li><a href="Bib.html#lab401">本卷中出现的引用</a>

</li>
</ul>
</div>
</div>
</div>

</div>

</div>
</body>
</html>