Order of proof evaluation in a lemma

[briangmilnes]

When checking when a lemma is not validating, I put in asserts and admits.
Most commonly,
let lemma_foo ...

if base-case
then ()
else admit().

If the validator is underlining the first () is it really telling me that it can't prove the
base case?

It does seem that if I have a
then (
assert(lemma precondition 1);
assert(lemma precondition 2);
lemma_...
)
That it is checking these in order. I can check this with an assert(False).

More generally, what is the algorithm (guarantee) of validation order?

[aseemr]

Hi Brian:

For the first example, indeed, if the first proof with the base-case does not go through, that means the solver can't prove the base case.

For the second example, there is no guarantee on the order of asserts. When all the asserts succeed, then the guarantee is that all the asserts succeed ( : ) ). But if some assert fails, then read is as at least that assert fails, but no guarantees about other asserts that are before or after the failing one. Though practically, I have also seen that the error usually points to the first assert that fails, but we should not rely on this behavior. All the asserts are sent in a single query to Z3.

But there is a command line option split_queries that sends each assert in a separate query to Z3 and reports all the asserts that fail. If you have multiple asserts and you want to know which of them succeed and which of them fail, you could try this option. (This option can be set in the file also with the #push-options or #set-options pragmas.)

[briangmilnes]

Thanks, I'll play with it. A bit more documentation on this would help learners develop proofs.
I'll suggest it to Nik.