伊德里斯:证明具体条款是不可能的

Question

伊德里斯版: 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.

如果我问伊德里斯案件分裂m只会告诉我IBase- 然后我就会陷入困境.

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

---

编辑0: 应用induction到m给我的以下信息:

Induction needs an eliminator for Iterate.Iterate.Iterate

---

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

Answer 1

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

%elim data Iterate = <your definition>

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

%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

就你而言，我想你需要结合几个证明。