标签: proof

我正试图在Project Euler上解决问题50 .不要给我答案或为我解决,只是试着回答这个具体问题.

目标是找到连续素数的最长和,这些素数会增加到低于一百万的素数.我写了一个筛子来找到n下面的所有素数,我已经确认它是正确的.接下来,我将使用以下方法检查连续素数的每个子集的总和:

我有一个空列表sums.对于每个素数,我将它添加到每个元素中sums并检查新的总和,然后我将素数追加到sums.

这是在python中

primes = allPrimesBelow(1000000)
sums = []
for p in primes:
    for i in range(len(sums)):
        sums[i] += p
        check(sums[i])
    sums.append(p)

我想知道我是否已经要求check()两个或更多连续素数的总和低于一百万

问题是有一个素数,953,可以写成21个连续素数的总和,但我找不到它.

我该如何证明n!任何常数自然数p不在O(n ^ p)中？并且(nk)(n选择k)在O(n ^ p)中,对于所有k？

我很难证明斐波那契的"坏"版本是O(2 ^ n).IE浏览器.鉴于功能

int fib(int x)
{
  if ( x == 1 || x == 2 )
  {
    return 1;
  }
  else
  {
    return ( f( x - 1 ) + f( x - 2) );
  }
}

我可以得到帮助证明这是O(2 ^ n).

我正在阅读软件基础书.在关于多态的章节中,有一节关于"隐式参数".在本节中,有一行:

Arguments nil {X}.

当我尝试在Poly.v文件上运行Coq (该章节的源代码,在此tarball中可用)时,它停在上面的行,给我错误:

Error: No focused proof (No proof-editing in progress).

我已将Poly.v文件缩减为这些内容,这仍然会给出相同的错误:

Inductive list (X:Type) : Type :=
  | nil : list X.

Arguments nil {X}.

我在Coq参考手册中找到的关于此错误的唯一内容是

当人们试图在校对编辑模式之外使用校对编辑命令时,Coq会引发错误消息:没有聚焦证据.

我认为"证明编辑模式"是指使用策略证明定理的上下文.我不认为它是在那种模式,也不是Coq,因为它说"没有正在进行的校对编辑".这是有道理的.

该错误声称这Arguments是一个"证明编辑命令",虽然它没有在其文档中说明,并且在证明处理章节中Arguments没有提到.

这让我觉得Coq错误地将其Arguments视为校对编辑命令,但我不知道为什么.

我认为这对我的设置而不是Poly.v文件本身来说是错误的,因为它是Software Foundations一书的一部分.我正在使用CoqIDE,作为Coq 8.3pl4的一部分,与Ubuntu 12.04一起发布.

为什么所有NP问题都可以在O(2 ^(n ^ k))中解决,也就是说EXPTIME？

其中n ^ k是输入大小为n的多项式函数,并且可以取决于问题的大小.(k> = 0)

我试图证明一个引理,它在某个部分有一个错误的假设.在Coq,我曾经写过"一致",它会摆脱目标.但是,我不知道如何继续Isabelle Isar.我试图证明我的le功能的一个引理:

primrec le::"nat ? nat ? bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ? False | Suc j ? le k j)"

lemma def_le: "le a b = True ? (?k. a + k = b)"
proof
  assume H:"le a b = True"
  show "?k. a + k = b"
  proof (induct a)
    case 0
    show "?k. 0 + k = b"
    proof -
      have "0 + …

我遇到了问题:

f(n) are asymptotically positive functions. Prove f(n) = ?(g(n)) iff g(n) = ?(f(n)). 

我发现的一切都表明这个陈述是无效的.例如,我遇到的答案是:

f(n) = O(g(n)) implies g(n) = O(f(n))
f(n) = O(g(n)) means g(n) grows faster than f(n). It cannot imply that f(n) grows
faster than g(n). Hence not true.

另一个州:

 If f(n) = O(g(n)) then O(f(n)). This is false. If f(n) = 1 and g(n) = n 
 for all natural numbers n, then f(n) <= g(n) for all natural numbers n, so
 f(n) = O(g(n)). However, …

data Nat = Zero | Succ Nat
type Predicate = (Nat -> Bool)

-- forAllNat p = (p n) for every finite defined n :: Nat

implies :: Bool -> Bool -> Bool
implies p q = (not p) || q 

basecase :: Predicate -> Bool
basecase p = p Zero 

jump :: Predicate -> Predicate
jump p n = implies (p n) (p (Succ n)) 

indstep :: Predicate -> Bool
indstep p = forallnat (jump p) 

题:

证明如果basecase …

我们有一个函数，可以将元素插入列表的特定索引中。

Fixpoint inject_into {A} (x : A) (l : list A) (n : nat) : option (list A) :=
  match n, l with
    | 0, _        => Some (x :: l)
    | S k, []     => None
    | S k, h :: t => let kwa := inject_into x t k
                     in match kwa with
                          | None => None
                          | Some l' => Some (h :: l')
                        end
  end.

上述功能的下列性质是相关的对问题（证明省略，对直接的感应l与n未固定的）：

Theorem inject_correct_index : forall A x …

我试图通过查看一些软件基础练习(最初用于Coq,但我希望对Idris的翻译不太糟糕)来提高我的Idris技能.我在"练习:1星(plus_id_exercise)"中遇到问题,其中包括:

删除"已录取".并填写证明.

Theorem plus_id_exercise : ? n m o : nat,
  n = m ? m = o ? n + m = m + o.
Proof.
  (* FILL IN HERE *) Admitted.

Run Code Online (Sandbox Code Playgroud)

我在Idris中翻译成以下问题:

plusIdExercise : (n : Nat) ->
                 (m : Nat) ->
                 (o : Nat) ->
                 (n == m) = True ->
                 (m == o) = True ->
                 (n + m == m + o) = True

我正在尝试逐个案例分析,我遇到了很多问题.第一种情况:

plusIdExercise Z Z Z n_eq_m n_eq_o …