coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formalization of the Jordan normal form in Coq

From: Mohit Tekriwal <tmohit AT umich.edu>
To: coq-club AT inria.fr
Cc: Jean-Baptiste Jeannin <jeannin AT umich.edu>
Subject: [Coq-Club] Formalization of the Jordan normal form in Coq
Date: Wed, 28 Apr 2021 21:39:38 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tmohit AT umich.edu; spf=Pass smtp.mailfrom=tmohit AT umich.edu; spf=None smtp.helo=postmaster AT mail-pf1-f170.google.com
Ironport-hdrordr: A9a23:HwtTKamwLMb84XPGzBx+omScon3pDfL03DAbvn1ZSRFFG/GwvcaogfgdyFvImC8cMUtPpfmsMLSNKEmyybdb+o8UVI3OYCDDmE+FaL5v9pHjxTqIIU3D38pQz71pfaQ7KPCYNzNHpP336gW5DNosqePvmJyAv/vUzHtmUGhRAZ1I0gERMGqmO3FtSBIDLZQ0E4f03Kt6mwY=
Ironport-phdr: A9a23:sgHZEhwRHu/Qrh7XCzKYzVBlVkAck4WxBRYc798ds5kLTJ7L16rrMEGX3/hxlliBBdydt6sVzbCM6eu+AiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagZb5+Ngu6oRvPusUZgIZvJLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6mb4YXD+QOIelXoZT+qVUAsxWwAhKhC/nzxj9NnHL23bE23/onHArb3AIgBdUOsHHModvyM6cSUeG1zLXVxjvdcfxW2i396InGcx87pfGHQLV9cdbUyUkoFwPFj0mQpJf4PzOQ1+QCr2ib4/B+Wu2ylm4qsgd8qSWgyckwkIfGnJ4Vykza+iVjxoY4PcO1RVJ0b9CqH5ZeuD2XOoV4TM4jXWxltzo3x6MIt5O4YiQH1pspywDcZvGbbYWF4hLtWuaPLDp2h39rd7yyihW0/EO9xOP8Ucy030xLripDitTDrGwC1xnJ5siAUPt98UGs0iuM2QDL8uxIP1w4mK7BJ5MiwrM8jIQfvVnfEiPshUn7jrOael069uWn9+jqYrDrqoGAO4NpjwzxKLgiltChDek9NgUBQmyW9OG+2bDn40L2XrBHg/k2n6TXrJzXINoXqbSkDwBP14su6RmyAji739kegHIJNkhKeAidgIjsI1zOIO73DfO4g1m0lTdk3fHGPrn4DpXVIHjPja7tfbhg50Ne1AY/199f55VTCrEOJPL8RFX9u8DfDh88KwC0wuDnB8th1o4GR26DHquUPLnRvFKI/O4jPfSAaJMPtDrgKfUp++bijXojll8ceamp04EXaHe9Hvl+P0WZZH3sgtcAEWcWpQc+UenqiFyeXj5TfXq9Qb8z5iwjBIK8EYjDXpytgKCG3CqjApJWYXlGBkmQHnfsaoWLQOwBaDmSI89kijwLT6KtS44n1RG0tQ/10aBrLuTO+n5QiZW2399soubXiBsa9DpuDs3b3XveYXtzmzYtQD83wOhDrE9ny0iK1eAsn/lfFd1Pz+5MUww6c5PQ0ropWJjJRgvdc4LRGx6dSdK8DGR0F4ppq/c+Jn1lEtDntSjtmiqnB7h9v7mCBZhx6qyFmnaoeJ47xHHB260syVIhR5kXXUWWw5Vn/g2WPLbn1l2Dns6CaKEd1y6L+WuenzLmlHEdaxZ5VOD+ZV5aY0LXqdrj4UaqZ6KrCL8ndAZN1JzbQpY=

Hello,

We have been attempting to formalize spectral radius and norms of matrices in Coq proof assistant. One of the bottleneck in this formalization is the formalization of Jordan normal form in Coq. Does there exist formalization of Jordan forms in Coq ?

We found a formalization in Isabelle/HOL: https://dl.acm.org/doi/pdf/10.1145/2854065.2854073

Thanking you,

Mohit Tekriwal,

PhD candidate,

University of Michigan, Ann Arbor.

[Coq-Club] Formalization of the Jordan normal form in Coq, Mohit Tekriwal, 04/28/2021
- Re: [Coq-Club] Formalization of the Jordan normal form in Coq, Bas Spitters, 04/28/2021
- Re: [Coq-Club] Formalization of the Jordan normal form in Coq, Erik Martin-Dorel, 04/28/2021