i am trying to learn coq on my own so that i can better understand the logic part of ai lectures in my university . i am trying to do all the exercises on my own to better understand coq. but i think some part of the exercises are to much time consuming so i need help to solve them . i dont want to check the complete solutions just need some kind of hint to solve them quickly.
example :-
Theorem identity_fn_applied_twice from the basics file which looks very long.
IMHO, if you really intend to self-learn how to program in Coq, a couple of hints per year might be fine (so to speak), but otherwise you have to go through the exercises yourself, as concocting an approach to a problem is most of what there is to the whole endeavour. Though you don’t need to solve them all, at least not at a first pass: 1 and 2 star exercises might be enough to get to the point you care for. That said, a proof of the theorem you have mentioned, without any shortcuts, takes literally four lines of code, of which the first is an intros, the last is a reflexivity, and the two in between belong to the little set of tactics that have been presented at that point…
And, if that is already too much for you / for your need of a more concrete grasp of basic logic, maybe you should look at something else altogether: namely, there are quite a few “logic calculators/solvers” based on natural deduction or sequent calculus, that are more focused to the problem of doing logic, that are also more “conventional” in that they more directly resemble what “doing logic” at a basic level looks like, and are of course also easier to use, some of which tools are even available online. (I could try and dig up something if you need.)
Anyway, my 2c: and I hope that hint helps.
1 Like