Coq中functional induction策略的作用及证明优化问询

Let's break down your questions one by one, starting with how functional induction works, then how to dig into its implementation, and finally a cleaner approach to your theorem proof.

1. What's the "principle generated by Function" mentioned in the functional induction docs? #

When you define a recursive function using the Function command (instead of Fixpoint), Coq doesn't just create the function—it also generates a custom induction principle tailored to that function's recursive structure.

For your insertNats function, which recurses on the n argument, the generated principle captures exactly how the function unfolds:

• For the base case (n = O), the function returns the input map directly.
• For the recursive case (n = S next), the function calls itself on next and then adds a key-value pair.

This principle is what functional induction uses to automatically set up the right case analysis and induction hypotheses for your proof. Unlike standard induction (e.g., on nat), which follows the type's built-in induction rule, functional induction follows the function's own recursive steps. This is especially useful for functions with complex recursion patterns (like mutual recursion, or recursion on multiple arguments in a non-trivial order) where standard induction might not align well with how the function works.

You can see this generated principle for yourself! After defining insertNats with Function, run:

Print insertNats_ind.

This will show you the exact induction principle Coq created for your function.

2. How to learn more about functional induction's inner workings? #

Viewing its LTac implementation #

You can inspect the LTac code behind functional induction directly in Coq:

1. First, locate where the tactic is defined:

   Locate functional_induction.
   

   This will confirm it's part of the FunInd library.
2. Then print the LTac definition:

   Print Ltac functional_induction.
   

   This will show you the high-level tactic code that orchestrates the induction using the function's generated principle.

Diving deeper into the source #

If you want to see the full implementation (including how Function generates induction principles), you can look at Coq's source code:

• The FunInd plugin lives in the plugins/funind directory of the Coq repository.
• The core logic for generating induction principles is in files like funind.ml and funind_common.ml.

Additional resources #

The Coq Reference Manual has a dedicated section on Functional Induction that explains the theory and usage in more detail (no external links needed—you can access it directly through Coq's built-in documentation or the official Coq docs site).

3. A cleaner proof for insertNatsDoesNotDeleteKeys #

Your existing proof works, but since insertNats is a simple recursive function on nat, you can use standard nat induction instead of functional induction—this is often more straightforward for cases where recursion aligns with a built-in type's structure. Here's a more concise, idiomatic version:

Theorem insertNatsDoesNotDeleteKeys: forall (n: nat) (k: nat) (mm: NatToNat),
  MNat.In k mm -> MNat.In k (insertNats n mm).
Proof.
  intros n k mm H.
  induction n as [|n' IHn'].
  - (* Base case: n = O *)
    simpl. exact H.
  - (* Inductive case: n = S n' *)
    simpl. rewrite MNat.add_in_iff.
    (* Either k is the new key we added, or it was already in the map from the recursive call *)
    right. apply IHn'. exact H.
Qed.

Why this is better:

• It uses standard induction, which is more familiar to most Coq users and avoids relying on the Function command's generated principles.
• The proof steps are explicit about the structure of nat, making it easier to follow.
• We don't need an extra assert—the add_in_iff lemma directly splits the case into "k is the new key" or "k is in the recursive map", and we just need the latter since we know k was in the original map.

If you still prefer using functional induction, you can simplify your original proof too:

Theorem insertNatsDoesNotDeleteKeys': forall (n: nat) (k: nat) (mm: NatToNat),
  MNat.In k mm -> MNat.In k (insertNats n mm).
Proof.
  intros n k mm H.
  functional induction insertNats n mm.
  - exact H.
  - rewrite add_in_iff. right. apply IHn0. exact H.
Qed.

The assert was unnecessary here—since we know k was in the original map, it must be in the recursive call's result, so we can directly apply the induction hypothesis.

内容的提问来源于stack exchange，提问作者Siddharth Bhat