"Apply evidence mismatch: non-function or dependent function"

[brianhuffman]

I'm trying to speed up a SAW proof by using a tactic to do explicit case analysis on a boolean variable b. Running z3 separately on two goals with b instantiated to True and False turns out to be much faster than running z3 on a single goal where b is a symbolic boolean variable.

To do the case splitting, I defined a case splitting rule with core_axiom like this:

Bool_cases <-
  core_axiom "(P : Bool -> Prop) -> P True -> P False -> ((b : Bool) -> P b)";

and then I used goal_apply Bool_cases in the later proof. The tactic seemed to work, I was able to print each of the resulting subgoals with print_goal, they looked like I expected them to, and z3 was able to discharge each of the new goals. But then when the proof script finished, I got this error message at the end:

Apply evidence mismatch: non-function or dependent function
(P : (Prelude.Bool -> Prop))
-> P Prelude.True
-> P Prelude.False
-> (b : Prelude.Bool)
-> P b

What's up with this? This example should work.

[brianhuffman]

The problem seems to be that checkEvidence with ApplyEvidence only allows theorems with non-dependent types. In other words, it can handle theorems that are simple implications, but not ones with any universal quantifiers. This is a severe restriction. We should extend the ApplyEvidence so that it can track the instantiations of any universal quantifiers in the theorem.

[robdockins]

Indeed, we cannot handle applying universal quantifiers at the moment.

In the worst case, this can't be done without requiring the user to provide the instantiation for the quantifier. I think this can already be done now in a very clunky way by a combination of goal_insert and goal_exact, but it should really be easier to do this kind of forward reasoning.

In many cases, however, an instantiation can be discovered via unification. This gets quite a bit more complicated to implement, but should handle lots of the easier cases. I don't know if we have the necessary flavor of unification already implemented.

[robdockins]

Looking at the code history a bit, I think I underestimated what goal_apply was able to do when I consolidated code together into the Proof module. It looks we are already doing a best-effort higher-order matching procedure to determine the subgoals and it is just the evidence checking that can't follow the argument.

I think we need to capture the computed instantiations in that step so the evidence checking pass knows how to specialize the given theorem.

[brianhuffman]

The goal_apply tactic already does precisely the unification we need; it uses the resulting instantiation to figure out what the new goals are. (See the call to scMatch in goalApply.) The problem is that it doesn't record the unifying instantiation in the Evidence value.

[brianhuffman]

I was thinking about updating the Evidence type from ApplyEvidence Theorem [Evidence] to ApplyEvidence Theorem [Either Term Evidence]. This way if you get a Left you can instantiate the outermost Pi of the theorem with the Term, and with a Right you can apply the theorem to the evidence as is done currently.

[robdockins]

I was thinking about updating the Evidence type from ApplyEvidence Theorem [Evidence] to ApplyEvidence Theorem [Either Term Evidence]. This way if you get a Left you can instantiate the outermost Pi of the theorem with the Term, and with a Right you can apply the theorem to the evidence as is done currently.

That is roughly what I was considering as well. This would let us pretty easily implement an explicit specialization step also.

We'll have to think pretty carefully about making sure de Brujin variable bindings end up handled correctly, but is should otherwise be OK.

[robdockins]

Fixed via #1587