# Yet Another Tactics Index for Beginners

**URL:** <https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249>\
**Category:** Announcements\
**Created:** [April 11, 2024, 6:39pm UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249 "2024-04-11T18:39:16Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![caverill](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/caverill/32/832_2.png) [@caverill](https://discourse.rocq-prover.org/u/caverill)\
**Post date:** [April 11, 2024, 6:39pm UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/1 "2024-04-11T18:39:16Z")

</div>

[https://charlesaverill.github.io/ctpe/](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](https://coq.inria.fr/doc/master/refman/coq-tacindex.html), which is, for lack of a better word, scary for a new Coq user. Then there are a few `intro to tactics list`s, 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).

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [April 12, 2024, 2:01pm UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/2 "2024-04-12T14:01:58Z")

</div>

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

> **[GitHub - jscoq/coqdoc-template: Basic coqdoc template for jsCoq](https://github.com/jscoq/coqdoc-template)**
>
> Basic coqdoc template for jsCoq. Contribute to jscoq/coqdoc-template development by creating an account on GitHub.

---

<div class="post-metadata">

**Author:** ![caverill](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/caverill/32/832_2.png) [@caverill](https://discourse.rocq-prover.org/u/caverill)\
**Post date:** [April 12, 2024, 3:00pm UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/3 "2024-04-12T15:00:51Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![pedroabreu](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pedroabreu/32/203_2.png) [@pedroabreu](https://discourse.rocq-prover.org/u/pedroabreu)\
**Post date:** [April 12, 2024, 4:00pm UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/4 "2024-04-12T16:00:22Z")

</div>

Awesome work. Thanks for sharing!!

---

<div class="post-metadata">

**Author:** ![ybertot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ybertot/32/61_2.png) [@ybertot](https://discourse.rocq-prover.org/u/ybertot)\
**Post date:** [April 15, 2024, 8:34am UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/5 "2024-04-15T08:34:52Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![faelannm](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/faelannm/32/1031_2.png) [@faelannm](https://discourse.rocq-prover.org/u/faelannm)\
**Post date:** [September 9, 2024, 9:57am UTC](https://discourse.rocq-prover.org/t/yet-another-tactics-index-for-beginners/2249/6 "2024-09-09T09:57:46Z")

</div>

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.