coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq vs lean for classical analysis

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>, Kevin Buzzard <kevin.m.buzzard AT gmail.com>
Subject: [Coq-Club] Coq vs lean for classical analysis
Date: Thu, 9 Jan 2020 07:02:21 +0100
Authentication-results: mail3-smtp-sop.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-yb1-f175.google.com
Ironport-phdr: 9a23:EQAiKxz9RPnf7GzXCy+O+j09IxM/srCxBDY+r6Qd2+0eIJqq85mqBkHD//Il1AaPAdyAragZ2qGG6ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe61+IRWyoAnetcQan5ZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLzliwJKyA2/33WisxojaJUvhShpwBkw4XJZI2ZLedycr/Bcd8fQ2dKQ8RfWDFbAo6kYIQBD+QPM+VFoYfju1QDtge+CRW2Ce/z1jNEmn370Ksn2OohCwHG2wkgEsoTvXvOt9X+KbocUfi0zKnU0TXMcelW2Szg44XPaR8tu+uDUah+cMbL0kkvDwLFjkmMqYP7JTOVzf8As2ee7+V6VOKvj3QrpB12ojiq38ohjJTCiIwSylDB7yp5wYA1KMW5SE59e96kEYFfuzuUN4tsWs8iTGBouDo6yr0bopG3ZjQFyJMixxPZdveJcJCI7wr9WOqNJTp0nnFodbKlixqs7EStzvfwWtS23VtKqCdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3T7/tLIUEwlabCK58u2aM8moMdsUjeHCL7mF/6jKCRdkUj9eio7/robq/6qZ+bMo94kgD+MqIwlcyjGek0LBQCUmyB9em/1LDv51P1TKhOg/Esj6XUspDXKdwepqGjAg9V1ogj6wy4DzejyNkXhmMLI0hfdBOJlYTpIEnOIPHkDfejnVusiixryuvJPr3kGJrNL3zDnK39crZ67k5Q0BAzwsxH55JIFrEBJ+r+VVP2tNzBFxM2Lwi0w/v8B9hmzYMfWWePAreDP6/IsF+I4PgvI+iWa4MPtjb9Matt2/m7pngg0XQZYKPhiZAQcTWzGulsC0Sfe3vlxNkbRyNCnQcgTeqiokCQQzdJaz7mXK8i5zd9DcSsEJXRT5qhqLOE1Sa/WJZRYzYVJEqLFCLCfp7MYO8NdD6fONQpxjZCXP6+DZQ51A2yuRXh47ViJ+vQvCYfsMSwh5BO++TPmERqpnRPBMOH3jTIFjksxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUKtfxMWwY+c5Xbyr4jUoygakf6Zt6MDW2ebJC+GzhoF4A+xtYPZwB2HNDw1kmejRrvOKcckvmwPLJx8q/Y2CKvdcN0ynKDxaN4yld/HZYJOmqhiapysQPUAtyRng==

Dear Kevin,

Thank you for your clarifications.
Let me try to see if I understand, you seem to be saying that lean
would have little advantages over coq for discrete mathematics such as
used in the Feit-Thompson theorem. In particular, the automation of
lean is not much stronger than that of Coq.

However, for classical real analysis you seem to be saying that native
quotients and choice have a big advantage. Here it is possible to make
a good comparison between the coq stdlib reals, coquelicot and
math-comp analysis on the one side and lean's math-lib on the other
side.
Could you explain how native choice/PEM is much preferable over a
choice *axiom* as is used in e.g. math-comp analysis.
https://github.com/math-comp/analysis
http://coquelicot.saclay.inria.fr/

Obvious differences with math-comp analysis are:
IIUC lean has dropped canonical structures and has a type class system
that is slightly different from Coq's. Moreover, lean's proof language
is more verbose than Coq's Ltac and in particular SSR.

Best wishes,

Bas

[Coq-Club] Coq vs lean for classical analysis, Bas Spitters, 01/09/2020