7

伊德里斯版本：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

即：如果nis notbase加上 的自然倍数jump，则两者都不是jump + n。

如果我要求 Idris 区分大小写m，它只会显示我IBase- 然后我就卡住了。

有人会指出我正确的方向吗？

编辑 0： 申请induction给m我以下消息：

Induction needs an eliminator for Iterate.Iterate.Iterate

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

4

2 回答 2

1

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

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

plus535 : Plus 5 3 (3 + 2)
plus535 = IBase
于 2018-11-22T18:55:27.927 回答
0

要编辑 0：要对一个类型进行归纳，它需要一个特殊的限定符：

%elim data Iterate = <your definition>

对于主要问题：抱歉，我没有通读您的所有代码，我只想对伪造证明提出一些建议。根据我的经验（我什至深入研究了标准库的源代码以找到一些帮助），当您需要证明Not a( a -> Void) 时，通常可以使用 some 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

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

于 2015-03-18T13:22:56.840 回答