Coq 中的“功能归纳”策略有什么作用？答案

【问题标题】：What does the "functional induction" tactic do in Coq?Coq 中的“功能归纳”策略有什么作用？
【发布时间】：2018-01-03 11:11:30
【问题描述】：

我在我一直在尝试的这个证明中使用了functional induction。据我了解，它本质上允许人们“同时”对递归函数的所有参数进行归纳。

The tactics page 声明：

战术功能归纳遵循函数的定义进行案例分析和归纳。它利用了函数生成的原理

我认为原理是一些我不知道其定义的技术。什么意思？

在未来，我如何发现这个策略在做什么？（有什么方法可以访问LTac吗？）

有没有更规范的方法来解决我在下面提出的定理？

Require Import FunInd.
Require Import Coq.Lists.List.
Require Import Coq.FSets.FMapInterface.
Require Import FMapFacts.
Require Import FunInd FMapInterface.


Require Import
        Coq.FSets.FMapList
        Coq.Structures.OrderedTypeEx.

Module Import MNat := FMapList.Make(Nat_as_OT).
Module Import MNatFacts := WFacts(MNat).



Module Import OTF_Nat := OrderedTypeFacts Nat_as_OT.
Module Import KOT_Nat := KeyOrderedType Nat_as_OT.
(* Consider using https://coq.inria.fr/library/Coq.FSets.FMapFacts.html *)
(* Consider using https://coq.inria.fr/library/Coq.FSets.FMapFacts.html *)
(* Consider using https://coq.inria.fr/library/Coq.FSets.FMapFacts.html *)

Definition NatToNat := MNat.t nat.
Definition NatToNatEmpty : NatToNat := MNat.empty nat.

(* We wish to show that map will have only positive values *)
Function insertNats (n: nat)  (mm: NatToNat)  {struct n}: NatToNat :=
  match n with
  | O => mm
  | S (next) => insertNats  next (MNat.add n n mm)
  end.

Theorem insertNatsDoesNotDeleteKeys:
  forall (n: nat) (k: nat) (mm: NatToNat),
    MNat.In k mm -> MNat.In k (insertNats n mm).
  intros n.
  intros k mm.
  intros kinmm.
  functional induction insertNats n mm.
  exact kinmm.
  rewrite add_in_iff in IHn0.
  assert(S next = k \/ MNat.In k mm).
  auto.
  apply IHn0.
  exact H.
Qed.

【问题讨论】：

几个 cmets：归纳原理只是特殊的引理，Coq 会为每种数据类型自动生成。例如，通常对数字的归纳是引理nat_ind。 Function 生成这样的引理；根据Function 的文档，此处使用的引理应称为insertNats_ind，而Check insertNats_ind 或Print insertNats_ind 应显示它。在 Ltac 上，文档还说 functional induction (f x1 x2 x3) is actually a wrapper for induction x1, x2, x3, (f x1 x2 x3) using qualid;它的定义应该在FunInd。
您的示例代码缺少一些 Require 以使其正常工作。当战术没有在 Ltac 中编程时，就无法访问“Ltac”，这是大多数 Coq 战术的情况。但是，您可以在使用策略之前和之后使用 Show Proof 来查看它的确切作用。
有一个死链接，你说“战术页面说...”
谢谢，我修复了链接！

标签： coq coq-tactic

【解决方案1】：

“原理”只是意味着“归纳原理”——为了“归纳”地证明某些动机而必须证明的一整套案例。

Coq中Function和Fixpoint的区别在于前者根据给定的定义创建归纳原理和递归原理，然后传入每个返回值（作为lambda，如果有绑定的变量通过案例分析或涉及递归调用的值）。这通常计算较慢。生成的原理与生成的 Inductive 类型相关，其中的每个变体都是函数调用方案的一种情况。后者Fixpoint 使用 Coq 的有限终止分析来证明函数递归的有根据*。 Fixpoint 更快，因为它在计算中使用了 OCaml 自己的模式匹配和直接递归。

归纳方案是如何创建的？首先，将所有函数参数抽象为forall。然后，匹配表达式的每个分支都会创建一个新案例来证明该方案（每个嵌套匹配的案例数量相乘）。函数中的所有“返回”位置都在一些匹配表达式绑定的范围内；每个绑定都是归纳案例的一个参数，它必须在重构参数上产生动机（例如，如果在 list A 的 cons 的情况下，我们有一个 a : A 和一个 list_a : list A 绑定，所以那么我们必须产生一个Motive (cons a list_a) 结果）。如果有一个带有 list_a 参数的递归调用，那么我们将进一步绑定 Motive list_a 类型的归纳假设。

一个真正的 Coq 实现者可能会纠正我上述的细节，但它或多或少是如何从有根据的递归函数推断出归纳方案的。

这一切都相当粗略，在Function 和Functional Scheme 的文档中有更好的解释。

终止分析可能太聪明了。它需要根据proof of False 进行修改（由 IIRC Maxime Dénès，干得好）给定（一个结果）单价公理。

【讨论】：