The Coq mailing list

[Xuanrui Qi <xuanrui AT nagoya-u.jp>]

Hi Hugo (& list),

I recall the talk on rewrite rules at the Coq Workshop last year. Once
rewrite rules are finally implemented in Coq, I suppose one can have
computable quotients, excluded middle (i.e. continuations) and choice
(no idea what the computational equivalent is) in Coq. Would you
envision this to be an ideal setting to do classical mathematics?

On the other hand,
> that if R->S is a ring homomorphism then any S-module is naturally an
> R-module
sounds remotely like transport to me. Would a cubical Coq (of course,
with rewrite rules) support this type of "free" reasoning?

These are also Coq features that I really want; while I consider myself
a constructivist and I believe that constructive arguments are morally
correct, I do acknowledge that sometimes classical reasoning principles
can make things (e.g., textbook real analysis) a bit easier :-)

-Xuanrui

On Sat, 2020-01-11 at 05:22 +0100, Hugo Herbelin wrote:
> Hi,
> 
> I'm afraid I have here (as one of the moderator of the list) to
> remind
> some healthy basic « rules of conduct ». The Irish words I just read
> go beyond what is welcomed on the list, whatever one may think of
> Conor's fragments of words.
> 
> I find otherwise quite interesting matter for thinking in the rest of
> the discussion.
> 
> On the constructive/classical debate, I tend to think that it is
> indeed a rather ideological issue. I would not be surprised that by
> about say 5 years from now on, we are able to design a type theory
> with fully-computational excluded-middle and fully-computational
> extensional axiom of choice. Presumably, this "classical" type theory
> will build on a cubical equality, which, I agree here with Thorsten,
> is the nicest way I know to provide computational quotients.
> Moreover,
> on the practical side, it would be easy in Coq to provide as soon as
> now a file axiomatizing quotients, as Arthur proposed, the same way
> as
> classical reasoning is already supported axiomatically.
> 
> While I'm at technical questions. I was pretty interested by Kevin's
> question about working in a system "which will instantly know that a
> totally ordered field is an additive group or that if R->S is a ring
> homomorphism then any S-module is naturally an R-module". I believe
> that there is more to say about this important point.
> 
> And while I'm at writing, let me thanks, like Théo already did, Bas
> for initiating this discussion and everyone to contribute, and to
> notably thank Kevin for sharing his thoughts in a way worth its
> talent, repairing the tone adopted in some decried talks. In
> particular, I appreciated his invitation to come and chat at
> https://leanprover.zulipchat.com/. I've known the Types community for
> now 30 years, a community who developed Agda, Coq, Isabelle, Idris,
> Matita, Twelf, Alf, Lego, Epigram, ... a community who welcomed
> NuPrl,
> Mizar, PX, the QED manifesto ... a community who will also now invite
> Leo de Moura at its next conference in March in Torino. I'd be happy
> to see this collaborative spirit being prolonged. There is indeed so
> much to do in the building of proof assistants and interactive
> theorem
> provers, towards better foundations, towards more expressive and more
> intuitive proof languages, more robust and more expressive tactic
> programming languages and automation, more cooperative ecosystems of
> libraries (and, probably, we should find here better ways to let
> users
> and developers collaborate altogether). I'd like also that we are
> able
> to address the needs of mathematicians as they are, so that proof
> assistants eventually deserve being also qualified as mathematical
> assistants.
> 
> Hugo
> 
> On Sat, Jan 11, 2020 at 02:26:31AM +0100, Tadeusz Litak wrote:
> > On 11.01.20 01:38, Conor McBride wrote:
> > 
> >     Ah, poly.
> > 
> > 
> > Póg mo thóin.
> > 
> > Now for this claim:
> > 
> >     "Dear mathematicians: your life will be the same as it is now,
> > except that
> >     faulty proofs will be less common. The only price is, you need
> > to revisit
> >     your notions of LEM and AC." I dunno man, hard sell.
> > 
> > This indeed amounts to underselling constructive mathematics.
> > 
> > Look for example at "Models for smooth infinitesimal analysis" by
> > Moerdijk and
> > Reyes.  As another selling point, consider 
> > 
> > http://math.andrej.com/2006/03/27/sometimes-all-functions-are-continuous/
> > 
> > https://arxiv.org/abs/1502.03621
> > 
> > Going around and telling people that  they shouldn't do this or
> > that... and
> > they might be able to prove some of results they believed to have
> > been proved
> > anyway if they try hard enough... is indeed hardly a winning
> > proposition. But,
> > as Albert Visser likes to put it, more is possible in the
> > constructive realm
> > than is dreamt of in classical philosophy.
> > 
> > Regards,
> > 
> > t. [2/3]
> > 
> > 
> > 
> > 
> >         On 10 Jan 2020, at 20:30, Tadeusz Litak <
> > tadeusz.litak AT gmail.com>
> >         wrote:
> > 
> > 
> >         On 10.01.20 20:41, Timothy Carstens [or Adam Chlipala]
> > wrote:
> > 
> >             The reason is that the author and many other
> > researchers today feel
> >             that proofs on paper have outlived their usefulness.
> > 
> >         While I am fully supportive of proof assistants conquering
> > both math
> >         and CS worlds, the present state of affairs does not seem
> > to justify
> >         such a bold statement. I presume it was intended to be sell
> > talk and
> >         supposed to be taken with a grain of salt, but even then it
> > can be
> >         dangerously misleading. 
> > 
> >         It might be applicable to a not-so-novel CS conference
> > contribution,
> >         where the underlying math is often not so interesting in
> > its own right,
> >         the framework has a somewhat ad-hoc flavour or is oriented
> > towards a
> >         rather specific application, proofs may largely consist of
> > crunching
> >         relatively trivial subcases etc. And crucially, few people
> > are likely
> >         to be willing to digest these proofs in ten or twenty
> > years' time.
> > 
> >         Otherwise, the code will bitrot, for example. From what I'm
> > hearing,
> >         Lean might be particularly bad when it comes to moving fast
> > and
> >         breaking down things, but this problem affects Coq too.
> > Libraries get
> >         obsolete. Plugins and tactics evolve. There is not so much
> > effort in
> >         making various community developments play nicely with each
> > other, not
> >         even comparable to Isabelle's Archive of Formal Proofs.
> > 
> >         And this is just within *one* ecosystem, not to mention
> > combining
> >         developments in different proof assistants. How many people
> > today can
> >         code in and work with, say, Coq, Agda, Isabelle, Mizar,
> > Lean, Abella,
> >         Beluga, Dedukti, Twelf, Matita,  Nuprl/RedPRL, and Idris at
> > the same
> >         time?!
> > 
> >         If you cannot even re-run legacy code in ten or twenty
> > years' time, how
> >         about reproducibility of scientific results? And more
> > importantly, how
> >         about their reusability? What kind of insights researchers
> > who come
> >         after you are supposed to get? How can they check if your
> > proof applies
> >         in a modified set-up?
> > 
> >         These are increasingly serious problems that, at least in
> > my view, are
> >         not sufficiently often discussed or taken seriously by
> > authors and
> >         referees alike.
> > 
> >         I had other comments on this discussion, but they're best
> > left to a
> >         separate email, this one is already growing too big.
> > 
> > 
> > 
> >