The Coq mailing list

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

I'm mostly interesting in the technical difference between lean and
coq, so did not want to make this into a constructive vs classical
debat.

But yes, large parts of commutative algebra can be developed
constructively and this is beneficial for computer algebra, and hence
formalization.
See e.g. this 1000pp book
Commutative algebra: Constructive methods. Finite projective modules
Henri Lombardi, Claude Quitté
https://arxiv.org/abs/1605.04832
One observation comes from topos theory, saying that one can avoid the
axiom of choice and classical logic by working with locales instead of
topological spaces.
Interestingly, the book above presents this in such a way that it
looks entirely natural.

A lot of such computational/constructive algebra has been developed in
the coqeal library:
https://github.com/CoqEAL/CoqEAL


Ramkumar > however, these don’t block computation, since computation
is done by a VM.
What has been proved about the VM? I expect it will block sometimes.

On Tue, Jan 7, 2020 at 6:23 AM Xuanrui Qi 
<xuanrui AT nagoya-u.jp>
 wrote:
>
> On a side note, I thought it was the case that in commutative algebra
> there is at least some awareness of constructive methods. I am by no
> means a working algebraist, though, so I might be mistaken.
>
> -Xuanrui
>
> On Mon, 2020-01-06 at 22:36 +0100, Bas Spitters wrote:
> > Let me just quote John Baez today:
> > "I think of topos theory as being fashionable again, now that famous
> > mathematicians like Connes and Lafforgue who we don't think of as
> > category theorists are trying to use topos theory to tackle big
> > problems in number theory etc."
> > https://twitter.com/johncarlosbaez/status/1214225792307060736
> >
> > Of course, synthetic mathematics is just one application of
> > constructive logic, the computational aspect is another one.
> >
> > On Mon, Jan 6, 2020 at 9:58 PM Kevin Buzzard <
> > kevin.m.buzzard AT gmail.com>
> >  wrote:
> > > Yes, Diaconescu is formalised in the Lean standard library and this
> > > is how excluded middle is proved in Lean:
> > > https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#the-law-of-the-excluded-middle
> > >
> > > While I'm here let me respond to something Thorsten said:
> > >
> > > > Now let me get to the point that most Mathematicians are not
> > > > aware of constructive Mathematics. This may well be true but does
> > > > this mean that they are right and that constructive Mathematics
> > > > is irrelevant for Mathematics? This seems rather a sociologically
> > > > issue than anything else. And fashions can change faster than you
> > > > think especially once a new generation of Mathematicians take
> > > > over who are not only influenced by the older Mathematicians but
> > > > who are often also excellent programmers acquiring new
> > > > intuitions. To not educate them as well in constructive
> > > > Mathematics reflecting these intuitions is a criminal omission.
> > >
> > > It is certainly true, and I would also argue that the law of the
> > > excluded middle is completely embedded in "Fields Medal
> > > mathematics". The bright young mathematicians look up to the Fields
> > > Medallists, and are taught on day one that Prop = bool and hence
> > > that the law of the excluded middle is an axiom. This will be an
> > > extremely hard cycle to break. I agree that young people are more
> > > and more coming into mathematics departments with a knowledge of
> > > programming and this is what I want to tap into, but rejecting LEM
> > > would not be a suggestion which would be taken seriously by anybody
> > > in our department. In fact I do not know of a mathematics
> > > department anywhere in the world where undergraduates are not told
> > > that LEM is true right from the start, and most lecturers. It would
> > > be interesting to find examples of International Mathematical
> > > Olympiad questions which would be unsolvable without LEM.
> > >
> > > Kevin
> > >
> > > On Mon, 6 Jan 2020 at 09:40, Bas Spitters 
> > > <b.a.w.spitters AT gmail.com
> > > > wrote:
> > > > 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
>