Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Understanding the "functional induction" tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Understanding the "functional induction" tactic


Chronological Thread 
  • From: Siddharth Bhat <siddu.druid AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Understanding the "functional induction" tactic
  • Date: Thu, 04 Jan 2018 09:30:51 +0000
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f181.google.com
  • Ironport-phdr: 9a23:RsP9rhRP/jneY4lm2rWdeZNTHtpsv+yvbD5Q0YIujvd0So/mwa69bBSN2/xhgRfzUJnB7Loc0qyK6/mmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfa5+IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27XhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBEusBMvtFoIn9vVQOtwe+BQmxD+7yyj9HnGP21rA93uQ6EAHJwREvH88UvHvJttX1KaYSXv2uwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTfzkkvEhnKjlSWqYH9MDOV1/gNs2iG7+V7T+6gl2knqwRprji02scjkJXGhoESylDa6yp52og1Jdm/SE91e9KrDJxQtyScOoBrQc0iW3lltDgmxrACo5K2fygHxI45yxLCavGLaZWE7xH+WOuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2xzK9siLVuJx/km81TuMygzf8O5EIUczlarUL54u3KQ8mYYUsUTGBiP2mUP2g7GKdkg85OSk9+Dqbq/lq5KcLYN4lBzyP6U0lsCiAuk0LxACX22B9uS90L3j81f5QLJPjvAuianZsY3VKtkGpqKjHgBVyJsj6xeiADq939QYmGMILFNBeB6dk4fpPFTOLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g4gZQCeEBrKTGKLUq16BoOw1cMeWY4pAgzfxJ/gs/eLuxVU5kENVKbKo0ZcKLnyiA/VqC0qcaHvoxNwGFDFZ7UIFUOX2hQjaAnZobHGoUvdk6w==

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!



Archive powered by MHonArc 2.6.18.

Top of Page