Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我具有以下证明状态：H：存在x：A，fx = y / \在xl中----------------------目标：存在x0： A，f x0 = y / \ In x0（x :: l）我知道In xl意味着In x（x :: l）。所以我想...
请考虑Coq中的以下命题：归纳subseq：list nat-> list nat-> Prop：= | nil_s：forall（l：列出nat），subseq nil l | cons_in l1 l2 x（H：subseq l1 l2）：subseq（x :: ...
我想了解语法简介[| n]。在下面的证明中。引理zero_or_succ：forall n：nat，n = 0 \ / n = S（pred n）。证明。简介[| n]。 - 剩下。自反性。 - 对。自反性。 ...
我有一个类似Definition的代码，甚至：= {n：nat |存在k，n = k + k}。定义even_to_nat（e：even）：nat。承认了强制even_to_nat：偶数>-> nat。示例示例：forall n：偶数，...
以下代码给我一个错误：要求输入实数。需要导入列表。导入ListNotations。打开范围R_scope。定义C：=（R * R）％类型。定义RtoC（r：R）：C：=（r，0）。 ...
在Isabelle校对助手中，可以单击Ctrl +单击一个术语，IDE会将其重定向到相关定义。可以用CoqIde完成吗？有一般证明吗？
单项和史诗函数是同构的，因此具有反函数。我想在Coq中证明这一点。公理functional_extensionality：全部A B（f g：A-> B），（全部a，f a = g a）-> f = ...
我希望能够有一个异类的依赖对（T，f）序列，其中T在Set中，如果函数T是f-> bool，例如Definition classif：seq（forall T：Set，T- > bool）：= ...
[这就是我要证明的：定理add_n_injective：全部n m p，n + m = n + p-> m = p。加号（+）表示，如https：//softwarefoundations.cis.upenn.edu/lf-current / ...
我正在尝试从列表中删除所有大于7的整数，如下所示，过滤器（fun n => n> 7）。但是，我得到以下错误：术语“ n> 7”的类型为“ Prop”时...
我正在阅读Logical Foundation的书。它介绍了此Fixpoint和该定理：Fixpointoptimize_0plus（a：aexp）：aexp：=将a与|匹配。 APlus（ANum 0）e2 => optimize_0plus e2 | ...
在上次使用coq中的列表播放期间，我遇到了类型问题。但首先是定义；休闲列表：归纳列表（a：设置）：set：= | nil：列出一个|缺点：一个->列表一个->列表...
Coq具有战术语言Ltac和比赛设施等。 Isabelle / HOL是否具有一些用于战术的编程语言以及解析，模式匹配等服务？我浏览了...
我是Coq的新手。我有一个记录类型和一个定义：Record t：Type：= T {width：nat; }。定义缩进移位f：=将f与|匹配。 T w => T（w + shift）结束。我...
John Major的等式带有以下重写的引理：检查JMeq_ind_r。 （* JMeq_ind_r：forall（A：类型）（x：A）（P：A->支撑），P x-> forall y：A，JMeq y x-> ...
如何在Coq中证明以下内容？目标所有人（AB）：类型（A * A = B * B）％type-> A =B。如果无法证明，可以安全地将其作为公理添加吗？