coq

2热度

1回答

我使用frama-C WP并希望调试我的ACSL注释（了解为什么证明者说我“不知道”）。我有一些绿色或橙色的结果。我打开why3 IDE并查看生成的脚本。然后我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代码。我看到一些公理定理，然后WP 然后，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t

3热度

2回答

检查evars的策略，返回一个值

我试图写一个策略，返回一个值，并在这样做的过程中，它需要检查是否是一个evar。不幸的是，我不能使用is_evar，因为那时策略不被视为返回一个值（而是另一种策略）。下面是一个例子。有什么建议吗？ Ltac reify_wrt values ls := match ls with | nil => constr:(@nil nat) | ?a :: ?ls' =>

2热度

2回答

替换术语的应用证明

我想证明在术语上应用空替换等于给定术语。下面是代码： Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Arith.EqNat. Require Import Recdef. Require Import Omega. Import ListNotations. S

2热度

1回答

为什么后面的Coq重写不适用于假设的右侧？

我有以下Coq env。 1 subgoals m : nat IHm : forall n : nat, n + n = m + m -> n = m n : nat H : S (n + S n) = S (m + S m) ll := ll : forall k : nat, k + S k = S k + k 做rewrite ll in H，只改变了LHS S (n + S

1热度

2回答

证明如果同时运行2个脚本，则一般抱怨脚本不完整

似乎PG不允许同时运行2个脚本。在尝试这样做的那一刻，Emacs会提示并要求撤消另一个文件。有时候，脚本不会重新运行。有没有办法在单个Emacs实例中真正运行2个（或更多）脚本？我认为coqide gui没有coq没有这样的问题。

3热度

1回答

如何在Coq中导入库？

我想用&&作为中的andb的中缀形式。官方文档告诉我&&定义在Coq.Init.Datatypes模块中。我尝试这样做： Import Coq.Init.Datatypes. 不过勒柯克给出了错误： Unknown interpretation for notation "_ && _". 什么是包括在勒柯克标准库的正确方法是什么？

4热度

2回答

如何从外部软件呼叫proof asistant Coq

如何从外部软件呼叫证明助手Coq？ Coq是否有一些API？ Coq命令行界面是否足够丰富，可以在文件中传递参数并在文件中接收响应？我对Java或C++桥梁感兴趣。这是一个合法的问题。 Coq不是通常的商业软件，人们可以期望开发者友好的API。对于Isabelle/HOL我有类似的问题，这是一个非常重要的问题。

1热度

1回答

在Coq中，如何定义一个像A = {x |的集合f（x）= 0}？

我是使用Coq的新手。我想问一下，如果我想定义一组像 A = {x | f(x) = 0}，我怎么能做到这一点？我写的东西，如： Definition f0 := nat->nat. Definition A : Set := forall x, f0 x -> 0. 预期他们没有工作。非常感谢。

-2热度

2回答

coq我应该使用什么策略？答：Prop，A - > ~~ A

我不知道我必须使用什么策略来证明该模板。我尝试了两种方法，但我被困在了两个。 Lemma Exo17 : forall A : Prop, ~~(A \/ ~A). Proof. Methode 1 intro. unfold not. intro. Methode 2 intro. intro. case H.

2热度

1回答

Coq矛盾的假设

在Coq我有两个假设H和H0，这相互矛盾。问题是，他们只是为了一些专业而互相矛盾，在这个证明的背景下，情况并不那么专业化。这时我的证明背景是这样的： color : Vertex -> bool v : V_set a : A_set x0, x1 : Vertex H : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> c