伊德里斯：证明特定条款是不可能的答案

【问题标题】：Idris: proof that specific terms are impossible伊德里斯：证明特定条款是不可能的
【发布时间】：2015-03-01 17:20:00
【问题描述】：

伊德里斯版本：0.9.16

我试图描述从 base 值和迭代的 step 函数生成的构造：

namespace Iterate
  data Iterate : (base : a) -> (step : a -> a) -> a -> Type where
    IBase : Iterate base step base
    IStep : Iterate base step v -> Iterate base step (step v)

使用它我可以定义Plus，描述来自jump 值的迭代添加的构造：

namespace Plus
  Plus : (base : Nat) -> (jump : Nat) -> Nat -> Type
  Plus base jump = Iterate base (\v => jump + v)

这个的简单示例用法：

namespace PlusExamples
  Even : Nat -> Type; Even = Plus 0 2
  even0 : Even 0; even0 = IBase
  even2 : Even 2; even2 = IStep even0
  even4 : Even 4; even4 = IStep even2

  Odd  : Nat -> Type; Odd  = Plus 1 2
  odd1 : Odd 1; odd1 = IBase
  odd3 : Odd 3; odd3 = IStep odd1

  Fizz : Nat -> Type; Fizz = Plus 0 3
  fizz0 : Fizz 0; fizz0 = IBase
  fizz3 : Fizz 3; fizz3 = IStep fizz0
  fizz6 : Fizz 6; fizz6 = IStep fizz3

  Buzz : Nat -> Type; Buzz = Plus 0 5
  buzz0 : Buzz 0; buzz0 = IBase
  buzz5 : Buzz 5; buzz5 = IStep buzz0
  buzz10 : Buzz 10; buzz10 = IStep buzz5

下面描述了base以下的值是不可能的：

  noLess : (base : Nat) ->
           (i : Fin base) ->
           Plus base jump (finToNat i) ->
           Void
  noLess Z     FZ     m     impossible
  noLess (S b) FZ     IBase impossible
  noLess (S b) (FS i) IBase impossible

base 和 jump + base 之间的值如下：

  noBetween : (base : Nat) ->
              (predJump : Nat) ->
              (i : Fin predJump) ->
              Plus base (S predJump) (base + S (finToNat i)) ->
              Void
  noBetween b Z     FZ     m     impossible
  noBetween b (S s) FZ     IBase impossible
  noBetween b (S s) (FS i) IBase impossible

我无法定义以下函数：

noJump : (Plus base jump n -> Void) -> Plus base jump (jump + n) -> Void
noJump f m = ?noJump_rhs

即：如果n 不是base 加上jump 的自然倍数，那么jump + n 也不是。

如果我让 Idris 对 m 进行大小写拆分，它只会显示 IBase - 然后我就卡住了。

有人能指点我正确的方向吗？

编辑 0： 将induction 应用到m 会给我以下信息：

Induction needs an eliminator for Iterate.Iterate.Iterate

编辑 1： 名称更新，这里是来源的副本：http://lpaste.net/125873

【问题讨论】：

我认为在目前的形式下，这个定理是错误的。例如。 Plus 5 3 2 为假，但Plus 5 3 (3 + 2) :~: Plus 5 3 5 为真。

标签： idris

【解决方案1】：

我认为有一个很好的理由停留在这个证明的IBase 案例上，那就是这个定理是错误的！考虑：

noplus532 : Plus 5 3 2 -> Void
noplus532 IBase impossible
noplus532 (IStep _) impossible

plus535 : Plus 5 3 (3 + 2)
plus535 = IBase

【讨论】：

【解决方案2】：

要Edit 0：引入一个类型，它需要一个特殊的限定符：

%elim data Iterate = <your definition>

对于主要问题：抱歉，我没有通读您的所有代码，我只想对伪造证明提出一些建议。根据我的经验（我什至钻研了标准库的源代码来寻找一些帮助），当你需要证明Not a（a -> Void）时，通常可以使用一些Not b（b -> Void）和一种方法来转换a 到 b，然后将其传递给第二个证明。例如，一个非常简单的证明，如果一个列表具有不同的头部，则它们不能是另一个列表的前缀：

%elim data Prefix : List a -> List a -> Type where
    pEmpty : Prefix Nil ys
    pNext  : Prefix xs ys -> Prefix (x :: xs) (x :: ys)

prefixNotCons : Not (x = y) -> Not (Prefix (x :: xs) (y :: ys))
prefixNotCons r (pNext _) = r refl

在你的情况下，我想你需要结合几个证明。

【讨论】：