This post is a continuation of the previous blog post on proof automation for the `data_encoding`

proofs.

data_encoding is a library used in the Tezos codebase to define binary and JSON encodings, by using some primitives and then combining these primitives with combinators.

As said in the previous post, we defined a custom tactic for automating
`data_encoding`

proofs. These proofs are usually mechanical at the beginning, for
each combinator we have a lemma or axiom that verify the outer term and
generates a *subgoal* for each of the inner terms, and for primitives we have
axioms to eliminate them. The *subgoals* remaining are regarding the combinators
injections and projections, which are distinct for each encoding.

The `data_encoding_auto`

tactic can eliminate all the combinators and
primitives terms, but we still have to finish the last *subgoals* by hand, at
last we did. Now we can use CoqHammer to
finish some proofs increasing even more the our level of automation.

Here is a proof using only `data_encoding_auto`

:

`Lemma ratio_encoding_is_valid`

: Data_encoding.Valid.t Ratio.Valid.t Constants_repr.ratio_encoding.

Data_encoding.Valid.data_encoding_auto.

intros x H; intuition; try apply H.

destruct H as [numerator [denominator dgt0]].

assert (x.(Constants_repr.ratio.denominator) >? 0 = true) by lia.

now rewrite H.

Qed.

And here is a proof using combination of `data_encoding_auto`

and CoqHammer:

`Lemma ratio_encoding_is_valid`

: Data_encoding.Valid.t Ratio.Valid.t Constants_repr.ratio_encoding.

Data_encoding.Valid.data_encoding_auto; scrush.

Qed.

The usual usage of CoqHammer is: you import it with `From Hammer Require Import Tactics.`

,
this puts `best`

tactic into the scope. Whenever you fell that CoqHammer can solve the
current go you fire the `best`

tactic. CoqHammer will try to find multiple
solutions for the current *subgoal* and it will print the best one in the
standard output, you then replace the `best`

with the tactic suggested by it, these include
`sauto`

, `scrush`

, `sfirstorder`

and much more.

`best`

tactic will try to use the lemmas in the scope to solve the *subgoal* but you can also
parameterize it to use other lemmas, here is another encoding verification example:

`Lemma origination_result_list_encoding_is_valid : `

Data_encoding.Valid.t Valid.t Migration_repr.origination_result_list_encoding.

Data_encoding.Valid.data_encoding_auto.

best use: Forall_True.

Qed.

In this case the last *subgoal* is something like this:

`forall x : list Migration_repr.origination_result,`

Valid.t x ->

Forall

(fun v_a : Migration_repr.origination_result =>

...

In *subgoals* like this we usually apply
Forall_True
lemma and continue the proof of the remaining *subgoals*. By parameterizing `best`

with `use: Forall_True`

it can finds its way up to the completion of the
proof. Also, CoqHammer can help us with other proofs not involving
`data_encoding`

as this is a generic automation mechanism for Coq.

Automation is important not only because it boosts our productivity but also because it generalizes the proofs so that they become easier to maintain and more robust to changes in the code.