The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Note, by the way, that Coq has a Grobner basis tactic (two, actually).  There is nsatz (named after nullstellensatz) and psatz (named after positivstellensatz).  See https://coq.inria.fr/refman/addendum/micromega.html and https://coq.inria.fr/refman/addendum/nsatz.html.

On Thu, Jan 2, 2020, 18:01 Kevin Buzzard <kevin.m.buzzard AT gmail.com> wrote:

On Thu, 2 Jan 2020 at 21:55, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 1/2/20 2:41 PM, Timothy Carstens wrote:
> * Tactic mode. Arguably this should be a rich programming environment
> with useful abstractions. Right now you can get that if you're willing
> to write a Coq plugin, but that's kinda heavy-handed, and it's
> certainly a highly-coupled (hard to maintain) way to go. Lean has a
> goal of offering a richer environment for tactics. IMHO everyone will
> eventually need to go in this direction.

I'm not sure I understand this point.  Ltac works well for most kinds of
tactic programming.  At least, I don't see how it could be held not to
meet the binary requirement of "a rich programming environment with
useful abstractions."

I am not a computer scientist and I don't have much experience with Coq,

but with Lean you only need to learn one language not two, and as well as

writing tactics people have been writing things like linters, new commands

which tell you which namespace you're in, which namespaces are open,

what variables you have and so on, stuff which makes the end users life

a bit easier.

How common is it for people outside the core Lean development team to
write their own nontrivial tactics?  In other words, is there evidence
that Lean's tactic style is attracting more satisfied users?

People come along and write tactics as summer projects. When I started

using Lean (and teaching Lean) my students (who are all used to the informal

point of view with N in Z in Q in R in C) all had trouble with goals of the form

a = b when they already had a proof of what looked to them like a = b, whereas

one of these a = b statements was actually int_to_rat(a)=int_to_rat(b) or whatever. I wrote

a suite of examples corresponding to problems which mathematians had been having,

then an MSc student who had some CS background but was not part of the core development

team came along and wrote a tactic which solved them all as part of a summer project.

"Regular users" such as me knock up simple tactics which mathematicians want,

but these would not be classed as nontrivial.

However I strongly suspect that Coq is ahead of Lean on the tactic front in general.

What I am finding as a mathematician who wants to reason about complex objects

is that I have pretty much all the tactics I need now, except that occasionally a Groebner

Basis tactic would be useful so I can quickly solve questions of the form "prove this element

of this ring is in this ideal" automatically (although of course I can solve these using

computer algebra packages and then just paste in the solution, it's just a bore).

In general, I think it's a mistake to compare proof assistants using
criteria associated with random varieties of open-source projects, since
typically open-source projects are much less involved in major
design-space innovations.  IMO, worrying about quality of library
ecosystems should mostly be avoided.

When mathematicians come looking at these systems, one of the first questions

they seem to ask is "how much mathematics is in there already?". They want

to see a coherent answer with words they understand, and the more undergraduate

level mathematics there is in one accessible place, the better. I did a recent sweep

with Lean:

https://github.com/leanprover-community/mathlib/blob/doc_cleanup/docs/mathlib-overview.md

and I would be interested to see the corresponding picture with Coq.

Kevin (still not really knowing if this post will go through, or whether his original long post did)