applyTactic: different behaviour in implicit arguments vs. interactive theorem proving

[pa-ba]

If applyTactic is used to derive implicit arguments, we need to sprinkle Solves in between the tactic script we produce. If applyTactic is used in interactive theorem proving those Solves result in an error message.

Consider the following Idris code that uses the custom tactic findFoo to find the implicit argument for the function foo:

data Foo = Bar

findFoo : List (TTName, Binder TT) -> TT -> Tactic
findFoo _ _ = Refine "Bar" `Seq` Solve

foo : {default tactics { applyTactic findFoo; solve } f : Foo} -> Foo
foo {f} = f

We can then use foo as follows:

useFoo : Foo
useFoo = foo

However, if we use interactive theorem proving to fill out the implicit argument, we get an error.

useFoo' : Foo
useFoo' = foo {f = ?f}

In the REPL we then try to prove f with the tactic applyTactic findFoo. But we get the error message

INTERNAL ERROR: Nothing to fill in. This is probably a bug, or a missing error message.

The situation is reversed if we remove the 'Seq' Solve part from findFoo as follows:

findFoo : List (TTName, Binder TT) -> TT -> Tactic
findFoo _ _ = Refine "Bar"

Then useFoo' does work, but useFoo does not work and we get the error message

Incomplete term

[david-christiansen]

The issue here is that the tactics construct and the prover are doing two different things. The prover automatically uses a solve when it can, because this gives a better user experience, as does the proof construct in Idris itself. You can get the tactics behavior in the interactive prover by first issuing the command :unset autosolve.

[pa-ba]

I tried the proof construct:

findFoo : List (TTName, Binder TT) -> TT -> Tactic
findFoo _ _ = Refine "Bar"

foo : {default proof { applyTactic findFoo } f : Foo} -> Foo
foo {f} = f

useFoo : Foo
useFoo = foo

Now I get the following error message:

INTERNAL ERROR: Nothing to fill in.

[edwinb]

The 'proof' construct won't work here - it is only useful if it introduces a complete proof, as it applies "solve" repeatedly which might close some things that it shouldn't. It is about giving a better user experience, as David said. "tactics" is the proper way, but you do also need the "solve".

We don't have any very good explanation of this behaviour in the documentation, nor do I have time to write a proper one here, but what you're seeing is the intended behaviour which is documented badly. I'm currently writing up (slowly) how to do proofs in Idris, and hopefully I'll address it then.

[david-christiansen]

@pa-ba Can we close this?

[pa-ba]

Yes, you can close this. Thanks for clearing things up.