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).