问题标签 [proof]

我有一个场景，我想证明一个引理，包括许多字符串和列表变量。可能，它需要“归纳”，但任何人都可以帮助我证明下面给出的引理。如果需要其余代码，我也可以提供。

试图证明元素插入函数到 bst 中的正确性，我被困在试图证明一个看似微不足道的引理中。到目前为止我的尝试：

显然，如果树中的所有内容都小于n并且n <= m所有内容都小于m，但我似乎无法让 coq 相信我。我该如何继续？

是否对任何假设的硬件 + 操作系统架构或整体软件设计进行了任何工作，这些工作可证明是不可能破解的？换句话说，一种只允许有限代码执行的架构，这样在“利用”的某些特定数学定义中，利用根本不可行。因此，漏洞利用在此框架下可能造成的潜在损害将被证明是有限的。

一般来说，我正在寻找基于一些合理的基本假设的“可破解”与“不可破解”架构的数学动机理论。

我可以清楚地看到 N^2 以 c2^N 为界，但是我如何通过使用 big-O 的正式定义来证明它。我可以简单地用 MI 来证明

这是我的尝试.. 根据定义，对于任何 n>n0，存在一个常数 C，其中 f(n) <= Cg(n) 其中 f(n) = n^2 和 g(n) = 2^n

我应该把日志带到两边并解决C吗？

还有一个关于斐波那契数列的问题，我想解决递归关系。

方程是..

还有一个

然后我开始迷路以形成一般方程 i 模式有点像帕斯卡三角形？

我一直在阅读有关随机数及其生成器的各种文章。我通常会从中得出 3 个重要的结论：

• 随机数并不是真正随机的
• 很多时候他们有偏差（模偏差）
• 当人类试图“随机行动”时，他们无法成为随机数生成器

因此，考虑到这些观察结果中的后者，我们将如何能够

1. 判断我们看到的一系列数字是否真的是随机的，更重要的是
2. 有什么方法可以证明所说的序列真的是随机的吗？

我的证明脚本给了我愚蠢的类型等式，比如nat = bool我 nat = list unit需要用来解决相互矛盾的目标。

在正常的数学中，这将是微不足道的。给定集合bool := { true, false }， nat := { 0, 1, 2, ... }我知道true ∈ bool，但是true ∉ nat，因此bool ≠ nat。在 Coq 中，我什至不知道如何表述true :̸ nat。

问题

有没有办法证明这些等式是错误的？或者，这不可能吗？

（Ed.：删除了一长串失败的尝试，仍然可以在历史记录中查看。）

It is a common programmer hobby to write programs which accomplish a task in 1 line of source code. But that is a bit trivial: I can take 1 000 000 lines of code, delete all the line breaks, and voila! 1 line!

So to make things interesting, we can count statements. For a C-style language, a simple of way of counting statements is counting semicolons: So nesting a million if-elses is fine.

Say you've got a program P with n statements. It goes through a sequence of states (variable values) s (where s is a vector) and produces output x. We can pose two questions:

1. Can a program with fewer than n statements produce output x?
2. Can a program with fewer than n statements go through some subset of s?

Immediately, some things become obvious. Take the following program:

We can refactor (or should I say "defactor") this into a one liner:

Can every program be defactored to one line? Take this program:

It's a bit more challenging.

The question can be answered exhaustively by trying every possible program with less than n statements, a number which is finite (theoretically you could have constants with infinitely many possible values, but no real language has infinite memory to store them or infinite disk space to accommodate the source code).

However:

A. Is it possible to prove for a program P which produces x (perhaps through s) with n statements that no Q which can do it in m statements can be found (in an efficient manner)?

B. Can the minimum n be found (in an efficient manner)?

C. Is minimum n guaranteed to be 1?

You can assume any language you want, although real languages would be more interesting. Please provide a definition of a "statement" in your language if your language is unusual.

I have assumed imperative languages, but adaptations of the problem to functional languages are welcome.

There is a trivial solution: For any P, run P and record x. Now write a program Q which simply prints x. For programs with input, make a very long if-else with each input mapped to a correct output.

This solution is unsatisfactory, although I'm not entirely sure why. Firstly, for infinite possible inputs it's impossible (but I already covered my ass by saying real programs are finite, so we can say real input is finite). Second, it only technically passes through a subset of s: Namely the empty set. Third, it's really anticlimactic.

Any help with defining away this little clever trick is also appreciated.

PS: For whatever my word is worth, this isn't homework. I simply got curious about the problem and tried to phrase it as clearly as I could. Of course, I would still say that if it was homework, so...

我有一个面试问题，我似乎无法弄清楚。给定一个大小为 N 的数组，找到大小为 k 的子集，使得子集中的元素彼此相距最远。换句话说，最大化元素之间的最小成对距离。

蛮力方法需要找到所有大小为 k 的子集，这在运行时是指数级的。

我的一个想法是从数组中均匀地获取值。我的意思是

1. 取第一个和最后一个元素
2. 找出它们之间的差异（在本例中为 10-1）并将其除以 k ((10-1)/3=3)
3. 从两端向内移动 2 个指针，从您之前的选择中挑选出 +/- 3 的元素。所以在这种情况下，你从 1 和 10 开始，找到最接近 4 和 7 的元素。那就是 6。

这是基于元素应该尽可能均匀分布的直觉。我不知道如何证明它有效/无效。如果有人知道如何或有更好的算法，请分享。谢谢！

在之前的问题中，我展示了（希望是正确的）这f(n) = O(g(n))意味着lg(f(n)) = O(lg(g(n)))有充分的条件（例如lg(g(n)) >= 1, f(n) >= 1， 和足够大的 n）。

现在，我需要证明或反驳这f(n) = O(g(n))意味着2^(f(n)) = O(2^g(n)))。直观地说，这是有道理的，所以我想我可以借助前面的定理来证明它。我注意到f(n)可以重写为just lg(2^f(n))，这让我很兴奋......这是我想要证明的双方的 log base 2，它简化了很多事情！g(n)lg(2^g(n))

但我很确定这行不通。仅仅因为lg(2^f(n)) = O(lg(2^g(n)))并不一定意味着2^f(n) = O(2^g(n))……这与前面的定理相反（它说“暗示”，而不是“当且仅当”）。

我是否需要以另一种方式尝试这个证明，或者我真的可以放弃我所拥有的（至少作为首发）？

**说到其他方式，也许我可以争论如何将 2 提高到g(n)“高于”的一些f(n)仍然会保持更高？这几乎感觉像是一个常识性的论点，但也许我错过了一些重要的东西..

**哦，哎呀！我忘了添加，f(n)并且g(n)是渐近积极的。根据我们的教科书定义，这意味着它们“对于所有足够大的 n 都是正的”。

问题：

(5n^2)(ln(n)) 是 n(ln(n)^2) 的大欧米茄

我试过的：

存在 c > 0, n0 > 0

(5n^2)(ln(n)) >= cn(ln(n)^2) 对于所有 n >= n0

(5n^2)(ln(n)) >= n(ln(n)) (对于 n >= 1) >= n(ln(n)^2) (对于 n <= 1)

因此得出结论，当 n = 1 = n0 时，(5n^2)(ln(n)) 是 n(ln(n)^2) 的大欧米伽；但这不符合（对于所有 n >= n0）的要求。

我被困在这里，有人可以帮忙吗？