coq - "functional induction"策略在 Coq 中有什么作用？

Question

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

The tactics page指出:

The tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle generated by Function

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

将来，我如何找出这个策略在做什么？ (有什么方法可以访问 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.

Answer 1

“原理”只是指“归纳原理”——为了“归纳”证明某个动机而必须证明的一整套案例。

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

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

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

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

• 终止分析可能太聪明了。它需要在 proof of False 之后进行修改(由 IIRC Maxime Dénès，干得好)给定(的结果)单价公理。