I have used functional induction in this proof that I have been trying. As far as I understand, it essentially allows one to perform induction on all parameters of a recursive function "at the same time".
The tactics page states that:
The tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle generated by Function
I assume that principle is something technical whose definition I do not know. What does it mean?
In the future, how do I find out what this tactic is doing? (Is there some way to access the LTac?)
Is there a more canonical way of solving the theorem which I pose below?
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.
The "principle" just means "an induction principle" - a complete set of cases that must be proved in order to prove some motive "inductively".
The difference between Function and Fixpoint in Coq is that the former creates an induction principle and recursion principle based on the given definition, and then each return value is passed in (as a lambda, if there are variables bound by case analysis or there is a recursive call's value involved). This generally computes slower. The principles generated are with respect to a generated Inductive type, each variant of which is a case of the function's call scheme. The latter Fixpoint uses Coq's limited termination analysis to justify the well-foundedness of a function's recursion*. Fixpoint is faster, because it uses OCaml's own pattern matching and direct recursion in computation.
How is the induction scheme created? First, all the function parameters are abstracted into a forall. Then, each branch of a match expression creates a new case to prove for the scheme (the number of cases multiplies for each nested match). All the "return" positions in a function are in scope of some number of match expressions' bindings; each binding is an argument to an induction case that must produce the motive on the reconstructed arguments (e.g., if in the case of a list A's cons, we have an a : A and a list_a : list A binding, so then we must produce a Motive (cons a list_a) result). If there is a recursive call with the list_a argument, then we get a further binding of an induction hypothesis of type Motive list_a.
An actual Coq implementer will probably correct me on the specifics of the above, but it's more or less how induction schemes are inferred from well-founded recursive functions.
This is all fairly rough, and better explained in the documentation on Function and Functional Scheme.