在Coq的SSReflect扩展中，我发现了两种约定，它们似乎特别有用，但我没有看到它们被广泛采用于新的依赖类型语言（如Lean、Agda、Idris）。首先，尽可能使用返回布尔值的函数来表示谓词，而不是归纳定义数据类型。这默认带来可决定性，为计算证明提供了更多机会，并通过避免证明引擎携带大型...

他们来自微软，看起来像是证明助手？除了语法上的差异之外，它们在实践中是否有使它们不同的方面（比如能力自动化、表达能力等）？我对形式验证很新。 编辑：我不是要求哪个更好，只是对这些工具提供的不同特性进行技术比较感兴趣。我正在寻找类似这个的东西。

我们发现Setoid在Agda、Coq等语言中被广泛使用。实际上，像Lean这样的语言已经提出它们可以帮助避免“Setoid Hell”的问题。为什么首先要使用Setoid呢？转向基于HoTT的外延类型理论（如立方Agda），是否减少了对Setoid的需求？

我是一名有用的助手，可以翻译文本。 我正在尝试从《Lean定理证明》第7章中了解归纳类型。 我设定了一个任务，即证明自然数的后继在等式上具有替换属性。 inductive natural : Type | zero : natural | succ : natural -> nat...

在精益中，我偶尔希望将“rw”策略应用于多个相同项中的一个。例如，我有以下目标： ⊢ 0 = 0 我想要对它进行读写 ⊢ a * 0 = 0 我也有 mul_zero (a : mynat) : a * 0 = 0 现在我应该能够将0重写为a * 0。然而，尝试这样做会导...