Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs


Chronological Thread 
  • From: Ken Kubota <mail AT kenkubota.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Interesting uses of Second order theorems in Coq proofs
  • Date: Fri, 10 Jun 2022 15:14:25 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT kenkubota.de; spf=Pass smtp.mailfrom=mail AT kenkubota.de; spf=None smtp.helo=postmaster AT plasma5.jpberlin.de
  • Ironport-data: A9a23:VHPPMKMZJwvk6UTvrR2/kcFynXyQoLVcMsEvi/4bfWQNrUog1jUFy mQcUWCAOfyLNDCmc9hxPouy9UIGuseEmIIxSnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EsLd9IR2NYy24DnWlvV4 7senuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB2jv5Ng2 e4duaCfagcTbpyPpuMMFAhXRnQW0a1uoNcrIFCntcWIykSbNXn0yfh0CEAwe4EVkgp1KTEWs 6ZEcXZQPlbY2Ypaw5rjIgVorsEqLc3DP44ZuWxqyi3QS/orKXzGa/yUuYQAhmZr7ixINfvlT dAaQh9zUCXJOU1NC0VHBqw7wc790xETdBUD8Q/L+fVui4TJ9yR616GoO97IcPSRVMBNlwCZo HjH9iL3GHkn2Me30T6M6Xel26nNhSn2QoYTEvu0+5aGnWF/2EQ5KF4HRGDrrcWWqU6EC+McF UsFvTsh+P1aGFOQcvHxWBixoXihtxEaWsZNH+BS1Dxh2pY48C7EXDVfFGcphMgO7ZRqHWVwv rOct4mxbQGDpoF5Xlqx2994RxuYNDIRLGlqicQsFFNcuoiLTG0bqhvJQp5JHbSxj9udJN0d6 yiOpTM7juhVj9YB2r+//FaBjz/ESnn1ouwduVi/soGNtFoRiGuZi2qAtQSzARFocdzxc7V5l CJY8/VyFchXZX13qASDQf8WAJai7OufPTvXjDZHRsd8q2v8qiL4JdELulmSwXuF1O5aIVcFh 2eN6GtsCGN7YBNGkIcsM97pYyjU5fG/SbwJqcw4nvIVO8UvKFDelM2fTU6d3mbpnUkq1LoiI Y+ca9rkAnMQCcxaIMmeGI8gPUsQ7nlmnwv7HMilpzz+iOr2TCPLFd8tbQXfBshkvPLsiFiEq L53apraoz0BC7eWSneMruYuwaUidiVT6Wbe8JAMKYZu42NORAkcNhMm6eJ4INY/wvkOzY8lP BiVAydl9bY2vlWfQS3iV5ypQOqHsU9XoS1pMCoyE0yv3nR/M4+j4L1GLck0cL8k6eZk0fcyQ /RcI5eMBfFGSzLm/TUBbMCh/dI4K0nx3VqDb3i/fTwyX598XAiVqNXqSQ3iqXsVBS2tuMpi/ rCtj1uJQZcKSwl4ItzRbfajkwG4sXQHwbggXEbOIcRZf1nltoRncnSjgvgyKsAKCBPC2jrDi 1fIW0hF/7GVrtZsotfThK2Co4O4KMdEHxJXTzvB8LK7FSjG5W7/k4VOZ+CFIGLGX2Tu9aT+O OhYwq2uMPADm1oW4YNwH6wynPAm49L0orYHiAZ8FnjRa1WtTL9teyHU0c5Kv6xL57lYpQrvB hPRoIYHY+3RNZO3CkMVKSokcv+HiaMelA7U4KlnO079/iJ2oOeKXBkAJRWKkyABfrJ5PJl8k LU5vMcN7gXizBgyONuciiFSsWiBdyRSX6Iiv5AcIYnqlgtylgAcO8OBUHeu7cHdcchIP2krP iSQ2PjIiYNayxeQaHE0D3XMgbdQiJlmVMqmF7Pey4llW+Yph8PbGDVJ9T0sSw0IiBdf2e9pP mltcUF4TUlLE/GEm+AbN11A2SkYbPFaxqA141gEkm7ERU60XyrBIQXR/M6TqVsB/Ts0kidzp dmlJaWMbdouVML82CgvU0l5orrvQLSdM+EEdN+PR6y4InXxXdYpbmJCq4bFR9sLzP7dXHH6m NQ=
  • Ironport-hdrordr: A9a23:cy2ZWaxrMikz/d6VmAtLKrPwJ71zdoMgy1knxilNoHtuA6mlfq GV88jzsCWftN9/YgBDpTntAsm9qDbnhP1ICPcqTNOftXjd1ldARbsKheCOrwEIWReOkdK1vp 0AT0ERMqyXMWRH
  • Ironport-phdr: A9a23:3VOM+RPNjHzEXsglj8Al6naABhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r1QaQFtiLo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJfglEmSexbbxyI Ri1sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KOCI2/2/KisJ/jqxVrh2iqRxx3YDZe52VNON7fq/BYd8WWWhMU8BMXCJBGIO8a I4PAvIEM+lGqYn2ul4ArQalCgmrGOPg0CJDi3jz3aIg0uQhFRrL3A8+ENIIs3TUsc76NKAOU e+v1qXH0CvMYupQ1Dzg54fGbgovruuQXbJsb8XR008vGhvLg1iNpoHoPT2b2voQvmWa6+dsS f6jhmEppQ1svDSi2MQhh4vHiI8I1FzJ9CZ0zYk7KNClRkN2fMCpHIdeuS+VMYZ9X80sQ2Ztu Ckgy70Gv4a2fC8EyZQjwB7fZfmHc4mO4h39TuaRPy13iGhjeL2hmxa+6VWvyur9VsWu11ZKt CVFn9/RvX4Ozxze8suKRudn8ku/1juDyhrf5+FHLEwum6fWKoYtz7oumpYJrEjOGiD7lF/yg aKYbEkp/uml5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxAWX2if4+u8z7jj8lf5TblQjP02i rLWv47AJcQfp665BRVZ3Zs95BqnDjem1soXnWUfIV9GZB6LlZblNl7TLPziDfqygE6gnTlqy vzeO73uGJTNLnzNkLf7erZ97lZRyA8pwtBe45JZEbIBL+z1Wk/yqdzXFRg5MxCuzOr9Fdpyy JsSWWSUDaCBKqPdrUeI5v4zI+mLfIIZpS7xK+I56P72kX85hVgdcLG10psQcXC0B+hpI0GEY XX3mdoBCmcLvg8mTOPwklGCUDhTZ2yzX60m/D07BpimXs//QdWmh6XE1yOmFLVXYHpHAxaCC yTGbYKBDtQBbmqxP8VmjjVMAb2oSosJ1hyotxLwzKZuaObZrH5L/an/3cR4srWA3So58iZ5W pz1OwClSmh1mjhNXDoqxOVkplQ7zF6f0K9+ivgeFNpJ5voPXB1pfYXEwblcDNb/EhnEYs/PU EyvF9CvADUZTd83wMIEZFp0Xdmv3VjYxyT/O7YOjPSQAYAstKfV3nz/PcF4nnPP1a0JjFQgQ dZFMnGvwKJypEDIH4CctUKfmu6xcLgEmi7A8GDW1W2VoERRSxJ9S43dWXkEY0KL69bh7E7YS 76oT7gqWudY4eiFLKYCKtjgjFEdAezmJMybeGWp3WG5GRePwLqIKovsYWQUmivHWgAClEgI8 HCKOBJbZG/pqn/CDDFoCVPkYl/9ueh4pnShS0YozgaMJ0R/3rux8xQRiLSSUfQWlr4DvS4gr X1zEjPfl5rTAtuEjwlseqZBa9Qh6RFL2CORtgBwOIChM7E3nkQXIEx8u0Lj0QkyC50VwZBs9 i9zilcib/nGgzYjP3uC0Jv9O6PaMDz39RGrMOvN303Glc2R4uEJ4eg5rFPquEeoEFAj+jNpy YowsTPU65PUAQ4VSZ+0XFww8k0worjbZgE+6oXXyHdrLaDyvjKIiLdLTKM1jw2tedtSKvbOE QbzF+UZCs6tNeYth1HvYh9Ob6hCsaUzOc2hbf6P3qWmaf1hkDyRhmNC+Ilh00iI+kKQU8bw1 o0ei7Gd1wqDDHLniUu599vwgcZCbC0TGWy2zW7lApRQb+t8Z9RDBWCrKsyxjtJw4vylE3tR9 VqLBF4A29KjfgabKVDwlQFdzkUYp3W7lDDwn2QyyW1w6PfPmneQi+35PAIKIGtKWHVvgTKOa cCvgtYWUVLpJwklmR255Frrkq1SpaBxNW7WEg9Deyn7KX0nU7Pl5uLEOZIWrs54934JA4HeK RiAR7XwogUXyXbmFmpan3Ugci2y/47+h1p8gX6cK3B6qDzYf9txzFHR/o+5J7YZ0zwYSS1/k TSSCEK7Oozj+NyVk7/Av+a9SmimSpQVfSShnubi/GOroHZnBxGyhaX5n9TmFSA53Cn4ytNtS SyOoBu2McH7kq+9N+xgZExhAlTxvtF7Fo9JmYw1nJgM2HIei8bwnzJPgSLpPN5cw667cGsVS GtB3YvO+Aa8kh4rPjeTyon+THnY3sZxe4zwfDYNwixkiqICQKaMsO4UxW0v/gP+8FyXOb8nx X8c0ad8uCZc2b1Q/ld9iH3aWOxaHFEEb3210U3Zv5bk8f0RPCH1Ld3SnAJ/hYzzVeDf5FgEH iyhKtF6WnUspsRnbACWiSa1sNm/PoOLPZRL8UfJ9nWIx+lNdsBrzqJT13Q4MjCn5SB9mbdj0 U48ms/m9N+OL2EnlE6gKjhfMDC9J8Ya+zW2yL1bgt7TxIe3WJNoBjQMWpLsC/OuCjMb8/r9Z U6IF3Unp3GXFKC6f0fX4Vp6r3/JD5GgNm2GbHgfw9J4QRCBJUtZyAkKVTQ+l5Q9G0ik3svkO Et+4zkQ4Bb/pH4ugqpwMALjV27EuAqyQi8wQYOaJUcQ7BlI6l3RMMrY4u8yVyBU85u9rRCcf 2yWYwMbaANBEkeABl3lIvyv/YyQq67CWrP4cquIOuvdzI4WH+2Fzp+uzIZ8qjOFN8HUe2JnE +V+wU1bG3ZwB8XenTwLDS0RjSPEKcCB93LesmV6qN6y9PPzVUfh/4yKXvFXONRr0xO7h6SeP emMjWB1JHwLs/FEjW+N07UZ0FMI3mt2cCKxFL0bqSPXZLrUk7RSBkNdaTt5OdFM7qR60gQHa qu5wpvlk7V/iPAyEVJMU1fsz9qoacI9KGa4LFrbBUyPOdxuwBXIzsf0fKm7VbQWgOgG73VYV h6YHkngIz6EizCvWx39aImkbQmDOBVFvYjgNBR1A2X5SNPgLBG2YocfsA==
  • Ironport-sdr: q9hfoQZcMF0ZiYhwqPuQC9xSsqGEdcu3dL5MXkhSbkG7dbBNHo0bYAfeDsusKzVXIlqr/f27VJ SdsHe3XlTIqj+i41nYY8yTB/4+awGyvn6u9OmUNe9gYPxJdFajn8+VGo3ep3xrJE4+5PNLBILS GlAV8VmOTWJmNnT+21gThDHP1yOU8lNggDmdM9e9Sm1TtEpCwOOVBXk1O8TCBoU92jyNs4X7g6 KCw2E0BTmYs1d++bJ+3ofOn38H/EcUfClO2u+3xoJ/XcchsJ0jzBGBBAF/XVQ5LYvIWzS+DDfW JZm+GjGi5Z6aOgtSqQAmbAQ4

