The Coq mailing list

[Bai Wei <baiweiyj AT gmail.com>]

Thanks!

When I try to extract the proof of a theorem to Ocaml, the arithmatic proof is erased. 

For example, for the below theorem  plus_O_n:

Theorem plus_O_n : forall n:nat, 0 + n = n.

Proof.

  simpl. reflexivity.  Qed.

Then, I run the extraction command:

Extraction "plus.ml" plus_O_n.

I only got a function name like:

(** val plus_O_n : __ **)

let plus_O_n =

  __

Does the extraction only can be used to deal with inductive relations that can be turned into purely functional programs and erase the arithmatic proof? 

Regards,

Wei Bai

On Thu, Apr 25, 2013 at 12:42 AM, Duckki Oe <duckki AT mit.edu> wrote:

Hi,

After you extract the raw proof term from your Ltac script (to check with Coq's kernel), you will also need to extract all the definitions that your proof may use from the standard library and distribute them as your theory as well. I don't know if there are any tools to automate this process. If you really want to use Coq (with tactics) as a proof generator. This will be the only way to do it. It will be certainly harder to translate Coq terms into simpler type theories like LF (twelf) than the other way around.

If you can use other proof generators (like SAT/SMT solvers), there are more options because SAT/SMT are smaller fixed logics and they have been encoded in several different proof systems.

-- Duckki

On Wednesday, April 24, 2013 at 6:35 AM, Bai Wei wrote:

> Hi. I want to implement Foundatinal proof carrying code (FPCC) paradigm. Does Coq proof checker can be used as a proof checker in FPCC? Many Thanks!
>
> Cheers,
>
> Wei Bai