我正在从Coq提取到Haskell,需要在Haskell端导入几个模块.是否有任何Coq提取功能允许您自动执行此操作？我知道我可以写一个脚本来做这件事,但我宁愿不必重新发明轮子.
我试图了解证明在Coq提取中的作用。我被两个取自有地板整数除法下面的例子在这里。我第一次尝试使用Admitted关键字：
(*********************)
(* div_2_even_number *)
(*********************)
Definition div_2_even_number: forall n,
(Nat.Even n) -> {p:nat | n=p+p}.
Proof.
Admitted.
(*************)
(* test_even *)
(*************)
Definition test_even: forall n,
{Nat.Even n}+{Nat.Even (pred n)}.
Proof.
Admitted.
(********************)
(* div_2_any_number *)
(********************)
Definition div_2_any_number (n:nat):
{p:nat | n = p+p}+{p:nat | (pred n) = p+p} :=
match (test_even n) with
| left h => inl _ (div_2_even_number n h)
| right h' => inr _ (div_2_even_number (pred n) h')
end. …当我Extraction Language Haskell.在Coq文件中使用Coq提取/编译Coq到Haskell 并运行时coqtop -compile mymodule.v > MyModule.hs,我得到了一个以Haskell开头的模块module Main where.
是否可以选择设置生成的Haskell模块名称？
我目前管道像这样sed -
coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs
但我正在寻找一个更清洁的解决方案.
我有一个功能PolyInterpretation(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html)
Definition PolyInterpretation := forall f : Sig, poly (arity f).
和模块签名TPolyInt(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html)
Module Type TPolyInt.
Parameter sig : Signature.
Parameter trsInt : PolyInterpretation sig.
Parameter trsInt_wm : PolyWeakMonotone trsInt.
End TPolyInt.
Module PolyInt (Export PI : TPolyInt).
然后在我的文件中rainbow.v,我定义了一个TPolyInt_imp使用仿函数的模块目的PolyInt
Module TPolyInt_imp.
Variable arity : symbol -> nat.
Variable l : list {g : symbol & poly (arity f).
Definition sig := Sig arity.
Definition trsInt f := fun_of_pairs_list …我知道可以将Coq程序提取到Haskell和OCaml程序中.有没有办法用C做到这一点？
我想象的是一个模拟C语言的库.也许这样的库将包含关于C构造如何与过程存储器相互作用的公理集合,以及关于IEEE浮点数的公理和定理.然后,它将能够在Coq中构建一个C程序以及有关该程序的定理.
比方说,我会使用这样一个库来构建一个C快速排序算法,该算法适用于可由GCC编译的浮点数组.
我目前正在尝试从我的程序验证引理生成Haskell代码,如下所示:
Lemma the_thing_is_ok : forall (e:Something), Matches e (calculate_value e).
在结束我的部分之后,我做:
Extraction Language Haskell.
Recursive Extraction the_thing_is_ok
它似乎并不是真的很高兴,因为它返回以下错误:
__ = Prelude.error "Logical or arity value used"
我有另一个Lemma似乎确实输出得很好,但我无法弄清楚究竟是什么问题.有关如何解决该错误的任何线索？
我在理解 Coq 中强规范和弱规范之间的区别时遇到了一些麻烦。例如，如果我想使用强规范方式编写复制函数（给定一个数字 n 和一个值 x，它会创建一个长度为 n 的列表，其中所有元素都等于 x），我将如何做到这一点? 显然我必须编写函数的归纳“版本”，但如何编写？
Haskell 中的定义：
myReplicate :: Int -> a -> [a]
myReplicate 0 _ = []
myReplicate n x | n > 0 = x:myReplicate (n-1) x
| otherwise = []
弱规范的定义：
用弱规范定义这些函数，然后添加伴随引理。例如，我们定义一个函数 f : A->B 并证明形式为 ? x:A, Rx ( fx )，其中 R 是对函数的预期输入/输出行为进行编码的关系。
强规范的定义：
给出函数的强规范：该函数的类型直接声明输入是类型 A 的值 x，输出是类型 B 的值 v 和 v 满足Rxv的证明的组合。这种规范通常依赖于依赖类型。
编辑：我收到老师的回复，显然我必须做类似的事情，但对于复制案例：
“例如，如果我们想从其规范中提取一个计算列表长度的函数，我们可以定义一个关系 RelLength，该关系建立预期输入和输出之间的关系，然后证明它。像这样：
Inductive RelLength (A:Type) : nat …当我查看 QuickChick 项目时，遇到了这句话“Require Import Ltac.我不知道这是做什么的以及Ltac模块在哪里”。我找到了一个文件plugins/ltac/Ltac.v，但这不可能是这个文件，因为该文件是空的（顺便说一句，包含空文件的目的是什么？）。我尝试过Locate Ltac.，但得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更令人困惑。
该模块的作用是什么Ltac，文件在哪里Ltac.v，为什么该Loacte命令在这种情况下不起作用？谢谢！
我是 Coq 的初学者，我很快就学会了这门语言，可以做证明等。
但我不明白我们能用这个做什么。好吧，我们证明了一些定义等。但是我们可以通过哪些方式使用它们呢？我看到我们可以提取 Haskell 文件，但我也不明白。
因为我想用语言来证明例如CVE 。