The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> I'm really disappointed with the tone of your remarks. If your 
> intention was to humiliate me, you have succeeded.

No, that wasn't my intention.  I'm confused about why you answered my 
previous suggestion by (what I interpreted as) saying that I wasn't 
suggesting "the right proof" of the theorem you had posed... or did you 
think that it was not possible to finish the proof from that point?  To 
me, it's a fundamental confusion to refer to a term of type [Prop] as a 
"specification," so I assumed you were lacking some basic background 
when you wrote that.  I also got the impression that you were working 
with some implicit rule that classified some proofs of a proposition as 
better than others, in some computational sense, which seemed to 
indicate another misunderstanding.

It sounds like maybe the issue is that Coq's versions of type families 
in different universes (e.g., [ex] vs. [sig]) were too bewildering at 
first, so you just picked [ex], though [sig] matches your intentions 
better.  If you are thinking of your implementation as aiming towards 
extracting programs, you should switch to [sig], especially if you want 
to ask more questions here and avoid confusing people.  I also want to 
re-emphasize that the canonical way of doing this involves writing 
normal functional programs, not going through interactive tactic 
sessions, even if your program has a rich dependent type.