During our work on verification of Tezos source code,
we faced a problem: some proofs were taking too long time to execute.
For example, function which proves equality of parse_ty_aux and
dep_parse_ty_aux was executing about 5 minutes, according to CI
(Not acceptable! We couldn't even merge this proof!).
For the information why we actually needed to prove the equality of parse_ty_aux
and dep_parse_ty_aux, and why we had to create a function-simulation
dep_parse_ty_aux, please check this article:
Simulations - dependently-typed version
What is the reason of such a long execution period? First of all the length of
original parse_ty_aux is about 500 lines of code. So the term itself is rather
big, and each step of its reduction is a time-taking procedure.
Many other functions that also need to be verified are even longer, for example
the Fixpoint parse_data_aux is having 4932 lines of code. Therefore, it is
very important that the proofs for such a long functions are optimized.