Tactic languages
Beta Ziliani
I use company-coq in Emacs. Some symbols will
display differently in your setup. At the
bottom of this file there is a list of
symbols used.
Example: An optimized arithmetic evaluator
Idea: have a syntactic representation of
arithmetic operations so we can write a sound
optimizer.
Ingredients:
- The type of arithmetic expressions [ aexp ].
- An evaluator: [ ⟦a⟧ₙ ]
- An optimizer: [ optimize a ]
- A proof of soundness: [ ⟦optimize a⟧ₙ = ⟦a⟧ₙ ]
We can evaluate an arithmetic expression
Optimization
The following function takes an arithmetic
expression and slightly simplifies it, changing
every occurrence of [0 `+ e] into just [e].
(Note: there are two pattern-matches here!) To make sure our optimization is doing the
right thing we can test it on some examples
and see if the output looks OK.
But if we want to be sure the optimization is
correct -- i.e., that evaluating an optimized
expression gives the same result as the
original -- we should prove it.
Proofs can be written in a variety of forms. Vanilla Coq of An Inexperience User
Problems:
- repeats a lot of similar operations.
- it resorts to arbitrary named variables.
- The proof breaks at any change in the context
or in the naming conventions in Coq.
- What if we add...? [Let a1 := `1.]
Proof without naming usign ssreflect.
Better, but still has a lot of repetition. A shorter proof with some automation.
If we remove the comments, we see that the
whole proof is only a few lines long now: (I
am inlining the first case)
We avoided the repetition in the proof and the
explicit use of generated names. However, there
is still a big issue here: we need to remember
the exact positions of variables and hypotheses
(the [?] and [->])! Writing custom tactics Let's write an alternative formulation,
without having to remember positions. The idea is
to pick from the context the right hypotheses to
do rewrite. We write a tactic using Ltac, the tactic
language of Coq.
Simplify and move everything in the list of
hypotheses.
Adapting proofs to changes in definitions
We now perform a reasonable change and see how
that affects our proof. Instead of having one case
for each binary operator, we squish them in one
case.
This is exactly the same
Same here
The optimizer is a bit different
We introduced the change; let's replay now the
proof and see how it breaks.
The actual proof
Idea: specify the type of the element to
perform elimination or case analysis so we always
know before hand why the proof breaks.
Let's do a tactic to check the type of the first
variable in the goal.
Add some nice notation because why not
If we have used the check in the original
proof, we would have gotten a much better error
message.
Specifying the exact cases There is one last annoyence: we have no
guarantee that the case we're solving is actually
the case we want to solve: what is [first] or
[last]? When should [try] succeed?
We change the optimizer to do one more thing:
If we replay the same proof as for [optimize],
it breaks:
We have more cases!
We'd like to write a tactic to select specific
cases in an elim/case, something of the sort
✓ binop; case; except OPlus, OMult do
solve_rewriting.
Unfortunately, Ltac won't help us here: there is
no support for this, or at least no simple way to
solve it without resorting to ugly hacks.
We need to bring another tactic language.
This is not the only limitation of Ltac: another
limitation is present already in the [✓] tactic,
as it doesn't work properly for polymorphic types:
We will make little use of its __typed__
nature, which is crucial in certain types of
tactics (see [Kaiser et al., ICFP 2018] for this
kind of use).
The point we make here is to show features that
are useful to code proofs and must therefore be
incorporated into tactic languages.
We start by re-doing the tactics we wrote so far,
but now in Mtac2.
Here we are just "importing" other tactics:
the ones from ssreflect and the tactic
[solve_rewriting] tactic we did above.
We re-create [check_arg] because of Ltac's
issue. We define a specific exception for it.
[check_arg] is almost the same as the Ltac
version.
Note: It is a Coq definition! We can write a
standard Coq notation for it:
We can write the proof almost as we did before.
[|1>] is [first] and [l>] is [last]
So far, we gain little to what we had. The
interesting bit comes when we can specify exactly
what are the cases we expect will remain in the
proof. For this we use the tactical included in
Mtac2 to specify the specific cases a tactic must
apply:
When we use the same proof for [optimize_more]
we see the error we get:
The error message could be improved. Good
news: we can do it easily! The Mtac2 tactics are
all written in Gallina, so we can simply rewrite
them at will for our project (of course, we can
and should also push to Mtac2's repo!).
Let's define an exception to show the
constructor of the failing case.
Yes, I love notations!
[apply_except] takes a list of constructors
[l] and a tactic [t]
We try the same proof again.
When applied to a real proof (also from SF) we
get... (demo PE.V)
Before concluding: One liners An alternative to the full-control style of
proving advocated here is to use heavy
proof-search. Let's bring THE HAMMER!
Problems:
- It often takes way too long to solve or fail.
- When it fails you don't know why and how to fix it.
Supplementary material
We will now move to a different kind of
tactics: we will take a natural number and convert
it to a
We can add a proof that the result evaluates
to the same.
It is too typed: it fails because we do not
have a proof for every nat.
Closing words