Raymond Smullyan's books can teach a fair bit about logic, up to about Godel's theorems and the halting problem (I remember To Mock a Mockingbird fondly), through carefully written sequences of puzzles that lead up to proofs of them. If you try to go through his books encoding the puzzles and their solutions in Coq, then you'll learn quite a lot about Coq and constructive mathematics also.
An interesting idea! I've long wanted to go through more of his books, and I've also long wanted to learn Coq, so that sounds like an interesting combination. Have you found it worthwhile to learn Coq?
Encoding (a subset of) the puzzles as SAT problems for something like z3 would be an alternative to Coq.