标签: induction

我正在尝试使用Induction连接到我的本地SQLite数据库,但是我不知道如何建立连接.在以前的SQLite客户端中,我只是打开了数据库文件.

我应该将哪些属性放入这些领域？我的数据库简单development.db而且位于我的Rails应用程序中

我真的试图围绕递归的工作原理并理解递归算法.例如,当我输入5时,下面的代码返回120,原谅我的无知,我只是没有看到原因？

def fact(n):
    if n == 0:
        return 1
    else:
        return n * fact(n-1)

answer = int (raw_input('Enter some number: '))

print fact(answer)

基于比较的排序是nlog(n)的大o,因此我们知道mergesort不能是O(n).不过,我无法通过以下证据找到问题:

命题P(n):对于长度为n的列表,mergesort需要O(n)时间.

P(0):空列表上的合并排序只返回空列表.

强诱导:假设P(1),...,P(n-1)并试图证明P(n).我们知道在递归mergesort的每一步,两个大约"半列表"被合并,然后"压缩".每个半列表的合并排序通过归纳获得O(n/2)时间.拉紧需要O(n)时间.因此该算法具有M(n)= 2M(n/2)+ O(n)的递归关系,其为2O(n/2)+ O(n),其为O(n).

我是新的coq,我真的很难应用感应.只要我可以使用图书馆的定理,或者像欧米茄这样的策略,这一切都"不是问题".但是一旦这些不起作用,我就会被困住.

确切地说,现在我试图证明

Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m.

案件n = 0我已经有了.

Proof.
    intros. destruct H as [H1 H2 ]. induction n.
      rewrite Nat.mod_0_l by omega. rewrite Nat.mod_0_l; omega.

但是如何制作诱导步骤呢？

1 subgoal
n : nat
m : nat
H1 : S n >= m
H2 : m <> 0
IHn : n >= m -> (n - m) mod m = n mod m …

我已经能够创建一个证明,表明树中的最大总节点数等于n = 2 ^(h + 1) - 1,逻辑上我知道二叉树的高度是log n(可以绘制它出去看)但是我在构建一个正式的证据时遇到了麻烦,这个证据表明一棵有n片叶子的树至少有"log".我遇到或能够组合的每个证据总是处理完美的二叉树,但我需要适合任何情况的东西.有什么提示可以引导我朝着正确的方向前进

当在纸上推理时,我经常通过归纳使用一些列表的长度.我想在Coq中形式化这些参数,但似乎没有任何内置的方法来对列表的长度进行归纳.

我该如何进行这样的归纳？

更具体地说,我试图证明这个定理.在纸面上,我通过归纳证明了它的长度w.我的目标是在Coq中形式化这个证明.

基本上,我想证明以下结果:

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.

这就是所谓的双重归纳的复发方案.

我试图证明它应用感应两次,但我不确定我会以这种方式得到它.实际上,我在那时陷入困境:

Proof.
  intros. elim n.
    exact H.
    intros. elim n0.
      exact H0.
      intros. apply (H1 n1).

Morte旨在作为超级优化功能程序的中间语言.为了保持强规范化,它没有直接递归,因此,诸如列表之类的归纳类型表示为折叠,而诸如无限列表之类的导电类型表示为流:

finiteList :: List Int
finiteList = \cons nil -> cons 0 (cons 1 (cons 2 nil))

infiniteList :: Stream Int
infiniteList = Stream 0 (\n -> (n, n + 1))

我想enumFromTo在Morte 上重写Haskell ,所以:

enumFromTo 0 2

归一化为:

\cons nil ? cons 0 (cons 1 (cons 2 nil))

那可能吗？

我需要证明以下选择排序代码（在Haskell中）始终在排序：

import Data.List (minimum, delete)

ssort :: Ord t => [t] -> [t]
ssort [] = []
ssort xs = let { x = minimum xs } in  x : ssort (delete x xs)

我们可以假设我们有一个名为“ sorted ” 的函数，该函数检查列表何时排序。

用结构归纳法证明的语句：sorted（ssort xs）

我尝试了以下操作，但无法完成证明。您能帮我完成证明吗？

基本情况：xs = []

sorted（ssort xs）=

sorted（ssort []]）=

排序（[]]

正确，因为sorted（[]）总是被排序

归纳步骤

IH（归纳假设）=排序（ssort xs）

显示：排序（排序y＃xs）

情况I：x = y =最小值

sorted（sort y＃xs）=

sorted（let {x = x中的最小值（y＃xs）}：ssort（删除x（y＃xs）））=（根据定义）

sorted（let {y = y中的最小值（y＃xs）}：ssort（删除y（y＃xs）））=（通过替换）

sorted（y：ssort（删除y（y＃xs）））=

sorted（y：ssort（xs））=（按删除定义）

排序（y：ssort（xs））

通过IH，我们知道sort（xs）已排序，y也是最小值，因此它排在第一位

情况二：y不是最小值

sorted（sort y＃xs）=

sorted（let {x …

我是一所大学的讲师，参加一门名为“ 类型系统的语言 ” 的课程，在最后一次讲解中，该教授将以下示例用于类型理论的归纳证明：

假设存在归纳定义的自然数（出于某种原因，他坚持称其为术语），而我们在它们上递归定义了一个大于函数。我们可以证明，对于每一个n，它都拥有（suc n> n）。

我准备了以下Coq代码以在类中实现此代码：

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = …