The Coq mailing list

[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

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

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!