Below, we provide a toy example for how you can use Tactician in your development. This page is a fully-fledged version of Coq, based on jsCoq. You can interactively navigate through this document using either the green buttons on the top right of the page, or using the shortcuts Alt+Down and Alt+Up.

This demo is based on lists of natural numbers. These `lists`

are inductively
defined with the constructors `nil`

for the empty list and `cons`

for adding
a number to an existing list.

With these lists we define the notations `[]`

for the empty list and `n :: ls`

to
append the number `n`

to the list `ls`

.

We are going to prove things about the concatenation operation on lists. Concatenation is defined below
as the function `concat`

with the notation `ls₁ ++ ls₂`

representing the
concatenation of the lists `ls₁`

and `ls₂`

.

The first thing we whish to prove is that the empty list `[]`

is the right identity of concatenation:

Now we need to prove this lemma, as can be seen with in the goal on the right panel. This is where Tactician's
automation comes in. The two main commands that Tactician provides are `Suggest`

and
`search`

. You can try `Suggest`

now, but because we have not proven anything yet Tactician
has not learnt any tactics yet and is unable to suggest anything:

Therefore, we will have to manually prove this lemma to give Tactician something to learn from:

The system has immediately learnt from this lemma. (It was even learning during the proof of the lemma,
you can see this by inserting `Suggest`

in different places in the proof above.)
Tactician is now ready to help you prove the next lemma, namely the associativity of list concatenation.

We can again ask for suggestions, and this time Tactician is able to give some answers:

If you wish, you can follow some of the suggestions by copying them into the editor. You can then repeatedly ask for more suggestions. Sometimes they will be good and sometimes not. Alternatively, you can also ask Tactician to search for a complete proof:

Tactician now immediately solves the goal. Notice that it has also printed a caching tactic in the right
bottom panel. You can copy this tactic and replace the original `search`

tactic above with it.
Now, when you re-prove this lemma, Tactician will first try to prove it using the cache, only resorting
to proof search if the cache fails (this can happen when you change definitions the lemma relies on).

In this example, we show how you can teach Tactician about user-defined, domain-specific tactics. This is very useful as it allows you to teach Tactician the "tricks of the trade". We start with an inductive type that incodes the property that one list is a non-contiguous sublist of another:

Here, `nc_sublist ls₁ ls₂`

means that `ls₁`

is a non-contiguous sublist of
`ls₂`

. We might now try to prove the proposition `nc_sublist (9::3::[]) (4::7::9::3::[])`

.
Altough this is clearly true, manually choosing the right constructors of `nc_sublist`

to prove this
is not entirely trivial. Instead, we can write a tactic that automates this for us. The following tactic will
repeatedly try to use the constructors `ns_cons₁`

and `ns_cons₂`

until it can finish
the proof with `ns_nil`

, backtracking if it reaches a dead-end.

Now, we can easily prove our proposition with this custom tactic:

As with other tactics, Tactician has immediately learned about `solve_nc_sublist`

.
Before we ask Tactician to use it, we will first teach it about using the lemma `concate_nil_r`

to rewrite a goal:

We will now ask Tactician to use the things it learned from these two examples to prove a more complicated lemma (although this is still a toy example).