2

我在锻炼。这似乎是一件微不足道的事情（简化以表明问题显然在于列表拆分）：

  infixr 4 _::_ _++_ _==_

  data _==_ {A : Set} : (x : A) -> (y : A) -> Set where
    refl : (x : A) -> x == x

  data List (A : Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  _++_ : forall {A} -> List A -> List A -> List A
  nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  data Permutation {A : Set} : List A -> List A -> Set where
    pnil : Permutation nil nil
    p::  : forall {xs} -> (x : A) -> 
                          (zs : List A) -> (y : A) -> (ys : List A) ->
                          x == y -> Permutation xs (zs ++ ys) ->
                          Permutation (x :: xs) (zs ++ (y :: ys))

  lemma-ripTop : forall {A} -> (xs : List A) ->
                               (y : A) -> (ys : List A) ->
                               Permutation xs (y :: ys) ->
                               Permutation xs (y :: ys)
  lemma-ripTop nil y ys ()
  lemma-ripTop (x :: xs) y ys (p:: .x zs y1 ys1 x==y1 ps) = 
                          p:: x zs y1 ys1 x==y1 ps

总而言之，我声明可以定义两个列表的排列，如果它们可以提供Permutation具有一对相等元素的较小列表xand y，并且插入位置y由zsand确定ys。

然后lemma-ripTop（本来打算做一些完全不同的事情，但这里只是idon Permutation）需要证明给定 a Permutationfor a list ( y :: ys) 的东西。

  1. 我不明白为什么 Agda 需要查看zs ++ (y1 :: ys1) == y :: ys（这是我得到的错误）-我认为这应该从类型声明和构造函数中清楚吗？即，既然Permutation xs (y :: ys)是在输入中给出的，那么在构造函数中作为见证提供的拆分p::应该加起来为y :: ys.

  2. 如何让 Agda 相信这个列表拆分是有效的？

错误信息：

zs ++ y1 :: ys1 != y :: ys of type List A
when checking that the pattern p:: .x zs y1 ys1 x==y1 ps has type
Permutation (x :: xs) (y :: ys)
4

1 回答 1

1
于 2014-01-07T00:32:51.747 回答