Ignat Insarov (Jun 21 2021 at 17:09): Ignat Insarov (Jun 21 2021 at 17:09):I was reading [this example] and I noticed that I can do like:
Goal false → False.
intros. contradiction. Qed.
This is surprising because false: bool: Set and therefore should not be treated as a property. The context tells me false is treated in a special way here. Set Printing All. shows this:
Goal false -> False.
intros.
(*
H : Bool.Is_true false
============================
False
*)
Apparently this is all contingent on this command being previously issued:
Coercion Bool.Is_true : bool >-> Sortclass.
What is going on?
[this example]: http://github.com/mattam82/Coq-Equations/raw/master/examples/polynomials.v
Emilio Jesús Gallego Arias (Jun 21 2021 at 17:12):Indeed, false here is just shortened display for false = true
Emilio Jesús Gallego Arias (Jun 21 2021 at 17:13):This is done so you can use boolean properties as propositions, for example this way you can write x \in s instead of (x \in s) = true
Gaëtan Gilbert (Jun 21 2021 at 17:13):https://coq.github.io/doc/master/refman/addendum/implicit-coercions.html#coq:cmd.Coercion
Ignat Insarov (Jun 21 2021 at 19:37):Why would anyone want this?
Ignat Insarov (Jun 21 2021 at 19:38):Yea, I kinda see how it works… so, any 𝔹 gets a = true added behind the curtain.
Ignat Insarov (Jun 21 2021 at 19:43):Imma hand the mic to the official anti-pattern guide.
Overuse of syntactic sugar via Notation, Coercion, Class/Instance, Implicit Insertion can lead to an incomprehensible proof state.
Ignat Insarov (Jun 21 2021 at 19:43):Indeed it does.
Christian Doczkal (Jun 21 2021 at 19:45):Ignat Insarov said:
Why would anyone want this?
Well, there are many reasons. First it is very natural to consider boolean expressions as proposition. More pragmatically, boolean expressions allow simplification, case analysis, and rewriting (without setoid infrastructure). For this reason they are pervasively used in the mathematical components library. IIRC, the is_true coercion originally comes from there.
Christian Doczkal (Jun 21 2021 at 19:51):Indeed, decidable predicates such as _ <= _ are defined as boolean predicates in mathcomp, and there are many equalities between such boolean statements in the library, e.g.
Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n).
So this is a central paradigm of one of the most comprehensive libraries out there. So I dare say it does not qualify as "overuse".
Christian Doczkal (Jun 21 2021 at 19:54):Also, there is no such thing as an "official anti-pattern guide". What you are referring to is a Wiki page without any official status. I disagree with half of this guide, while also disagreeing with some of the choices in mathcomp. :grinning:
Ignat Insarov (Jun 21 2021 at 19:56):I do not mean to sound hostile, but this all makes me sad.
Ignat Insarov (Jun 21 2021 at 19:57):I have been asking but a few days ago and the page about anti-patterns is the closest to a style guide there is for Coq.
Ignat Insarov (Jun 21 2021 at 20:00):Unfortunately I also find that mathcomp is the closest I have ever seen to intentionally obfuscated code in real life.
Christian Doczkal (Jun 21 2021 at 20:07):Well, you should be very careful. While most people involved in the development of mathcomp with readily admit that the style propagated by mathcomp is not exactly beginner-friendly, this is anything but an "intentional obfuscation". The design of mathcomp is the result of running, time and again, into the limitations of the Coq system. This involves both the management of complex hierarchies of mathematical structures and the long-term maintainability of the code. Ultimately, the mathcomp libraries are enabling experts to get things done, and they are very successful at that.
Ignat Insarov (Jun 21 2021 at 20:09):Not to hurt their feelings. They did a great job with their proofs. But they did it for themselves, not for the wider community. _(Which Coq does not have anyway, so not much loss here.)_ And it is of course my problem that I dislike their style.
Ignat Insarov (Jun 21 2021 at 20:11):Unfortunately I only get to write proofs in my own time, so I simply cannot afford to spend hours deciphering their short hand.
Christian Doczkal (Jun 21 2021 at 20:11):I don't know what your definition is of a "wider community", but mathcomp is very much a project that is done for others. This is why it always supports 2-3 versions of coq, and documents every little compatibility-breaking change.
Ignat Insarov (Jun 21 2021 at 20:13):I can only wish them great success!
Christian Doczkal (Jun 21 2021 at 20:16):The problem is, that the "Standard Library" of Coq does not have any coherent design. Yes, things are in a way "simpler", but the various parts of the library are a lot less integrated. So once you try to do more complex stuff, there is a high likelihood of spending more time reinventing the wheel than it would take to learn mathcomp. Its a question of the size of your project your purpose. If the goal is to learn type theory and formal proof, a more bare-bones approach may be preferable.
Ignat Insarov (Jun 21 2021 at 20:18):No question to that. But did they have to put in so much notation and short hand? Is it necessary?
Christian Doczkal (Jun 21 2021 at 20:24):Yes, this is absolutely crucial to not get lost in cluttered statements that span many lines and/or state lemmas in a suitably generic way and still apply them to all the concrete instances they should apply to. Things like re-indexing big operators really do not depend what the operator is, or splitting big operator into two only requires that the operation is commutative and has an identity. Similarly, you don't want to see what the index ranges over, if can be inferred from the context. So you want to write \max_i F i rather than something much more verbose.
Ignat Insarov (Jun 21 2021 at 20:25):Generality is one thing, short hand is another.
Ignat Insarov (Jun 21 2021 at 20:26):Surely you can have either one without the other.
Ignat Insarov (Jun 21 2021 at 20:26):Maybe I am deeply misguided. I have not been proving monumental theorems.
Christian Doczkal (Jun 21 2021 at 20:28):That's actually the point I was trying to get to: try not to be judgmental about something without understanding the rationales that led to a particular design.
Christian Doczkal (Jun 21 2021 at 20:29):Formalizing things in a rich type theory, like the one of Coq, is not straightforward. Some designs look nice at first and then fail miserably once one tries to scale it up. I've had some moments like this ...
Ignat Insarov (Jun 21 2021 at 20:31):Of course, Coq is so much different from mere _programming_ languages. Much more complex things get written casually.
Ignat Insarov (Jun 21 2021 at 20:32):Really, computer programming without formal proof is but a triviality. And the average intelligence of a _programmer_ is much lower than that of a mathematician working on formal proof.
Christian Doczkal (Jun 21 2021 at 20:32):Yes, it's actually a very limited programming language. Only terminating programs, and no side effects. But this is necessary in order to use it as a logic.
Ignat Insarov (Jun 21 2021 at 20:33):They only give nice names to stuff because their programs are so trivial and they need to create an appearance of hard work…
Ignat Insarov (Jun 21 2021 at 20:33):I mean, really.
Ignat Insarov (Jun 21 2021 at 20:33):Maybe it is like that. Then I should pack my stuff and go.
Christian Doczkal (Jun 21 2021 at 20:34):I am bad enough at programming that I wouldn't call it trivial. I'm more one of those people doing math in coq (with mathcomp). Writing clean, correct, and maintainable code is a challenge of its own. Independent from verifying its correctness.
Ignat Insarov (Jun 21 2021 at 20:37):I think I went too far, sorry if I offended you.
Ignat Insarov (Jun 21 2021 at 20:38):I do not mean to hurt anyone's feelings.
Christian Doczkal (Jun 21 2021 at 20:38):Then the best advice I can give is to be careful with bold statements, in particular around scientist. :grinning_face_with_smiling_eyes:
Ignat Insarov (Jun 21 2021 at 20:38):Not yours and not the developers of mathcomp's.
Ignat Insarov (Jun 21 2021 at 20:48):Which of my statements I should be careful with though?
Gaëtan Gilbert (Jun 21 2021 at 20:50):Ignat Insarov said:
Really, computer programming without formal proof is but a triviality. And the average intelligence of a _programmer_ is much lower than that of a mathematician working on formal proof.
Those are very strong claims with 0 evidence
Ignat Insarov (Jun 21 2021 at 20:50):Yes, this is me being sarcastic.
Gaëtan Gilbert (Jun 21 2021 at 20:51):sarcasm in text can be dangerous
Ignat Insarov (Jun 21 2021 at 20:51):Me being the average programmer.
Ignat Insarov (Jun 21 2021 at 20:53):My real statement would be that notation and short hand are entirely optional for the design and architecture of any library, mathcomp not being an exception.
Ignat Insarov (Jun 21 2021 at 20:53):In other words, Coq does not force one to use notation and short hand.
Ignat Insarov (Jun 21 2021 at 20:54):I hope it does not!
Pierre-Marie Pédrot (Jun 21 2021 at 20:55):No, you can perfectly write all of your proofs directly in CIC.
Ignat Insarov (Jun 21 2021 at 20:56):Or in nice, approachable language. Right?
Pierre-Marie Pédrot (Jun 21 2021 at 20:57):CIC is much nicer than, say, x86 and its crazy memory model.
Ignat Insarov (Jun 21 2021 at 20:57):Not sure if you are making fun of me, Pierre-Marie.
Ignat Insarov (Jun 21 2021 at 20:58):Do you agree or disagree with my statement that Coq can be written in beautiful and approachable style?
Pierre-Marie Pédrot (Jun 21 2021 at 20:58):Define beautiful.
Ignat Insarov (Jun 21 2021 at 20:58):Commensurate with the human cognitive ability.
Ignat Insarov (Jun 21 2021 at 20:59):Approachable — arranged for possibly easier appreciation.
Ignat Insarov (Jun 21 2021 at 21:00):I am not sure if you folks take offense. I am really bad at reading between the lines. Should I leave?
Pierre-Marie Pédrot (Jun 21 2021 at 21:00):I am personally not taking offense, but I'd recommend trying to write a serious proof to understand why mathcomp is the way it is before potentially pissing off mathcomp devs / users (I am not one of those)
Pierre-Marie Pédrot (Jun 21 2021 at 21:01):And I stand by the fact than CIC is simpler than x86 for all reasonable metrics.
Ignat Insarov (Jun 21 2021 at 21:02):I do not agree nor disagree with your statement about CIC and x86 assembly.
Ignat Insarov (Jun 21 2021 at 21:02):But please tell me, can Coq be written in beautiful and approachable style, as defined above?
Pierre-Marie Pédrot (Jun 21 2021 at 21:03):I believe the question is ill-posed, beauty and approachability is in the eye of the beholder.
Ignat Insarov (Jun 21 2021 at 21:03):Of course it is. Beholder is defined well enough though.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:04):math-comp is an amazing tool, and so far it has not been surpassed IMO, however it is optimized for one particular thing: ultra expert users writing a particular set of proofs in a particular style [for example, no automation]
Ignat Insarov (Jun 21 2021 at 21:04):Thanks Emilio, I was hoping someone would say this.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:04):in fact, so far all of the problems you have been posting, have been solved already in math-comp [such as subtypes I mean] in an often superior way, due to decades of careful design and validation
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:05):but indeed there is no general Coq style / patterns / anti-patterns
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:05):the same way there is not for C or C++
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:05):for example, in math-comp using auto is an anti-pattern
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:06):in other devs it is the base, so YMMV; I am a math-comp user just because it solves my problems very well, but I admit at first was like for Spaniard to learn Russian or Japanase, hard
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:06):fortunately I can read code, so I just went and read the code, then I was amazed at the stuff they wrote and I understood how far I was of even grasping what was going on
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:07):so indeed math-comp is kind a of particular case: you will find many people that don't even understand its basics talking bad about it
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:07):but all the advanced users have only praise
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:07):interesting isn't it?
Ignat Insarov (Jun 21 2021 at 21:07):I sure hope the problems I yet have with Coq are already solved! I stumbled upon them in my first steps. I hope to get to hard problems eventually.
Pierre-Marie Pédrot (Jun 21 2021 at 21:08):@Emilio Jesús Gallego Arias Stockholm syndrom fits the symptoms though.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:08):Indeed math-comp significantly differs from a programming language in that it makes extensive use of unifccation in the day-to-day programming
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:08):so a totally new worlds opens up once you have, as a programmer, that power at your hands.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:08):Pierre-Marie Pédrot said:
Emilio Jesús Gallego Arias Stockholm syndrom fits the symptoms though.
wrong
Ignat Insarov (Jun 21 2021 at 21:08):So please tell me, would mathcomp become worse were it rewritten with 90% notation removed and plain English naming style?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):trivilally wrong
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):Ignat Insarov said:
So please tell me, would
mathcompbecome worse were it rewritten with 90% notation removed and plain English naming style?
would become unusable
Ignat Insarov (Jun 21 2021 at 21:09):How so?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):and moreover, writing proofs on it would become hard
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):you can try and see, maybe you are right, after all proof engineering is an experimental field
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):but if you want to pilot an airplane
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:09):or any other advanced machine
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:10):prepare to spend many hours studying how the thing works
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:10):there is no free lunch, nor silver bullet
Ignat Insarov (Jun 21 2021 at 21:10):Not sure why you are saying this.
Ignat Insarov (Jun 21 2021 at 21:10):I am prepared to spend the next 50 years studying formal proof.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:11):math-comp is way more advanced than what most people unfamiliar with it is, just because it has a lot of unique stuff, that people is not aware even it exists, this is indeed an interesting phenomenon in the psychological sciences but I'd let PMP find the concrete naming for it :)
Ignat Insarov (Jun 21 2021 at 21:11):You folks make fun of me, do you not.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:12):Ignat Insarov said:
Not sure why you are saying this.
I was just saying that something similar to what Christina said, before judging such a complex piece of software such as math-comp, be sure to know it well. In the same way a different alphabet may look strange at first, maybe once you have become familiar with it you actually do prefer it to the previous one
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:12):Ignat Insarov said:
You folks make fun of me, do you not.
Not at all, at least in my case
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:12):Why do you think I'm making fun?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:12):I am dead serious
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:12):this is a very interesting topic, I see people use Coq is such horrible ways everyday
Ignat Insarov (Jun 21 2021 at 21:13):I take it that you all know each other pretty well, and I am a newcomer whom you all disagree with.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:13):For math-comp I just say, don't jugdge a book by its cover
Ignat Insarov (Jun 21 2021 at 21:13):I actually really like the cover of their book!
Ignat Insarov (Jun 21 2021 at 21:13):I like the style of the book. Aside from code snippets.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:13):A lot of the problems you have been facing these days, are ruled out if you use math-comp, because it was designed not to have them in the first place
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:14):For example you need a "subtype"? Just write { x : nat | x < 10 }
Ignat Insarov (Jun 21 2021 at 21:14):All I want is to make the argument that architecture is independent of naming.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:14):Are you in math-comp, voila! You get automatically all the instances for that type, and proof irrelevance in the arg
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:14):Ignat Insarov said:
All I want is to make the argument that architecture is independent of naming.
What do you mean?
Ignat Insarov (Jun 21 2021 at 21:16):That you can change all the names in mathcomp in such a way that it suddenly becomes beautiful and approachable _(in the sense defined above if you require a definition)_ without losing any of its semantics.
Pierre-Marie Pédrot (Jun 21 2021 at 21:16):Naming schemes are very important for any programming languages though.
Pierre-Marie Pédrot (Jun 21 2021 at 21:17):Replacing all identifiers in an arbitrary program with randomly generating names is going to quickly disprove your thesis.
Ignat Insarov (Jun 21 2021 at 21:17):Of course Pierre-Marie. You have to rename in such a way that all associations remain in place.
Ignat Insarov (Jun 21 2021 at 21:17):You are putting a straw man in place of my actual argument.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:18):Ignat Insarov said:
That you can change all the names in
mathcompin such a way that it suddenly becomes beautiful and approachable _(in the sense defined above if you require a definition)_ without losing any of its semantics.
naming is actually pretty good in math-comp, but it is designed to be concise, as proof space is essential; lines are limited to 80 chars, and you wanna chain a lot of lemmas in rewrite in a single line so it is important
Pierre-Marie Pédrot (Jun 21 2021 at 21:18):No. Amongst all the stuff mathcomp got right, there is their naming scheme.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:18):I much prefer to write rewrite addnC addn0 than the equivalent
Pierre-Marie Pédrot (Jun 21 2021 at 21:18):Somebody in this thread already mentioned it.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:18):also the nmemonics are better
Ignat Insarov (Jun 21 2021 at 21:18):lines are limited to 80 chars
Are you living in the 80s?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:18):Ignat Insarov said:
lines are limited to 80 chars
Are you living in the 80s?
??
Ignat Insarov (Jun 21 2021 at 21:19):Even Linus Torvalds does not insist on 80 character limit anymore.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:19):Really you need to use a less aggressive approach here
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:19):If you want us to help you
Ignat Insarov (Jun 21 2021 at 21:19):I apologize if this sounds aggressive. What I mean is to say that screens got much better since the time 80 character terminal was a standard.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:19):When there is a huge gap in experience with a system, indeed it becomes very hard to communicate
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:20):The reason proofs are limited in math-comp is due to the same reason PDF papers have a width limit
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:20):You can watch any of the talks of George he explains it
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:20):Take 100 if you think 80 is small
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:21):but math-comp files are meant to be documents, and as such, like HTML ones or LaTeX ones
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:21):they have a limited width
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:21):and it makes a lot of sense
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:21):in many accounts
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:23):
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:23):
Ignat Insarov (Jun 21 2021 at 21:24):Surely a proof is not required to be this many characters wide to be correct.
Ignat Insarov (Jun 21 2021 at 21:25):Returning to renaming: nowhere I say to replace all names at random or that the naming scheme in mathcomp is not systematic enough. What I am saying is that it is plausible there to be a way to rename everything in a way that it becomes beautiful and approachable while staying reasonably close to the original system.
Ignat Insarov (Jun 21 2021 at 21:26):I mean, we gotta at least try?
Ignat Insarov (Jun 21 2021 at 21:26):Digitizing math books is the least of my concerns, truly… Are you saying that this is what Coq is for?
Ignat Insarov (Jun 21 2021 at 21:27):I do not mind if you digitize books to Coq of course, but this is sort of… not the primary purpose?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:27):That was the primary purpose of the math-comp project
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:27):basically to verify a few advanced group theory books
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:27):to provide a digital, checkable version of it
Ignat Insarov (Jun 21 2021 at 21:28):That fits in the same amount of pages?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:28):on the way they solved many other problems, such as implementing a state of the art hierachy of math-structures, etc...
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:28):Ignat Insarov said:
That fits in the same amount of pages?
I don't recall the formalization ratio , but for sure it is one of the best ever achieved in Coq
Ignat Insarov (Jun 21 2021 at 21:29):Was it a requirement that it fits in a certain amount of pages, or further that it preserves the layout of the original texts?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:29):It is a desire, not a requirment
Ignat Insarov (Jun 21 2021 at 21:29):Is there such a requirement for many Coq developments?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:29):that's my understanding
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:29):depend on who writes them, every person has their style, and every problem may require a different approac
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:30):for example I understand math-comp tried some automatization at the beginning
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:30):it didn't work
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:30):proofs would break all the time
Ignat Insarov (Jun 21 2021 at 21:30):Emilio, please understand. I looked at their papers where they explain how they tried different ways to put hierarchies of mathematical structures into Coq.
Ignat Insarov (Jun 21 2021 at 21:31):I understand that they made a strong effort to develop a great architecture.
Ignat Insarov (Jun 21 2021 at 21:31):I am saying repeatedly that I have no objections to their architecture.
Ignat Insarov (Jun 21 2021 at 21:31):All I am saying is that naming is not essential to correctness.
Ignat Insarov (Jun 21 2021 at 21:31):While being essential for beauty and approachability.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:32):Naming scheme is one of the best things math-comp has
Ignat Insarov (Jun 21 2021 at 21:32):Here of course Pierre-Marie enters with his question: who is the beholder.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:32):so what you propose to call addnC
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:32):?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:32):add_nat_commutative
Ignat Insarov (Jun 21 2021 at 21:32):Natural.addition_commutes would be my style.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:33):for once they managed to make Hungarian naming scheme be pleasant
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:34):Ignat Insarov said:
Natural.addition_commuteswould be my style.
This is a name I'd love to read
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:34):But if I had to write it, i would have not good feelings
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:34):that style is just too verbose I'm afraid
Ignat Insarov (Jun 21 2021 at 21:34):Naming scheme is one of the best things math-comp has
I have repeatedly said that I do not propose to abolish the system of naming from any library. I rather support following a strict naming scheme. Best if a machine can parse it. Therefore I suggest systematically renaming things, not arbitrarily.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:35):I can tell you already that your proposed naming scheme is unworkable in practice
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:35):of course that is my opinion, I'd love to be proved wrong
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:35):a different issue here is documentation
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:35):like you would like to associate a couple of tags to addnC such as nat and commutative
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):@Enrico Tassi @Cyril Cohen , myself and likely other people have been working on this
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):see the wiki page where they described a very interesting proposal
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):but addnC is just much superior
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):very easy to remember
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):need multiplication
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:36):mulnC
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):need the ring equivalent
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):mulrC
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):need the word equivlaent?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):subwC
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):etc..
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):I was able to type the 3 lemmas in less characters than one single lemma in your style
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:37):imagine the impact this has on productivity
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:38):but we have enough tooling you could try the renaming if you wish
Ignat Insarov (Jun 21 2021 at 21:39):Natural.addition_commutes would be my style.
This is a name I'd love to read
But if I had to write it, i would have not good feelings
Now we come to an interesting place. Let us talk about this for a minute if you please. Which is more important — to read with ease or to write with ease? And for whom?
You may look at any modern popular industrial library. You will see beautiful and approachable naming. Because those libraries are written for the many. If you write a library for your 10 collaborators, then surely you can all agree on a short hand. But if you write a library for people that maybe use 100 other libraries along with yours, you have to stick to naming conventions similar to the other 100 libraries. And the convention is readily available — it is plain English. Very well developed and widely understood.
And this is all I want to say and for people to hear from me.
Ignat Insarov (Jun 21 2021 at 21:40):You can also take the Holy Bible for an example. In the times of rare and expensive hand written books, it was written with short hand. But in our time you would not see short hand in the Bible. It is now written in plain and full English.
Ignat Insarov (Jun 21 2021 at 21:42):So, the question is whether you want to keep Coq to your 10 collaborators or to spread the word. If you wish to spread the word, you need beautiful and approachable words to spread in the first place.
Ignat Insarov (Jun 21 2021 at 21:43):Thanks for reading!
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:45):I guess spreading the word is more of a social activity, and marketing and being able to fund engineers to refine a product is way more important than a particular naming scheme which can be easily solved by having both a reading / writing mode.
Leaving such complex questions aside, as of today I care: a) that my lemma statement is easy to read b) that my proofs are quick and easy to write
Pierre-Yves Strub (Jun 21 2021 at 21:45):Ignat Insarov said:
lines are limited to 80 chars
Are you living in the 80s?
No, i have a human eye that is not able to jump from the end of a 200-character wide line to the beginning of the next line. But if you think that people are doing typography the wrong way, please, be my guest.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:45):that's the current state of the field
Ignat Insarov (Jun 21 2021 at 21:49):Pierre, is there any research showing that reading code on a modern screen is hard when it has lines of 120 characters' worth of beautiful and approachable names, as compared to 80 characters' worth of short hand? Please make me aware of it. By the way, I also have human eyes. Maybe we can meet in the middle of, say, 130? _(You go 50, I go 70.)_
Ignat Insarov (Jun 21 2021 at 21:51):Emilio, now we are talking. You have your preferences. Making me happy with beautiful and approachable names is not the first among them. This is of course understandable. Do you agree though that my argument makes sense?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:51):80 is a good default on laptops , my current, very recent thinkpad is 14''
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:52):and the line width of my emacs buffer is 168
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:52):given that I take half for the goal buffer
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:52):80 is actually perfect for it
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:52):I would go for more, but even 90 overflows my current setup
Ignat Insarov (Jun 21 2021 at 21:53):I refer you to Linus Torvalds with the question of line width. If he cannot persuade you, he can at least be an example that proves existence.
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:53):Do you agree though that my argument makes sense?
Not sure, in the sense that IMHO you should try to write more proofs and discover more styles, then see if you still agree with your proposal
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:53):Linus doesn't have half of the screen taken by a goal window
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:53):also C ...
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:54):You've been told twice tho the reason, are you didn't provide any argument to PY's comment
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:54):other than pointing to a comment a random individual unrelated to Coq made about his own toy
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:55):for writing a Kernel maybe I'd trust Tovarlds
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:55):and he was very vocal about the line widht
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:55):but for writing proofs I may trust GG more
Ignat Insarov (Jun 21 2021 at 21:55):Who is GG?
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:55):Georges Gonthier sorry
Emilio Jesús Gallego Arias (Jun 21 2021 at 21:56):So indeed you can use stuff such as the experimental Python API of SerAPI to do the renaming automatically, but I predict few of us will prefer it, IMHO writing a good reader and a good documentation system seems more promising
Ignat Insarov (Jun 21 2021 at 22:00):So, you have your preferences, I have mine, people out there have theirs. This is fine. What I am saying is that I feel bad using mathcomp because its excess of notation and short hand impedes my progress.
Ignat Insarov (Jun 21 2021 at 22:00):I also make an argument that this impediment is not necessarily bound to the functionality of mathcomp.
Ignat Insarov (Jun 21 2021 at 22:00):Do you agree or disagree with this?
Ignat Insarov (Jun 21 2021 at 22:03):See that I am prepared to put time into making a more approachable standard library. I am not asking anyone to do it for me. I only share my experience here because the conversation is taking place.
Emilio Jesús Gallego Arias (Jun 21 2021 at 22:06):I disagree
Emilio Jesús Gallego Arias (Jun 21 2021 at 22:06):I think that stuff that bothers you today
Emilio Jesús Gallego Arias (Jun 21 2021 at 22:07):may actually feel very differently in the future
Ignat Insarov (Jun 21 2021 at 22:07):I do not say it will not. This is not what I asked you to agree or disagree with.
Emilio Jesús Gallego Arias (Jun 21 2021 at 22:08):it is true that math itself is full of notation, shortcuts, and ambiguity, but at least in math-comp you can eventually understand it
Ignat Insarov (Jun 21 2021 at 22:08):I have no doubt in that.
Emilio Jesús Gallego Arias (Jun 21 2021 at 22:08):if that's about your feeling, how can I agree disagree? You have your opinion, it is valid of course
Ignat Insarov (Jun 21 2021 at 22:08):I believe in the efficacy of mathcomp for the expert.
Ignat Insarov (Jun 21 2021 at 22:08):No, I have an experience.
Ignat Insarov (Jun 21 2021 at 22:08):It is not an opinion. It is a story that actually took place in my life.
Ignat Insarov (Jun 21 2021 at 22:09):My roommate can corroborate my sleepless nights.
Ignat Insarov (Jun 21 2021 at 22:09):The other point I am making is technical: naming is not tied to architecture. You can try disagreeing.
Ignat Insarov (Jun 21 2021 at 22:10):Please see also that I have been writing and reading programs in various languages over the years. I have my preferences for good reason and they are not going anywhere because of one odd library. Actually I think myself a programmer of better style than an average mathematician, simply because it is my daily bread to write simple and understandable code, rather than publish narrowly read papers.
Even in the Coq ecosystem, stdpp is an example of much better style, and the code of Adam Chlipala is little short of perfection. So, there is no real problem in writing beautiful and approachable code in Coq — proof by example.
Ignat Insarov (Jun 21 2021 at 22:19):I do not want you to agree with some absurd statement like _«we should immediately throw mathcomp away»_ or _«let's use randomly generated names»_. I never said any such nonsense. I only want to know if you agree that:
mathcomp more beautiful and approachable while keeping the meaning nearly the same.This is really all I am saying over the course of this conversation.
Ignat Insarov (Jun 21 2021 at 22:24):Emilio?
Ignat Insarov (Jun 21 2021 at 22:25):See you later then… Hope no hard feelings.
Joshua Grosso (Jun 22 2021 at 02:06):I'm also a relative beginner to Coq (and almost completely unused to mathcomp), so please take my thoughts with a grain of salt.
In my experience as well, mathcomp has a very steep learning curve—given time, I'm able to prove what I want to, but I sense that my code is comically inelegant when compared to a more experienced mathcomp user's. (For example, I'm only used to seriously manipulating propositions rather than boolean expressions, so I end up littering my proofs with bajillions of apply (rwP foo_barP)s.)
With that said, I don't personally think mathcomp is less "beautiful" due to its notations and names. The software developer in me wants to give everything long, descriptive names as a first instinct (sometimes I define a function with a long name and then make a shorter notation for it, as a compromise with myself). But, my guess is that proofs are sufficiently different from "normal" code that my past experience may be simply inapplicable. Obviously, descriptive names help with future readability and maintainability—but I'm thinking that that might not actually be important when e.g. doing algebraic manipulation in a proof. Maybe nitty-gritty steps really are best-served by being as concise (and thus de-emphasized) as possible.
To my limited knowledge, proof brittleness is a legitimate concern (AFAIK researchers are currently developing proof repair systems), which I guess would be the closest thing to the traditional concept of maintainability. Nonetheless, I'd assume proofs need to be modified much less than executable code. I'd wager that proofs needing to change is several orders of magnitude less common than business requirements requiring algorithms to change.
(I'm a novice thinking out loud here—so don't be afraid to tell me it's all nonsense :-P)
Enrico Tassi (Jun 22 2021 at 07:20):@Ignat Insarov I'm sorry you had troubles using mathcomp. My best effort in making it more accessible is this book https://github.com/math-comp/mcb/ which also gathers some of the reasoning behind the coding style. To answer to your initial question, if you have false in you context you can just use // (the trivial automation) to conclude, this is explained extensively in the book, which I recommend to look at.
Ignat Insarov (Jun 22 2021 at 08:54):Thanks Enrico. I have the book, it is very well written. And I know from it that the naming style of mathcomp is deliberate:
… Finding an appropriate name for a
lemma can be a delicate task. It should convey as much information as possible, while
striving to remain short and handy. In particular, bureaucratic lemmas that are frequently
used but represent no deep mathematical step should have a short name: this way they
are both easy to type and easy to disregard when skimming through a proof script.
All the conversation above is me trying to get across that:
Please believe that I have absolutely no intention to diminish the achievements of yours and your collaborators', and I apologize if some of my messages come across as such. All I want is to make my opponents see that another style is possible and may be advantageous for another section of users of Coq.
Cyril Cohen (Jun 22 2021 at 09:20):Ignat Insarov said:
All the conversation above is me trying to get across that:
- This naming style _(and the choice of notations)_ is indeed deliberate, and may be changed independently of the design and the architecture of the library. _(Please do correct me if this is wrong!)_
- The many short hands and notations impose a barrier on entry. Which is a trade off you of course made consciously in accordance with your design goals.
Hi @Ignat Insarov , I do agree with both these statements, and I am sorry that it made life difficult for you.
It indeed looks like "deliberate obfuscation" to most newcomers and I know it can be deterrent, especially since one needs to hang on long enough to witness how useful it turns out to be (given the current technological context of proof assistants). We (some of my colleagues, like @Enrico Tassi, @Assia Mahboubi, @Yves Bertot for example, but there are more, and myself) would really like to make the learning curve less steep, and we envisioned having simplified versions of mathcomp, using less advanced tactic idioms and why not less compact names at some point. None of this is mature, but they wrote a book and I hope it will help you.
EDIT: indeed it would be nice to be able to turn on a "beginner mode" which prints some hidden coercions and expand some names. And of course examples of code written in pure "beginner mode". And then you could gradually tune the "beginner mode" to more and more "advanced" as you learn more...
Ignat Insarov (Jun 22 2021 at 09:45):No need to be sorry, Cyril and Enrico. The place I stumbled upon the implicit coercion of false into a proposition is an example code for an independent project. It is not even brought into scope from mathcomp — they define it in the same file. I suppose this example was not written with a reader unfamiliar with the idioms of mathcomp in mind… but that is another question altogether.
Ignat Insarov (Jun 22 2021 at 09:45):indeed it would be nice to be able to turn on a "beginner mode" which prints some hidden coercions and expand some names. And of course examples of code written in pure "beginner mode". And then you could gradually tune the "beginner mode" to more and more "advanced" as you learn more...
— Or stay there and keep writing code that is accessible to other beginners!
Cyril Cohen (Jun 22 2021 at 10:42):Ignat Insarov said:
— Or stay there and keep writing code that is accessible to other beginners!
I wish I could, but in my experience, at some point it gets in the way of actually doing stuff, at least with the current technological advances.
The reason is I do not write interactive proofs in the same way I write a program. I change my mind way more often on which path I will take to code and the API is way larger (thousands of lemmas and their names to "remember"/"search"). With shortnames and shorthands, it takes me sometimes <1s to swap two letters and take another path. If names were longer, I would spend 10 times more keystrokes and probably 10 times more time, and given that some formalizations took me months... of course I could think more and experiment less, but is that the point? Of course "final scripts" could be expanded (most scripts in mathcomp if not all are already post-processed to "look better" for some metric, cf section 4.3 of the mathcomp book), but the longest ones, which sometimes fit one to three screens, would become less maintainable. Contrarily to what I read here and there, proofs are often rewritten again and again, in the light of new abstractions and their theories, which even question the meaning of the expression "final script"...
Anyway, a trade-off could in principle be set so that "simple proofs" are written in expanded style, but I would rather have an alternative "beginner style" library of simple results, which helps transitioning to the "advanced style", so that at some point everyone gets the opportunity to be more proficient, with time and experience.
Ignat Insarov (Jun 22 2021 at 11:03):This is bad news for me! What I read from your message is that the state of the art in computer assisted proof writing is such that proficiency implies a lot of typing. That under the requirement that automatic proof search is not wielded. I really hope there is some way to improve on this, waiting to be discovered!
Ignat Insarov (Jun 22 2021 at 11:04):If the art develops fast enough, I may never even hit the ceiling where proofs stop being simple.
Cyril Cohen (Jun 22 2021 at 11:27):I really hope there is some way to improve on this, waiting to be discovered!
I also do hope so, that's why I'm still doing research :) with the hope of lifting more and more burden from the user, and showing how it can be done.
However, you may be overestimating the time and energy required to become a knowledgeable user of mathcomp. Yes it takes some, but I'd say it is a couple of month at most.
Ignat Insarov (Jun 22 2021 at 11:30):It is more that my wishes are modest. I want stuff like a formally proven sieve of prime numbers, factorization of polynomials. Stuff like that. I do not aspire to prove long standing conjectures or formalize any fancy mathematics. Rather, I want the basic stuff to be accessible.
Ignat Insarov (Jun 22 2021 at 11:33):Hopefully I would not need proofs spanning several screens for such modest tasks!
Ignat Insarov (Jun 22 2021 at 11:33):Would I?
Cyril Cohen (Jun 22 2021 at 11:38):Ignat Insarov said:
Would I?
For a prime number sieve, you would't... but for factorization of polynomials, depending on which algorithm you pick, I'm not sure...
Dan Frumin (Jun 23 2021 at 20:37):FWIW you can turn on the display of implicit coercions with
Set Printing Coercions.
It helps if you want to "debug" the state of the proof
Last updated: Oct 03 2023 at 04:02 UTC