如何在Agda中实现Floyd的乌龟兔子算法？
我想将以下Haskell代码翻译成Agda： import Control.Arrow (first) import Control.Monad (join) safeTail :: [a] -> [a] safeTail [] = [] safeTail (_:xs) = ...
证明继承者在相等性质上的替换性质
我是一名有用的助手，可以翻译文本。 我正在尝试从《Lean定理证明》第7章中了解归纳类型。 我设定了一个任务，即证明自然数的后继在等式上具有替换属性。 inductive natural : Type | zero : natural | succ : natural -> nat...
“arith”和“presburger”在Isabelle中有什么区别？
到目前为止，我在Isabelle中遇到的所有使用 arith 可以解决的目标也可以通过 presburger 解决，反之亦然，例如： lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n" by presburger (* or arith *) 这...
如何在Isabelle中搜索常规定义、定理、函数等内容的最佳方法？
我正在尝试阅读Isabelle（定理证明器）的Isar章节，第一个语句如下： lemma "¬ surj(f :: 'a ⇒ 'a set)" 我想了解常数surj是什么。我知道可以使用以下方法查找相关定理： thm notI 显示的内容为： (?P ⟹ False) ⟹ ¬ ?...
在Idris中苦恼重写策略
我正在学习陶哲轩的实分析教材，该教材从自然数开始构建基本的数学概念。通过尽可能多地形式化证明，我希望熟悉Idris和依赖类型。 我定义了如下数据类型： data GE: Nat -> Nat -> Type where Ge : (n: Nat) -> (m: N...
我如何仅对一个术语应用重写？
在精益中，我偶尔希望将“rw”策略应用于多个相同项中的一个。例如，我有以下目标： ⊢ 0 = 0 我想要对它进行读写 ⊢ a * 0 = 0 我也有 mul_zero (a : mynat) : a * 0 = 0 现在我应该能够将0重写为a * 0。然而，尝试这样做会导...
具有结合和交换操作符的模式匹配
模式匹配（如Prolog、ML家族语言和各种专家系统外壳中所发现的）通常通过按严格顺序逐个地将查询与数据元素进行匹配来运作。 然而，在自动定理证明等领域中，有一种要求需要考虑到某些运算符是可交换和结合的。假设我们有以下数据： A or B or C and查询 C or $X 根...
在Isabelle中同时使用Nitpick和Sledgehammer
当我在Isabelle中声明引理时，我通常会输入nitpick，如果这不能给我一个反例，那么我会输入sledgehammer来尝试自动找到证明。 我想知道：是否可能调用Nitpick和Sledgehammer以便它们同时运行？既然Sledgehammer已经将我的引理发送给许多自动证明器，难...
Idris中的自定义证明策略
如果我理解得正确（主要是从 applyTactic 函数的存在推断），在 Idris 证明器中编写自定义策略是可能的。有哪些例子可以用来学习如何实现这一点呢？
在Z3中打印内部求解器公式
定理证明工具z3花费了很长时间来解决一个公式，我认为它应该轻松处理。为了更好地理解并可能优化我的输入到z3，我想看到z3作为其求解过程的一部分生成的内部约束。当使用命令行从z3时，如何打印z3为其后端求解器生成的公式？