coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Cc: Jean-Baptiste Jeannin <jeannin AT umich.edu>
Subject: Re: [Coq-Club] Formalization of the Jordan normal form in Coq
Date: Wed, 28 Apr 2021 20:04:00 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl1-f172.google.com
Ironport-hdrordr: A9a23:riBj/K0pI9INuF+cD8tODgqjBaNyeYIsi2QD101hICF9WMqeisyogbAnxQb54QxhJU0ItPKhHO27QX3a/YNo+oV5B9yfdSTvpWfAFuBfxKTvzzDqEyf9ss5xvJ0QFZRWJ8b3CTFB4frSxQmjDpIB7bC8gdmVrMLf1WoocQZxd6p75Rx4AQrzKDwMeCBiBYAlUKaa/NZNvTC6eX8aKv28HGRtZZm4m/TutLbLJSELHAQm7g7mt0LV1JffHwKD1hkTFxNjqI1DzUH/nwb05rquvpiAo3e360bp441SiJ/dzLJ4a/CksNQfKTnnl2+TCbhJZrvqhl4IidDqwFwhlsXKvgoxJsgb0QKoQkiF5THk3xDp0DgogkWSq2OwsD/Gi4jEXj4gYvAx4r5xQ1/840oksMoU6tMp40up86FaFBXagWDU7MTTW3hR5y6JiEtnm+YWlnReX4wfZdZq3OkiwH8=
Ironport-phdr: A9a23:ZiZPiRBQqmhItGQ8siyVUyQULkQY04WcBSYlr6E/grcLSJyIuqrYVGTh7PlgxGXEQZ/co6odzbaP4ua6AzZLscrJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRG7oR/PusUIn4duJaU8xxTUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU063/chNBug61HoRKhvx1/zJDSYIGJL/p1Y6fRccoHSWZdQspdUipMCZ6+YYQSFeoMJelXr4f/qFUOoxWwBhSiCv3zxTJTmn/6wbc33/g9HQ3a3gEtGc8FvnTOrNXyMacfSf24w7PTzT7ecv1WwTb96JTUch8/u/GMRq97fM3KxkU1DQzJlFuRpZb+PzON1+QNr3Sb4PR6VeK0kGMnpARxrSKuxscokIXGmoUVylXd+Ch/3Y06KsG2RlRhbt64DJtfqTuaN41uT888TG9luiY3x74YtJO6ciUHyokryhDRZfCab4SF/A/vWfqfLDtkinxpZryxihe2/EWuyODwS9S53UpXoydKjtXBsG0G2RLU6siCUPR9/0Gh1C6A1wDS9uFEIV00mrHBJ5E9xb4wk4Ifvl7fES/zgkn2i7WWdkoi9+O16Orneq3rqoGAO4JwkA3zMaQjltahDeglPQUCRXWX9Oai2LDl4Eb3Wq9FjucsnancqJ3aJdoUpqq+AwJN14Ys8Re/DzO/3NQAmXkLMUtJeByag4XrJV3COv/4DfC4g1SjlDdk2erKMaHmApXINnTDkbHhcqhh60NE1gY/0dRS64hXB7wBOv7/RFL9udPCAhMkMQG43f7rCNBn2YMfXWKPDLWZMKTXsVKQ/e0jOfODaJUbuTrnMPgl///ujWMlmVADZ6mpxoAaaH+9Hvt8IkWZZWDgjcsGEWcPpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWHXfpcYWEQfYMZziILs9viDxXHYSmHqQmzFmFsBLwg+5sKfOR8SkFv7ri0sJ07qvdj0dh2yZzCpG32nrFdHl1gn8FXSR+iKo5qApijEyb0LRkjuZDPdNW7vJNFAw9MMiPnKRBF9nuV1eZLZ+yQ1G8T4DjWGlpJvoBhuQWakM4IO2MywjZ1kKCDLoclrjND5sxoPq090i0HN50zjP97Idkj1QiRaNnMGSngutn81GWCdeWyQOWkKGlcala1ynIpj/r5VrLh1lRVUtLaYuAWHkeYkXMqtGRzkzHRr6qT78gN1kYofM=

There's a fair amount of linear algebra here:
https://github.com/CoqEAL/CoqEAL

On Wed, Apr 28, 2021 at 6:49 PM Mohit Tekriwal <tmohit AT umich.edu> wrote:
>
> 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