标签: induction

请多多包涵。我将首先描述书中的一个例子，然后在最后提出我的问题。

根据编程语言范式的文本：

归纳指定是指定一组值的强大方法。为了说明这个方法，我们用它来描述 自然数 N = {0, 1, 2, ... . .} .

自上而下的定义：

一个自然数 n 在 S 中当且仅当

1. n = 0，或
2. ? 3 ? S。

我们知道 0 ? S. 因此 3 ? S，因为 (3 ? 3) = 0 和 0 ? S. 同样 6 ? S，因为 (6?3) = 3 和 3 ? S. 以这种方式继续，我们可以得出结论，所有 3 的倍数都在 S 中。

其他自然数呢？是 1 吗？? 我们知道 1 != 0，所以不满足第一个条件。此外，(1?3) = ?2，它不是自然数，因此不是 S 的成员。因此不满足第二个条件。

自下而上的定义：

定义集合 S 为包含在 N 中的最小集合，并满足以下两个性质：

1. 0 ? 沙 …

首先抱歉提出这样一个基本问题.

但是我很难理解用于解决复发的替代方法.我正在关注Algo.s-CLRS简介.由于我无法找到足够的例子和模糊性是主要关注点.尤其是归纳步骤.在教科书中我们必须证明f(n)意味着f(n + 1)但在CLRS中这一步骤缺失或可能是我没有得到这个例子.请逐步解释如何证明O(n ^ 2)是递归函数T(n)= T(n-1)+ n的解

它是我想要了解的替代方法的一般步骤.如果你能够对强大的数学归纳有所了解,并提供关于替代方法的材料的链接,这也会有所帮助.

按照亚瑟的建议,我改变了我的Fixpoint关系,Inductive建立了一种"建立"游戏之间不同比较而不是"向下钻取" 的相互关系.

但现在我收到一条全新的错误消息:

Error: Parameters should be syntactically the same for each inductive type.

我认为错误信息是说我需要所有这些互感定义的相同精确参数.

我意识到有一些简单的黑客来解决这个问题(未使用的虚拟变量,包含所有内容的长函数类型forall),但我不明白为什么我应该这样做.

有人可以解释这种对互感类型的限制背后的逻辑吗？是否有更优雅的方式来写这个？这种限制是否也意味着相互之间的归纳调用必须都使用相同的参数(在这种情况下,我不知道任何黑客可以保存大量的代码重复)？

(所有类型和术语的定义,例如compare_quest,game,g1side等,与我在第一个问题中的定义相同.

Inductive gameCompare (c : compare_quest) : game -> game -> Prop :=
 | igc : forall g1 g2 : game,
    innerGCompare (nextCompare c) (compareCombiner c) (g1side c) (g2side c) g1 g2 ->
    gameCompare c g1 g2
with innerGCompare (next_c : compare_quest) (cbn : combiner) (g1s g2s : side)
    : game -> game …

你如何解释归纳谓词？它们是做什么用的？他们背后的理论是什么？它们仅存在于依赖类型系统中，还是也存在于其他系统中？它们在某种程度上与 GADT 相关吗？为什么它们在 Coq 中默认为 true？

这是 Coq 的一个例子：

Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))

你会如何使用这个定义？它是数据类型还是命题？

我正在尝试学习 coq，所以请假设我对此一无所知。

如果我在 coq 中有一个引理

forall n m:nat, n>=1 -> m>=1 ...

我想通过对 n 进行归纳。我如何从 1 开始归纳？目前当我使用“归纳n”。战术它从零开始，这使得基本语句为假，从而难以继续。

任何提示？

我读到一种类型的归纳原理只是一个关于命题的定理P.所以我构建了一个List基于右(或反向)列表构造函数的归纳原理.

Definition rcons {X:Type} (l:list X) (x:X) : list X := 
  l ++ x::nil.

归纳原理本身是:

Definition true_for_nil {X:Type}(P:list X -> Prop) : Prop :=
  P nil.

Definition true_for_list {X:Type} (P:list X -> Prop) : Prop :=
  forall xs, P xs.

Definition preserved_by_rcons {X:Type} (P: list X -> Prop): Prop :=
  forall xs' x, P xs' -> P (rcons xs' x).

Theorem list_ind_rcons: 
  forall {X:Type} (P:list X -> Prop),
    true_for_nil P ->
    preserved_by_rcons P ->
    true_for_list P. …

我正在阅读Jeremy Gibbons关于折纸编程的文章,我坚持练习3.7,要求读者证明列表的融合法展开:

unfoldL p f g . h = unfoldL p' f' g'

Run Code Online (Sandbox Code Playgroud)

如果

p . h = p'
f . h = f'
g . h = h . g'

Run Code Online (Sandbox Code Playgroud)

unfoldL列表展开的功能定义如下:

unfoldL :: (b -> Bool) -> (b -> a) -> (b -> b) -> b -> List a
unfoldL p f g b = if p b then Nil else Cons (f b) (unfoldL p f g (g b))

这是我目前尝试的证据:

(unfoldL p f …

考虑zip由Peano数字索引的通常矢量长度的这个定义:

{-# language DataKinds          #-}
{-# language KindSignatures     #-}
{-# language GADTs              #-}
{-# language TypeOperators      #-}
{-# language StandaloneDeriving #-}
{-# language FlexibleInstances  #-}
{-# language FlexibleContexts   #-}

module Vector
  where

import Prelude hiding (zip)

data N
  where
    Z :: N
    S :: N -> N

data Vector (n :: N) a
  where
    VZ :: Vector Z a
    (:::) :: a -> Vector n a -> Vector (S n) a

infixr 1 :::

deriving instance Show a …

我工作在以下定理的证明Sn_le_Sm__n_le_m中IndProp.v的软件基础（第1卷：逻辑基础）。

Theorem Sn_le_Sm__n_le_m : ?n m,
  S n ? S m ? n ? m.
Proof.
  intros n m HS.
  induction HS as [ | m' Hm' IHm'].
  - (* le_n *) (* Failed Here *)
  - (* le_S *) apply IHSm'.
Admitted.

其中，的定义le (i.e., ?)是：

Inductive le : nat ? nat ? Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : …

在 Haskell 中有很多关于生成素数的主题，但在我看来，它们都依赖于 ' isPrime' 函数，如果我们还不知道素数序列，它应该如下所示：

isPrime k = if k > 1 then null [ x | x <- [2,3..(div k 2) + 1], k `mod` x == 0]
                     else False

（div可能会替换为sqrt，但仍然......）

我试图基于“归纳定义”构造素数（假设我们有一组前n 个素数，那么第(n+1) 个素数是最小的整数，这样前n 个素数中没有一个是它的除数）。我试过用斐波那契数列的方式来做，它是：

fib :: Int -> Int
fib 0 = 0
fib 1 = 1
fib n = fibs !! n
    where fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

我最终得到了这个： …