coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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. 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.."?
--
Sending this from my phone, please excuse any typos!
- [Coq-Club] Understanding the "functional induction" tactic, Siddharth Bhat, 01/04/2018
- Re: [Coq-Club] Understanding the "functional induction" tactic, Pierre Courtieu, 01/04/2018
Archive powered by MHonArc 2.6.18.