The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Mon, Sep 29, 2014 at 11:38 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
> Hello,
>
> Here are some remarks about this.
>
> First of all, if you have a proof that [forall n:nat, P(n)] then A
> should always return true, therefore A = [fun x => true] should behave
> as you wish. :)
>
> I suspect however that this is not exactly what you are thinking about...
>
> The standard way of dealing with decision procedure is to prove a
> property like [forall n:nat, P(n) \/ ~P(n)]. This proof is indeed a
> decision procedure if your did not use any axiom in its proof. Note it
> is preferable to prove the variant [forall n:nat, { P(n) } + { ~P(n)
> }], for technical reasons.

The second variant is especially helpful in dependently typed
programming.  You can view a decision procedure as a function that
returns an "answer" along with its certificate.

If you have a verified decision procedure implemented in some other
framework, you can also make this type.  If you haven't verified it
but have reason to believe it's correct, you could take it as an axiom
and in the implementation you'd need to manually patch up code to call
out (if you wanted to extract code).

Another way to think about this is to think about tactics as decision
procedures.  As an example, the "omega" tactic has been coded up as a
decision procedure for arithmetic based on the omega test.  If you
have a decider that provides certificates but isn't fully verified,
you could imagine hooking it into coq by means of a tactic that called
out to the solver.

Kris