有没有一种方法来证明关于我的C++程序的属性？
我了解像Coq和Idris这样的语言可以用来证明使用这些语言编写的程序的属性（根据我在该课题上的少量经验。），但我想知道是否存在一种可行的方法，可以对已有的代码库进行外部验证。 是否有一种方法可以使用像Coq这样的工具或其他专业工具来证明用C++编写的算法的正确性？如果有，那么需要满足哪些要求？
如何在Coq中复制一个假设？
在一个证明过程中，我遇到了一个假设H。我的引理是：H -> A和H -> B。 我该如何重复利用假设H来推导出两个假设A和B？ 编辑后：lemma l1: X -> A. lemma l2: X -> B. 1 subgoals, subgoal 1 (ID: 4...
为什么基于建筑计算的语言会如此频繁地使用Setoids？
我们发现Setoid在Agda、Coq等语言中被广泛使用。实际上，像Lean这样的语言已经提出它们可以帮助避免“Setoid Hell”的问题。为什么首先要使用Setoid呢？转向基于HoTT的外延类型理论（如立方Agda），是否减少了对Setoid的需求？
在Coq中，程序的Fixpoint和Function有什么区别？
它们似乎具有类似的目的。到目前为止我注意到的唯一区别是，虽然 Program Fixpoint 可以接受类似于 {measure (length l1 + length l2) } 的组合度量，但是 Function 会拒绝这样做，只允许 {measure length l1}。 Progr...
我该如何在Coq中显式地提供隐式参数？
假设我有一个定义 f : x -> y -> z，其中x可以很容易地推断出来。因此，我选择使用Arguments使x成为一个隐式参数。 考虑以下例子：Definition id : forall (S : Set), S -> S := fun S s => s. ...
为什么要在Coq中公理化实数？
我在想Coq是将实数定义为Cauchy序列还是Dedekind划分，因此我检查了Coq.Reals.Raxioms，但…没有这两个。实数是公理化的，连同它们的运算（作为Parameter和Axiom）。为什么会这样？ 此外，实数严重依赖于子集的概念，因为它们的一个定义性质是每个上界有一个最小...
Coq简化程序修复点
有没有类似于策略simpl用于程序不动点的东西？ 特别地，如何证明以下平凡语句？ Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n' => S (bla n') end. Lemma...
证明 f (f bool) = bool。
在Coq中，我如何证明一个接受布尔值 true|false 并返回布尔值 true|false 的函数 f（如下所示），在将其应用两次于单个布尔值 true|false 时，总是返回相同的值 true|false：(f:bool -> bool) 例如函数f只能做四件事情，我们称函数的输...
将Coq转换为Idris
如何将Coq源代码转换为Idris代码，有哪些有用的指导方针（例如它们的类型系统有多相似，如何翻译证明等）？据我所知，Idris的内置策略库很少但可扩展，因此我想这应该是可能的，只需进行一些额外的工作。