Sometimes, we have a valid proof, in the sense that its certificate can be verified. But the proof is too complicated, in the sense that the prover cannot re-discover the proof ("reprove") if we were to lose the certificate. In this situation, we often want to "explicate" the proof, ie to add more detailed steps to the .ac file so that the prover is able to re-discover the proof.

Prerequisite

We can only explicate when we have a valid proof. So, the first step is to check that we have valid proofs in the module that we want to explicate.

acorn check MODULENAME

Note that module names can be single words like "add_ordered_group" or dot-separated like "comm_ring.binomial".

If the check fails, we won't be able to explicate.

Explicating One Module

The next step is to figure out which lines we need to explicate. Run a reprove with --fail-fast. Once we find a line that fails, we'll know we need to explicate it.