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