The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 18.12.2012 21:27, schrieb Victor Porton:
> Hi all,
>
> Once I attempted to learn and use Coq. Then I decided not to continue with 
> Coq for reasons in my pre-previous email to this mailing list.
>
> As for now, I've forgotten much of it and would need learn it anew.
>
> With a solution offered by Olivier Uanelineur, the reason why I stopped to 
> use Coq disappeared.
>
> So I am now again faced with the decision: Should I use Coq?
>
> I'd like to formalize poset/lattice theory with Coq and afterward to 
> formalize my theory.
>
> I've recently put my entire theory into one 216 A4 pages book. Now I am busy 
> with checking my book for errors. In any case I need to finish my (manual) 
> checking for errors in the book and settle it with a publisher. (And I find 
> many little errors while checking it.)
>
> Is it worth to formalize my book in Coq afterward?

Dear Victor.

So apparently after finishing a project and before publishing a book, 
one turns to the deep questions of life.
What is my purpose in this life? Can anything I do be useful for God? 
Should I use Coq to formalize my book?

There are many things I would suggest if you feel like this. Let me 
first answer concerning the initial, Coq question. That is a tough one. 
I would not suggest learning Coq WHILE formalizing a 216 pages proof 
concerning lattice theory. You will encounter many small hardships and 
all of them will be very frustrating. If you have no intuition for why 
Coq rejected your Lemma, this "debugging" will take a ton of time. But 
of course developing this intuition takes time.
There are some things which are very hard to formalize in Coq and not so 
hard to prove on paper. Sometimes things have to be restructured. I have 
very little knowledge of lattice theory, so I'd be a fool to make myself 
a judge in this case. My rule of thumbs is that inductive types and 
structurally inductive proofs are very nice to formalize; everything 
else can become a major pain.
I have had to chew through Barras' formalization of confluence and 
termination of CC and I extended it by some amount. There were a few 
such things, like extensional equality, that Barras was able to build 
around. It was a very technical and hacky solution. If you're not 
familiar with Coq, a problem of this size might already be more than an 
unsatisfying technicality - it might be the death of the endeavour. Of 
course there is always the Coq mailinglist, where such problems can be 
solved - but if you'll throw the towel everytime, just like you just 
were doing, I can guarrantee you won't be very productive.
Apart from this, formalizing your stuff in Coq certainly is a great way 
to find and eliminate all the errors you have been talking of. It is not 
unusual to introduce a miriad of problems, forget minor cases or 
conditions, etc - Coq, of course, will force you to fix all of this. 
Apart from this, some working Coq code certainly is a great way to add 
credibility to your proof.
I have to admit that sometimes, when I encounter some new problem, the 
first thing I think about is how to formalize it in Coq. It really 
itches me to formalize it then. Lately I haven't had the time to do it, 
but it still was a great feeling whenever I did and managed to conquer 
the Coq. It's very rewarding in itself, if you have the time to do it.

Now on to your more severe problems. Obviously this is not the forum to 
discuss such things, but I can recommend this: the Jesuit order offers 
spiritual exercises called retreats. The interesting thing is that these 
services are sometimes offered for groups of atheists and non-believers 
as well. The idea is to find your place in the world, and answer 
personal questions (like the ones you ask above). The means is a few 
days of silence, in which you contemplate and meditate, read, discuss 
privately. You are guided through this quest of self-discovery by a 
member of the order. Even though I did not take part in such an event 
yet, I have heard only good things thus far. I plan to attend such an 
event once I have my phd (and I'll probably need it then, haha).

In any case, I hope this e-mail helped you in some way.

Kind regards, Jonas