The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,




2018-01-04 10:30 GMT+01:00 Siddharth Bhat 
<siddu.druid AT gmail.com>:
> Hello everyone,
>
> I've been trying to write proofs about maps in Coq, and in doing so, I found
> that the module FMapList.v uses functional induction.
>
> So, I used the same in my proofs, and "it works". However, I lack any
> insight as to what it does and how it does it. If I wish to understand this,
> how do I do so?
> The documentation mentions:
>
> The tactic functional induction performs case analysis and induction
> following the definition of a function. It makes use of a principle
> generated by Function

The doculentation says: "(see section 2.3)" and "(see section 13.2)",
this is where you can find more details about the principles
geneerated.

> What does it mean when it says "it makes use of a principle.."?

This question suggests that you should first read the documentation
about inductive types and there induction principles. Look for
instance at the type of the following principles (generated
automatically from bool, nat and list): bool_ind, nat_ind, list_ind.

The principle here is to be understood as the "induction principle"
similar to the one generated with each inductive, but tailored for
reasoning about the function.

In short:
When defining a function f with keyword "Function", several automatic
term generation procedures are triggered. Some of them can be
triggered later by using "Functional Scheme" with some subtle
differences.

1) An inductive R_f is generated, it defines the graph of the
function. Say f is of type nat -> bool -> bool, then f_R is of type
nat->bool->bool->Prop and such that f x y z is provable iff f x y = z.
2) f itself
3) Proofs of correctness and completeness of R_f wrt to f. Named
R_f_complete ans R_f_correct.
4) Proof of the equation of the function. Named f_equation.
4) An induction principle f_ind (f_rect and f_rec too actually), that
looks a bit like the one of R_f (named R_f_ind) but specialized to
proving goals about f.

The two following tactics make use of these generated terms:

- "functional induction f x y" is more or less a shortcut for
"induction f, x, y, z using f_ind".

- "functional inversion H" is more or less a shortcut for "apply
f_ind_correct in H; inversion H".


Last point: In the case of a non structural recursion, a few more
things are generated to allow the definition of the function itself.

Best,
Pierre


> Stack overflow question about the same thing with an example (Raw Link:
> https://stackoverflow.com/questions/48076202/what-does-the-functional-induction-tactic-do-in-coq?noredirect=1#comment83143293_48076202)
>
>
> Thanks,
> Siddharth
>
>
> --
> Sending this from my phone, please excuse any typos!