For the Proof Engineer, the formalization of code in Coq is like an amazing adventure. But sometimes it can be tedious and monotonous due to the same repetitive actions that programmers should perform. Fortunately, Coq provides us with proof automation which helps us significantly increase our productivity.
In this post, we will show how we use/write tactics in our work on Tezos code formalization. In particular, we will touch the following topics:
- presentation of some features of Ltac (the Coq's tactic language),
- recursive proof search,
- built-in Coq tactics
Please consider the lemma below:
Lemma unparse_ty_parse_ty (loc_value : Alpha_context.Script.location) (ctxt : Alpha_context.context) (ty : Script_typed_ir.ty) (legacy allow_lazy_storage allow_operation allow_contract allow_ticket : bool) : match (unparse_ty loc_value ctxt ty) with | Pervasives.Ok (mich_node, ctxt1) => match parse_ty ctxt1 legacy allow_lazy_storage allow_operation allow_contract allow_ticket mich_node with | Pervasives.Ok ((Ex_ty ty1), ctxt1) => ty = ty1 | Pervasives.Error _ => True end | Pervasives.Error _ => True end.
In this lemma, we need to prove the compatibility of two functions:
parse_ty. We are now going to dive into this lemma and examine its details.
We are going to consider the fact that type
ty itself is rather big and has 32
constructors. In order to prove our lemma, we will need to prove it for each and
every constructor of
ty. So in total, we have 32 subgoals, which we have to
Some constructors of
ty are pretty similar: in particular, there are 12
constructors with just one argument
| Unit_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty | Int_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty | Nat_t : Script_typed_ir.ty_metadata -> Script_typed_ir.ty ...
All these 12 subgoals can be solved with very similar blocks of code (but still, there are differences in the code for each constructor).
In order to automate the solution of these 12 subgoals, we create the
destr_if and call it in the body of our proof.
This is what we gain:
- code gets shorter
- code gets more readable
- we avoid reduplications in the code
Here is the tactic, written in Ltac:
Ltac destr_if := match goal with | |- match (let? ' _ := Alpha_context.Gas.consume _ _ in _) with _ => _ end => destruct Alpha_context.Gas.consume; [ simpl in * | simpl; trivial] | |- match (if ?cond then _ else _) with _ => _ end => destruct cond; simpl; auto | |- match (let? ' _ := Script_ir_annot.check_type_annot _ _ in _) with _ => _ end => destruct Script_ir_annot.check_type_annot; [ simpl in * | simpl; trivial] | |- ?a _ = ?b => unfold b; subst; reflexivity end.
Okay, our tactic can solve 12 goals. Do we have to call our tactic 12 times? Nope! We will call it just once, please consider the code below, it solves automatically all 12 subgoals.
Proof. intro H. destruct ty eqn:TY; simpl; repeat destr_if.
We used the tactic combinator
(repeat tactic_name) would loop through
a running tactic, and will run it on all subgoals, which were generated,
and on sub-sub-goals and so on. The process would stop only when the tactic
fails. Sometimes we fall into frivolity and use repeat on tactics that always
succeed. In these cases, we usually have to reload the computer.
We can expand our tactic by calling repeatedly some built-in Coq tactics.
When one of the tactics fails at any point of our search tree, that particular
subgoal is left to be handled by later tactics and so on. There are some
"all-powerful" tactics that give the developer a feeling that any goal can be
solved with them. This feeling is, of course, deceptive. But developers are
giving them fancy names that speak for themselves:
There are some useful built-in Coq tactics:
ring, and many others.
Tactics in Coq are programs that find proof. We can use built-in tactics, or if we need a higher level of automation, we can write our own tactics in Ltac and tune them for specific goals. In our work on the Tezos' code formalization, tactics play important role. If some tactic is really specific we keep it in the file where we use it (for example the tactic for data-encodings is in Proofs/Data_encoding.v). If the tactic is universal and can be useful in many files we locate it in our tactics library.