I'm new to Coq, working on set-theoretic proof writing. I realized that parentheses are omitted, and it makes difficult for me to read the formula. For example, 1 subgoal A, B : {set T} H : B \su...

when constructing proof in coqide, I didn't find a way to step though T1; T2; T3; ...; Tn. one tactic by one tactic. So it became very difficult to construct correct proof like the code above. ...

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then g...

Unlike Agda, Coq tends to separate proofs from functions. The tactics Coq gives are great for writing proofs, but I'm wondering if there is a way to replicate some Agda-mode functionality. Specifi...

I'm using CoqIDE to complete the exercises in the Software Foundations book about Coq. I can successfully compile Basics.v, resulting in Basics.vo and Basics.glob in my directory. When I try to run...

I am a Coq newbie and therefore to improve my understanding of proof checking I am trying to use the Ssreflect library. I have installed Ssreflect v 1.5 on a Mac OS v 10.10.3 ( Yosemite ) which r...