coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Erik Martin-Dorel <e.mdorel AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Formalization of the Jordan normal form in Coq
- Date: Wed, 28 Apr 2021 20:52:59 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e.mdorel AT gmail.com; spf=Pass smtp.mailfrom=e.mdorel AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f42.google.com
- Ironport-hdrordr: A9a23:RecxD6G58QL7aOa8pLqFpJHXdLJzesId70hD6mlaTxtJfsuE0/2/hfhz726NtB89elEF3eqBNq6JXG/G+fdOi7U5EL++UGDdyQ+VBa5464+K+UyEJwTf8apn2b5kY+xCDrTLfDtHpOLbxCX9LNo62tmA98mT5Nv263t2VwllZ+VBwm5Ce2GmO3Z7TgVHGpY1faD0jqF6jgGtdngNYsOwCmNtZYj+jubGjZf3JSMBbiRXijWmty+i67LxDnGjr3Ejeg5IqI1SiFTtokjW4uGGv+ugwhHRk1XP54lb8eGM9vJzQOKLjMYRJnHAqCaNIL5gVbqLoSwvrIiUhWoCoZ3jpREvOsg20XfNZyWOpwf30QWI6lkTwk6n8lOTjXv9rcGRflwHN/Y=
- Ironport-phdr: A9a23:m0vfshSaJ0/3/cqH+fwEqqVQl9psov2YAWYlgqEPu/d1aq2muq7aFwnh351FslbFUM3h5u5ejKKO6ua8AD1Gu8zb+ylaK9RlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMssQam5VuJrgvxhfGv3dEZ+pbzn50KFyOmBrx+t2+94N5/SRKvPIh+c9AUaHkcKk9ULdVEjcoPX0r6cPyrRXMQheB6XUaUmUNjxpHGBPF4w3gXpfwqST1qOxw0zSHMMLsTLA0XTOi77p3SBLtlSwKOSI1/H3Rh8dtiq9QvRCvqAFlw4PMb46VOvhxfrndc90URmRPQ9hfWDBaD4ymc4cCFfAMMfpEo4T/oVYFsBuwBROrBOPq0jJGiWX23aw50+88Fg/JxhYgH84PsHTStdn7OqASUfqrw6nM0D7OaO1Z1S346IfVdRAhu++DXbZrfMrezEkgDQLFjlGKpYP5ODOV0/0Avm6G5OVvSeyhkXQoqx1tojex3McsjJHEiIIVx13F6Cl3zps4KcG3RkN0fNKpDZ9duS6VOoZ2TM4vQW5mtDsmxrEYp5K2fCwHxpQnyRDRdvCKfYuF7xDgWeuXPDx2inVleLeliBaz90it0uz8Vs+u0FZLtCVJiNfMtmoV2xPJ9seHT+Fx/kC72TaAzwzT7/tLIVoolaraLZ4t26M/lp0JsUvdGi/6gkL2jLWZdkgi5+Om6Pznb634qpOAM4J4kALzP6Q0lsChHOg1MRICUmeF9em6ybbt51f2QK9Qgf0ziqTZsI7VJcAcpqOhBg9ayIcj6xKmAzi40tQUgGALLFxKdR6ZlYTpNFbOIPf3Dfe7nVugiitkx/fDPrH5A5XNKGbMkKv5cLpj90JRzBA/wNNf6p5OFL0NPfH+VlX+udDGFhM5Nha7w+fjCNVzzIMeXmePD7eHP6/ItF+H++UvI/OSa48Rozv9JP0l6OTvjX89g1MSYa6p3Z4PZHCiAvtmO1mZYWbrgtoZDWgKuRM+QPX2h12GTD5cfG2/X7k85zE+EIKpF53PRoGrgLyb3Se0BIdaZm5cCgPELXC9fIKdHvwIdSi6I8l7kzVCW6LycYI50QCSs1r30btkaO/d4DEZs9fv08J448Xekwp38S1zCYKayW7eYXtzmzYlXT41lIV2u1B8zBKv1rJ1h7QMGJpW6/RTXwMSOpvVzug8ANf3DFGSNuyVQUqrF431SQo6Scg8lodmS3Y4IM2ri1X45wTvA7IRkNSjAZU19ufR3SG0KZonjXnB06Ylgh8tRc4dbQWOtutE7wHWQrXxvQCcnqeue74b2Ubl+2KKzG7It0ZdAlcYeZWAZmgWYw7tlfq8/lnLJ5ehDL0mNk1KzsvQcsN3
Hello,
See also Guillaume Cano's PhD thesis:
the accompanying formalization being available at:
with:
- the Jordan normal form;
- the Bolzano-Weierstrass theorem;
- the Perron-Frobenius theorem.
Best,
Erik
Le mer. 28 avr. 2021 à 18:49, Mohit Tekriwal <tmohit AT umich.edu> a écrit :
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.2854073Thanking 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
Archive powered by MHonArc 2.6.19+.