agda - リストの分割が有効であることを証明するには?

Question

私は運動しています。これは簡単なことのようです（問題が明らかにリスト分割にあることを示すために単純化されています）：

  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

要するに、2 つのリストの順列を定義できることを宣言します。それらがとによって決定されるとのPermutation等しい要素のペアを持つ小さなリストの を提供できる場合です。xyyzsys

次にlemma-ripTop(まったく別のことをするつもりだったが、ここでは にあるだけidである)リスト ( ) に対してPermutation与えられた何かを証明する必要がある。Permutationy :: 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)

Answer 1