Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
有没有一种轻量级的方法来定义一个可变字典，可以在 Coq 中返回它的所有键？
我想定义一个可变字典，它可以返回其域中的所有键。钥匙不必订购。我在互联网上搜索了 coq 库文档，似乎没有找到任何东西
刚从 Coq 开始，尝试编写一个列表插入函数，该函数将返回新列表，或者如果提供的索引不合法，则使用 sumor 进行证明。我对递归没问题......
我正在编写一个玩具语言的编译器及其证明，并且我有文件 L1、L2、C 和 P，其中 L1 和 L2 包含语言 l1 和 l2、C 包含的抽象语法和操作语义。 ..
如何证明 coq 中的定理：(x | a) -> (x | b) -> x <= (gcd a b)?
我对最大公约数有这样的认识： 定点 gcd_ (m n d : nat) : nat := 将 d 与 | 0 => if (m =? 0) then n else m | S k => if (m mod S k =? 0) && (n mod S k =? 0)...
看起来依赖类型语言并不是图灵完备的。为什么我们不能允许每个函数都具有通用递归（这将使语言图灵完整）？ 有什么东西
例如： Agda：https://en.wikipedia.org/wiki/Agda_(programming_language)#:~:text=Agda%20is%20a%20total%20语言，可能%20to%20证明%20任意%20语句 Coq：有什么实用的
根据 coq 手册，unfold 策略对定义执行 delta 缩减，然后进行其他几个缩减，包括 beta 缩减。 似乎有时，要触发β-红...
例如Agda和Coq。 与 Idris2 和 Fstar 相比。 另外，诸如 Agda 之类的依赖类型编程语言不是图灵完备的，是否存在实际缺点，或者它是……
sig 类型定义如下： 归纳 A：集合 := mkA : nat-> A。 函数 getId (a: A) : nat := 将 a 与 mkA n => n 匹配。 函数过滤器 (a: A) : bool := if (beq_nat (getId a) 0) then ...
假设我有 A、B、C、D、E、F 类型。 A 的构造函数之一采用 F 类型的参数； B 的构造函数需要 A，D 的构造函数需要 C 和 A 类型的参数，E 需要 D 和 F
我需要在 Coq 中证明一个关于具有某些属性的连通图的引理： 图的顶点是 V:Type 类型，并且有一个函数 f: V -> nat 关联一个自然麻木...
错误：找不到绑定到逻辑路径 Strand 的物理路径。在coq
我有 coq 文件，并且已经处理了好几天，但现在该文件给了我以下错误： 错误：找不到绑定到逻辑路径 Strand 的物理路径。 所需的包如下：
如何证明对于所有 n m, n <= m -> m <= n -> n = m
定理 le_trans: forall n m o, n <= m -> m <= o -> n <= o. Proof. intros n m o Lnm Lmo. generalize dependent Lnm. generalize dependent n. induction Lmo. -intros. apply Lnm. -intros....
是否有`(A -> B \/ C) -> (A -> B) \/ (A -> C)`的直觉证明？
以下是经典命题逻辑中的一个有用的引理。 (A -> B \/ C) <-> (A -> B) \/ (A -> C)。 向后的方向很容易证明。但我找不到直观的...
我在理解依赖类型的模式匹配方面遇到了麻烦。假设我们有以下代码： 变体 Op := op1 |操作2。 变体 Res : Op -> Set := | r1：Res op1 | r2：Res op2 |...
定理 fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (bb' : bool), 长度 f = n /\ n > 0 /\ r < n /\ h = firstn r f /\ h' = (app h ((nth r f 0)::nil)) /\ r' = ...
InteractionTrees 库 - ASM 上的简单程序
我正在尝试在本教程中的 ASM（一种简单的控制流图语言）上编写简单的程序： 交互树 -> ASM.v 我的最终目标是使用图书馆的
我不知道在什么情况下我应该使用定理而不是引理或相反。这之间有什么区别（语法除外） 定理l：2 = 2。 琐碎的。 问。 和这个 引理 l : 2 ...