Skip to main content

Formalization of code in Coq - tactics

· 4 min read
Natasha Klaus

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

Presentation of the features of Ltac (the Coq's tactic language)​

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: unparse_ty and 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 prove.

Some constructors of ty are pretty similar: in particular, there are 12 constructors with just one argument ty_metadata

  | 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 tactic 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. (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.

Built-in Coq tactics​

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: hammer, crush, best...

There are some useful built-in Coq tactics: lia, nia, intuition, trivial, congruence, ring, and many others.

Conclusion​

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.