Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我有一个定义如下的图表。 定义 ldd_state ：类型 := gmap loc (nat * (loc * loc))。 这是从 loc（正数）到值 nat 和两个子项的映射。每个节点都“活着”...
我得到了 com 的以下定义，它可以在单个命令中将新值分配给多个变量： 感应式 com : 类型 := |跳过 | CAsgn (xs : 列表字符串) (es : 列表 aexp) (* ...
我对 coq 比较陌生，我不知道如何继续。 我想为列表库的 In Fixpoint 编写一个可判定性函数，如下所示： 程序定点 InDec (s : K) (l : 列表...
如何证明nat_to_bin结合了bin_to_nat b = Coq中标准化b
我是新手，用参考书软件基础入门学习Coq 在这句话的最后部分，有一个练习证明 将二进制更改为自然数并且
在 Coq 中，作为一个简化的例子（使用 False 忽略结论）， 定理例子 (f : nat -> 布尔) (g : 布尔 -> 布尔 -> 布尔) (cmplx:= 让 a := f 0 进入 让...
我因 IH 结构不完善而遇到麻烦（或者我犯了错误）。 从 stdpp 需要导入地图集。 从 stdpp 需要导入 gmap。 从 stdpp 需要导入选项。 从 stdpp 需要导入
我正在尝试证明以下引理。 感应布尔：类型：= |真的 |错误的。 引理 andb_true_iff : forall b1 b2 : bool, b1 && b2 = true <-> b1 = true // b2 = true。 证明。
我正在尝试证明对立性。我的证明如下。这不起作用。 定理反证：forall (P Q : Prop), (P -> Q) -> (~Q -> ~P)。 证明。 介绍。 摧毁H...
我已经有了一个定理 定理 plus_id_example : forall n m:nat, n = 米 -> n + n = m + m。 我想证明它的“逆形式”。所以我有 定理 plus_n_n_injective ：对于所有 n ...
如何申请（S n' <=? m) = true to S n' <= m?
试图完成 Coq 证明，但我最终陷入了最后一个目标。我把目标变成了S n' <= m and have a hypothesis (S n' <=? m) = true, but am unable to unify these. I tr...
我有两个函数 build_goal_aux 和 last 定义如下： 定点 build_goal_aux (acc:list nat)(n:nat) : list nat := 匹配 n 与 | O => ACC | S n' => build_goal_aux (n::acc) n' ...
引理 x: forall P Q: Set -> Prop, forall f：设置->设置， 对于所有 x，(P x -> Q (f x)) -> （存在x，P x）->（存在x，Q x）。 我尝试去做...
软件基础（lf）：证明leb_plus_exists和plus_leb_exists
我一直在学习《软件基础》第一卷，但我无法通过 Logic.v 中的一对可选问题。有人知道该怎么做吗？ 定理 leb_plus_exists ：对于所有 n m, n &l...
我注意到，在 Coq 的有理数定义中，零的倒数被定义为零。 （通常，除以零是没有明确定义/合法/允许的。） 需要导入 QArith。 引理 inv_zero_is_zer...
Coq/Ltac：是否可以设计一种策略，在决策程序证明目标时证明目标已被证明，而无需证明项？
我正在设计一种 Coq 策略，它调用一个决策过程，该过程回答是/否，而不给出证明术语。当我回答“是”时，我想说 Ltac 目标已得到证明。 有没有办法...
我正在尝试在 Coq 中实现一个索引函数。我写了这段代码： 表示法 grid := (list nat)。 定点index_aux (n : nat) (g : grid) (i : nat) : 选项 nat := 将 g 与 | [] =>...
引理 x: forall P Q: Set -> Prop, forall f：设置->设置， 对于所有 x，(P x -> Q (f x)) -> （存在x，P x）->（存在x，Q x）。 我尝试去做...
为什么 coq 无法识别 `None = Some v` 是 false？
我有一个功能： 定点评估 (fuel : nat) (env : 环境) (e : exp) := 匹配燃料 | 0 => 无 | S 燃料' => (...) 结尾 我现在正在证明这种函数的属性......
使用以下 Coq 代码： 搜索“prod_uncurry_subdef”。 需要导入算术。 搜索“prod_uncurry_subdef”。 打印出以下内容： prod_uncurry_subdef: forall [A B C : T...