Yet Another Tactics Index for Beginners

Announcements
1

https://charlesaverill.github.io/ctpe/

I’ve been using Coq for a little longer than a year now. One of the things that left me very apprehensive about learning more about the system was the (in my opinion) poor availability of simple explanations of tactics. We have the official tactic index, which is, for lack of a better word, scary for a new Coq user. Then there are a few intro to tactics lists, but they focus a lot on the tactics that I was able to figure out on my own. So I decided to write yet another list of tactics that I think get used a lot but don’t get enough attention, especially their alternate forms.

I’m updating this in my free time so not a whole lot of constant development. Next big category I’d like to add are the e-tactics (In hindsight, I had way too much trouble understanding them for how complex their usage actually is - likely a me problem).

7 Likes
2

Very nice @caverill , you could also make the page interactive at some point if you feel like, using jsCoq.

There is a little template to get you started, but note that you can just use your current page .html

2 Likes
3

Good idea @ejgallego! I’ll definitely integrate this, thank you!

1 Like
4

Awesome work. Thanks for sharing!!

1 Like
5

I have not looked at it yet, but if there is enough acclaim, we should add a pointer to this page from the Coq web-site.

2 Likes
6

Thank you @caverill for sharing your work I appreciate your effort to simplify Coq tactics, as the official index can be overwhelming. I want to the addition of e tactics; they can be quite complex, so your insights will be very helpful.

1 Like