Stack Overflow
Stack Overflow

Questions tagged [coq-extraction]

The extraction mechanism allows users to derive ocaml, haskell or scheme code from their coq development. This corresponds to a compilation phase.

28 questions
8
votes
1 answer

Can you automatically add Haskell import statements when extracting from Coq?

I'm doing an extraction from Coq to Haskell that requires importing a couple of modules on the Haskell end. Is there any Coq extraction feature that allows you to do this automatically? I know I could just write a script to do this but I'd prefer…
tlon
  • 413
  • 2
  • 6
8
votes
2 answers

Is it possible to write C programs using Coq?

I know that one can extract Coq programs into Haskell and OCaml programs. Is there a way to do this with C? I am imagining a library that models the C language. Maybe such a library would contain a collection of axioms about how C constructs…
Mark
  • 5,286
  • 5
  • 42
  • 73
7
votes
2 answers

Proofs' role in Coq extractions

I'm trying to understand what is the role of proofs in Coq extractions. I have the following example of floor integer division by two taken from here. For my first try I used the Admitted keyword: (*********************) (* div_2_even_number…
OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
7
votes
1 answer

How to set the module name when extracting Coq to Haskell

When I extract/compile Coq to Haskell using Extraction Language Haskell. in the Coq file and running coqtop -compile mymodule.v > MyModule.hs, I get a Haskell module which starts with module Main where. Is there an option to set the resulting…
yairchu
  • 23,680
  • 7
  • 69
  • 109
6
votes
0 answers

Extract functor in Coq to OCaml using Extraction mechanism of Coq

I have a function PolyInterpretation (http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html) Definition PolyInterpretation := forall f : Sig, poly (arity f). and a module signature…
Quyen
  • 1,363
  • 1
  • 11
  • 21
5
votes
1 answer

What does the Coq command Require Import Ltac do?

When I am looking at the QuickChick project, I encountered the sentence Require Import Ltac. I don't know what this does and where the Ltac module is. I found a file plugins/ltac/Ltac.v, but this couldn't be the one since this file is empty (by the…
Jian Wang
  • 103
  • 5
5
votes
1 answer

Generating Haskell code from COQ: Logical or arity value used

I am currently trying to generate Haskell code from my program verification lemma, which looks like this: Lemma the_thing_is_ok : forall (e:Something), Matches e (calculate_value e). Right after ending my Section, I do: Extraction Language…
wtf8_decode
  • 452
  • 6
  • 19
4
votes
2 answers

Coq: Strong specification of haskell's Replicate function

I'm having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it creates a list of length n, with all elements equal…
Cris Teller
  • 99
  • 5
4
votes
2 answers

string_dec and string in Ocaml library

I have file: String0.ml extracted from String.v (It is from Coq library) String.ml : is a string library of Ocaml After extracted my test file from Coq to Ocaml, I want to used String.ml in the library of Ocaml, so I write an replace command to…
Quyen
  • 1,363
  • 1
  • 11
  • 21
3
votes
1 answer

Use function after generated by extraction from Coq to Ocaml

I have a folder tmp which is generated after I do extraction from coq to ocaml. ~/tmp/cpf0.ml cpf0.mli cpf0.o cpf0.cmi cpf0.cmx cpf0.cmo main.ml is a file I use to call one function in cpf0 : let prf = Cpf0.proof;; I got an error saying…
Quyen
  • 1,363
  • 1
  • 11
  • 21
3
votes
1 answer

Coq proof usage

I'm a beginner with Coq, I learnt the language quickly, to do proofs etc. But I don't understand what can we do with this. Ok we prove some definitions etc. But in which ways can we use them? I saw that we can extract in Haskell files, but I don't…
ARevX
  • 31
  • 2
3
votes
1 answer

Extraction of Type Scheme

I'm trying to extract some file system code that I've written in Coq. I want to replace my FileIO Monad with Haskell's IO Monad. My code looks like this: Variable FileIO : Type -> Type. Variable sync : FileIO unit. Extract Inlined Constant sync =>…
Konstantin Weitz
  • 6,180
  • 8
  • 26
  • 43
2
votes
0 answers

Coq tutorial on evars, e* tactics, contexts?

I've been trying to find a good guide/read/set of exercises on Coq Contexts, evars, e* tactics etc. Ideally I want to build a Coq context with some vars abstracted, which I'll fill in later in the OCaml or Haskell extraction. Is that possible and…
rausted
  • 951
  • 5
  • 21
2
votes
1 answer

OCaml string and Coq string (Extraction from Coq to OCaml)

I used the extraction from Coq to OCaml, where I have type Z, N, positive I don't use to extract it in int of OCaml. Then the type I have after the extraction is: type positive = | Coq_xI of positive | Coq_xO of positive | Coq_xH type coq_N = |…
Quyen
  • 1,363
  • 1
  • 11
  • 21
2
votes
1 answer

The extraction of coq type nat into which type of ocaml so that I can have a certified program

In Coq, the extraction from type nat into int or big_int are not certified (they are efficient). As in these links…
Quyen
  • 1,363
  • 1
  • 11
  • 21
1
2