prove command returns Valid even when there are unsolved subgoals

[brianhuffman]

Using the new goal_apply tactic, we can create proof states that contain multiple subgoals. A proof is supposed to be complete when all of its goals have been discharged; however, prove seems to succeed even if there are still more unproved goals. (It does print a little warning message though.)

sawscript> let andI = core_axiom "(a b : Bool) -> EqTrue a -> EqTrue b -> EqTrue (and a b)"
sawscript> r <- prove do { simplify (cryptol_ss()); goal_apply andI; abc; } {{ True && False }}
prove: 1 unsolved subgoal(s)
sawscript> print r
Valid

On the other hand, prove_print correctly checks for unsolved subgoals and fails if there are any left:

sawscript> result <- prove_print do { simplify (cryptol_ss()); goal_apply andI; abc; } {{ True && False }}

user error ("prove_print" (<stdin>:1:11-1:22):
prove: 1 unsolved subgoal(s)
Valid)
sawscript> print result

<stdin>:1:1-1:13: unbound variable: "result" (<stdin>:1:7-1:13)

[brianhuffman]

I think that fixing this will require us to change the return type of prove. Currently we have

prove : ProofScript SatResult -> Term -> TopLevel ProofResult

where ProofResult has just two constructors: Valid, and InvalidMulti which contains a counterexample. Maybe we should add a third Unknown constructor to ProofResult, which could cover cases like "solver gave up" or "this goal is valid, but unsolved goals remain".

[atomb]

I'm going to mark the commands that work with multiple subgoals as experimental until we fix this.

[brianhuffman]

@atomb: That seems reasonable. I don't think we want to change the type of a basic saw-script operator like prove at the last minute before a release. We can fix this properly before the next one.

[robdockins]

I think this may be fixed now, following some reworking of the proof infrastructure. We should write a test case.