coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Mohit Tekriwal <tmohit AT umich.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Formalization of the Jordan normal form in Coq
Date: Sat, 1 May 2021 17:33:26 +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-pj1-f41.google.com
Ironport-hdrordr: A9a23:1n/Z66BSvUgFarrlHejTsceALOonbusQ8zAX/mp2TgFYddHdqtC2kJ0gpH3JoRsyeFVlo9CPP6GcXWjRnKQe3aA9NaqvNTOW31eAA5pl6eLZsl7dMg34stVQzKJxN5V5YeeAdWRSqcrh+gG3H5IBzbC8gduVrMPfy3socg1wcaFn6G5Ce2OmO3Z7TgVHGpY1faD0jqEmmxOadXsadci9DHUeNtKzweHjr576fQUAQycu9Qjmt1KVwYTnGBuV1Ap2aUIq/Z4e9wH+4nXEz5TmnfX+7hPHzWfc49BthdP9xrJ4aPCku4w6LDPjjwrtSaZAf/m5vD4zqPyy81pCqrTxiiZlEcJ05XbcOluwvAKo4Q/9yzwjgkWM9XaoxV/qocn0X1sBerB8rLMcSRfS50o+sNwU6sx2414=
Ironport-phdr: A9a23:oQhftRZvfNsJcZUuI+b9G9T/LTF914qcDmYuwqpisKpHd+GZx7+nAna3zctkgFKBZ4jH8fUM07OQ7/mxHzZavt3Y6S5KWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAHcutMIjYd8KKs9xQbFrmZJdu9L2W5mOFWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy247ab52aO/RjcK3dc80USmhCUMhWTCFOGJ+wb44VAuoBIepVrY/wrEYOoxukAgmsAfvixDhPhn/23K06z/kqHx/Y0wwjBdIOsXrVo8/xNKwPVu210KzIzTLDb/NXxTfw85XIchUgof6QXbJ8a9TexlQyFw7ciFibtIPqMS+P2OsXr2ib8/RvVfipi2M/qAx9vDaiy8gsh4TKmo4byk7J+yp6zYsoK9C1SUF2bNG5HZVetiyWK5V7T8ImTm9mtis3zrMIt5G5cSUWxpkr2hjSYOGJfYiP5xLsTueRITFgiXJkfrK/nRey/lK6xu3yTMm4yExFoTZAktXWsXANzRPT5tCCSvRn5EehxTeP1wbK5u5ZJkA0j7TUK5o7zr43jJoTvkLOFTL1lkXulKKaaFko9+yy5+nkYrjqvIGQO5J1hw3kPakih9SzDfo3PwQSX2WW/Pqw2KH+8UD8WrpGkuE6nrfcvZ3eJ8kWqau0DgBJ3oss9xqyCjOr3MockHYdKV9IewyIgJToNlzLI/34A/iyjlWqnTx23f7JJKfhDY/ILnXbkLfuY7J960lExQo2199f5pZUBqgZIPLxR0P9rdLYAxAkPwCuzObnD9J91owaWW2RGKOWLKTSsVqQ6uIuJemDepMVtS7jJ/Q54/Pil3w0lF8HcaW3wJcaaWq0E/t7L0mBZHrjmNYBEWMEvgokS+zqjUWPUSJWZ3a1X6I85y07BZm7DYfGR4CinLyB0D2lEZJLe2BKEkqMHmvwd4WYR/cMbzqfLdNmkjwdTLSuV4sh1Qy1uwLh0LpmLu/U+jUCup751dh14ffTlRAo+jBuAcSdyTLFc2YhlWQRAjQywapXoEpny17F37IrreZfEIl24PNITk8GOJ3GzvNzD5imRgfGftaVYEujQ96mRzw9U4RikJc1f09hFoD63Vj41C2wDupN/5S7Qacs+6eZ5EDfYsN0ynLIzq4k53E7R8pENSurirMtrmD7N8vyi0yc0p2SW+EExiel3HqGzGGO+kxUTVwoOY31GEsHb06TluzXo0PPS7jGIbEuMw8E0czbb6UWM5vmilJJQPqlM9PbMTrZpg==

Thanks Erik for reaching out to us !

On Apr 29, 2021, at 12:22 AM, Erik Martin-Dorel <e.mdorel AT gmail.com> wrote:

Hello,

See also Guillaume Cano's PhD thesis:
https://www-sop.inria.fr/marelle/Guillaume.Cano/these.pdf (in French)

the accompanying formalization being available at:
https://www-sop.inria.fr/marelle/Guillaume.Cano/
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.2854073

Thanking you,
Mohit Tekriwal,
PhD candidate,
University of Michigan, Ann Arbor.

--
Érik Martin-Dorel
http://erik.martin-dorel.org/

Re: [Coq-Club] Formalization of the Jordan normal form in Coq, Mohit Tekriwal, 05/01/2021
- <Possible follow-up(s)>
- Re: [Coq-Club] Formalization of the Jordan normal form in Coq, Mohit Tekriwal, 05/01/2021