The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Thanks for the summary.

Do I understand correctly that the formulation of lean's choice
implies excluded middle (by Diaconescu) ?

About ad-hoc polymorphism: it has been done in coq in two ways:
canonical structures (Gonthier, Ziliani, Nanevski, Dreyer, How to make
ad hoc proof automation less ad hoc,
https://people.mpi-sws.org/~beta/lessadhoc/)
type classes (Bas Spitters and Eelis van der Weegen, Type Classes for
Mathematics in Type Theory,
http://dx.doi.org/10.1017/S0960129511000119)

On Sat, Jan 4, 2020 at 6:43 AM Ramkumar Ramachandra 
<artagnon AT gmail.com>
 wrote:
>
> Lean has much lower startup-cost for pure mathematicians, since the 
> built-in features and mathlib are great for doing undergraduate-level group 
> theory & topology, masters-level commutative algebra & category theory, but 
> I think it plateaus quickly thereafter; future releases of Lean will 
> probably fix this.
>
> Lean seems to have taken a top-down approach, by focusing on writing real 
> proofs as quickly as possible, without compromising soundness 
> [https://github.com/digama0/lean-type-theory/releases/tag/v1.0]. There are 
> three axioms in Lean: propositional extensionality, quotient soundness, and 
> choice; however, these don’t block computation, since computation is done 
> by a VM. However, they break good type theoretic properties like strong 
> normalization, subject reduction, and canonicity — this was a conscious 
> design choice, and they decided that these properties weren’t as important 
> to working mathematicians.
>
> Coq, on the other hand, has always been very particular about sound type 
> theoretic foundations. The recent “Coq Coq Correct!” paper 
> [https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf]
>  proves various metatheoretic properties of the Coq engine.
>
> Lean supports both constructive and classical reasoning, but I’m hoping 
> HoTT will be integrated into mainline Coq and solve most of the 
> setoid-related issues (not that I understand much about it).
>
> One would think that Lean is an engineering feat, since it’s written in C++ 
> (and lean4 is written mostly in C): math-comp is 90k loc, while mathlib is 
> 150k loc; and it takes over thirty minutes to build mathlib! Coq is much 
> faster.
>
> Quotients are indeed a great feature to have, and makes formalizing 
> commutative algebra painless; an example 
> [https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean]
>  of using quotients in Lean. However, quotients are tricky to implement 
> without breaking certain metatheoretic properties that Coq’ers cherish, 
> which is why it hasn’t been implemented yet.
>
> Lean’s inheritance 
> [https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#inheritance]
>  is another good feature; it disallows diamond-inheritance, and seems like 
> a bit of a hack, but Coq should definitely get some form of a 
> well-thought-out ad-hoc polymorphism.
>
> Category theory in Lean has not been developed 
> [https://github.com/leanprover-community/mathlib/blob/master/docs/theories/category_theory.md]
>  with higher categories in mind; I’m not sure how one would define 
> ∞-categories, since universes are explicit, and since there are no 
> coinductive types: Coq’s impredicativity seems to be a better design choice.
>
> Footnote. Metamath Zero [https://github.com/digama0/mm0] might be of 
> interest to the Coq community for high-performance checking.
>
> Ram