Although it is not a Coq proof, this is a good example for a second-order
lemma:


https://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/

Group theory can't be expressed properly without second-order types, which
are missing in HOL.
Mike Gordon had suggested these, but the main implementations currently still
lack this important feature.
I had implemented this in a Hilbert-style system based on Peter B. Andrews'
logic Q0.

See, for example, the group definition on p. 362 here:

https://www.owlofminerva.net/files/formulae.pdf#page=362

The second-order language has a more complex universal quantifier.
Read "∀g[λa." as "for all a of type g".
And since it is a raw software implementation, it doesn't use infix notation,
but the operator (here represented by the operator variable "l")
and the boolean connectives are on the left hand side,
such that "a∧b" is stated as "∧ab" and
"for all a of type g: a l e = a ∧ e l a = a"
(the properties of the identity element e of a group (g,l) with operator l on
the set g)
is expressed as
"∀g[λa.(∧(=(lae)a)(=(lea)a))]" (p. 362).

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100



> Am 09.06.2022 um 06:14 schrieb kirang <kirang AT comp.nus.edu.sg>:
>
> Hi Coq Club,
>
> For various reasons, I'm currently doing a light survey of examples of
> interesting uses of second order properties/lemmas in Coq proof scripts.
>
> Currently, the main examples I've found in the wild have mostly been using
> various induction principles for custom datatypes and the such (found
> through searching Github/using Coq's search mechanism).
>
> I've seemingly exhausted searching through Github for now and so I thought
> I might reach out to the magnanimous wisdom and experience of the Coq club
> community in this search.
>
> Do you have any interesting examples of other classes of second order
> properties (i.e other than induction principles) you have seen/used in your
> own proofs?
>
>
> Thanks,
> Kiran.




Archive powered by MHonArc 2.6.19+.

Top of Page