I don't think coq is intuitive to anyone :) It might have the steepest learning curve of any language I've learned, possibly tied with Idris, which just so happens to be another dependently typed language. The bits between Lemma and QED are kinda neat -- they're "proof tactics" written in the tactic language LTAC. It's kind of a metalanguage that directs Coq through synthesizing an actual program. Like, for example, here's a simple proposition written in LTAC: intros a b [Ha Hb]. exact Ha. Qed. and here's what Coq synthesizes for that: fun (a b : Prop) (H : a /\ b) => match H with | conj Ha _ => Ha end : forall a b : Prop, a /\ b -> a (fun is the keyword for lambdas, kinda like \ in Haskell.) In other words, that stuff is both program and proof! Lemma fst : forall a b, a /\ b -> a. fst =
What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting. Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P
It feels like most Coq documentation and tutorials are written for people getting Ivy-league graduate degrees where they can just pop over to any number of professors or fellow students to ask a quick question or get a decent idea of what the "right" way to do something is. Not having any of that, it's a bit tricky. I started very simple, proving basic logic statements and getting the hang of those tactics, then branched out a bit into proving things about numbers and lists. A fair bit of that came from Coq in a Hurry. From there, Coq'Art is a dated but good resource for the questions Coq in a Hurry doesn't answer. Most of the proofs mostly work, but some of the tactics are different now? However, even with those resources, I still find myself spending a lot of time looking around on the internet, finding bits and pieces in various disorganized places. Coq's standard library documentation is also horrendous and the various search commands in the language sometimes miss things for no apparent reason. And the error messages are only marginally useful. That said, once you get a feel for its eccentricities it is pretty fun, and learning it has helped me get better at writing proofs even in informal settings! Anyway, all this is to say maybe I should have learned Agda but I have to learn emacs first before I can make a fair call there :D
This is really, really cool from a conceptual perspective. At the same time, I'm immensely glad that I don't have to work with this professionally :) Do you have an end-goal in mind for learning Coq, or is it more of a curiosity you want to satisfy? Curious to see what else you might try with the language!
I also find this way cool. You will probably enjoy Wadler's Propositions as Types if you want to understand the proof/program thing in more detail. I am generally interested in program analysis and theorem proving and that sort of thing. I picked it up to maybe use it with my research, since being able to generate proofs and extract executable code is pretty handy, but we'll see if I can become competent in it fast enough to be able to actually apply it. Also I like roosters I did write another thing about using Coq that shows some of the proof state as you go. The interactive part really makes writing proofs possible; I don't know if I could just look at something and write all the ltac for it without any help. This is a bit more along the lines of what I'm doing for research, but still a long ways from what counts as cutting-edge nowadays :)