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