proof

0热度

1回答

功能递归地查找并从具有整数元素 Min(A, b, e) if (b=e) return A[b] m = (b+e)/2 // floor is taken x = Min(A, b, m) y = Min(A, m +1, e) If(x < y) return x else return y 我的前提是一个阵列返回的最小元素：b和e为大于零的整数

3热度

2回答

解释为什么X = =〜（〜X + 1）+ 1（二进制补码和背部！）

我们都知道通常负数在内存中表示作为这样的 from x to ~x + 1 ，并获得二的补数回到我们不这样做明显的东西一样 ~([~x + 1] - 1) 而是我们做 ~[~x + 1] + 1 有人可以解释为什么它总是工作？我想我可以用1位，2位，3位数来证明它，然后使用数学归纳法，但它并不能帮助我理解它的工作原理。谢谢！

2热度

1回答

在Coq中定义间隔函数

我想在Coq中定义一个名为interval的函数，给定两个自然数计算这两个之间的所有自然数的列表。但是我的定义不是原始递归的。这里是我的代码：正如你所看到的，我正在使用有根据的递归关于间隔的长度。我将这个度量定义为这个值，即S n - m。我希望被要求证明forall m, n, true = m <= n -> S n - S m < S n - m 但是，我得到的证明义务并不像这一点，是相

2热度

1回答

不理解n个节点的具有高度h的递推公式在AVL树显示ħ<= 2为log N

我知道公式是：n(h) = n(h-1) + n(h-2) + 1 我知道它可以减少为： n(h) = n(h-1) + n(h-2) + 1 >= n(h-2) + n(h-2) + 1 >= 2n(h-2) + 1 >= 2n(h-2) 经过这一步后，我不明白会发生在这里的复发。我正在网上阅读证明，他们这样做： >= 2n(h-2) >= 2(2n(h-4)

3热度

1回答

终止意味着存在正常形式

我想证明终止意味着存在正常形式。这是我的定义： Section Forms. Require Import Classical_Prop. Require Import Classical_Pred_Type. Context {A : Type} Variable R : A -> A -> Prop. Definition Inverse (

3热度

1回答

证明逻辑操作利用推理规则

前提1：p ∧ q 前提2：q → r 前提3：s → ¬r 前提4：¬r → ¬u 前提5：t ∨ s 前提6：t → ¬p ∨ U 证明：u ∧ q 有谁知道如何解决使用推理规则证明了这一点？我知道推理的规则，如modus ponens/tollens，但我不确定如何在这里使用它们。我仍然开始学习这些类型的证明。任何人都可以告诉我如何完成此？谢谢。

1热度

1回答

勒柯克的测算风格的双条件链

我试图证明勒柯克一个双条件： P <-> Q 而且我写下了具有这种结构的证明： P <-> S <-> T <-> Q thus: P <-> Q 我怎么可以模仿这个的测算证明结构在Coq？预先感谢您。

0热度

1回答

证明Coq的nat的高斯定理

我想证明nat的高斯定理。在普通（非精确）语言，它说：如果a划分b*c和无的a的因素是在b那么它们必须全部在c。 Require Import NPeano. Theorem Gauss_nat: forall (a b c:nat), gcd a b = 1 -> (a | (b*c)) -> (a | c). 定理已经为整数Z定义，见here in the Coq manual。但我需

3热度

2回答

有目的的递归Coq

我想写一个函数来计算Coq中的自然分割，并且由于它不是结构递归，所以我在定义它时遇到了一些麻烦。我的代码是： Inductive N : Set := | O : N | S : N -> N. Inductive Bool : Set := | True : Bool | False : Bool. Fixpoint sum (m :N) (n

7热度

1回答

在idris中证明map id = id？

我刚开始玩idris和定理证明一般。我可以在互联网上查看大部分基本事实证明的例子，所以我想尝试我自己的任意东西。所以，我想要写一个证明长期在地图的以下基本属性： map : (a -> b) -> List a -> List b prf : map id = id 直觉，我能想象的证明应如何工作：取一个任意列表L和分析地图ID L中的可能性。当l空着时，很明显;当 l非空时，它基于函数应用