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

Question

我一直在尝试的这个证明中使用了functional induction。据我了解，它本质上允许对递归函数 "at the same time".

的 all 参数执行归纳

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

"principle" 只是意味着 "an induction principle" - 一组完整的案例，必须证明才能证明某些动机 "inductively".

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

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

类型的归纳假设

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

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

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

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

What does the "functional induction" tactic do in Coq?

coq

coq-tactic