如何證明列表拆分有效？

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 

長期和短期的它，我宣佈一個可如果他們可以定義兩個列表的置換，提供具有一對相等元件x和y的較小列表的Permutation，並且y的插入位置由zs和ys確定。

然後lemma-ripTop（是爲了做一些完全不同的，但在這裏它只是id上Permutation）需要證明的東西給出一個列表（y :: ys）一個Permutation。

1. 我不明白爲什麼阿格達需要看到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

考慮下面的代碼片段（你可能知道這是感應原理的身份類型/命題平等）：

J : {A : Set} (P : (x y : A) → x == y → Set) 
    (f : ∀ x → P x x (refl x)) (x y : A) (p : x == y) → P x y p 
J P f x y p = ? 

當我們的模式匹配p並用refl代替：

J P f x y (refl .x) = ? 

阿格達會大叫

x != y of type A 
when checking that the pattern refl .x has type x == y 

這是因爲x和y再也不能任意模式：有這兩個已經揭示圖案p匹配關係。即，x和y必須是相同的東西。你必須，而不是寫：

J P f x .x (refl .x) = f x 

或許更重要的例子是自然數的奇偶觀點：

data Parity : ℕ → Set where 
    even : ∀ k → Parity  (k * 2) 
    odd : ∀ k → Parity (1 + k * 2) 

我們可以計算出每一個自然數的奇偶：

parity : ∀ n → Parity n 
parity 0 = even 0 
parity (suc n) with parity n 
parity (suc  .(k * 2)) | even k = odd k 
parity (suc .(1 + k * 2)) | odd k = even (1 + k) 

注意，在模式匹配之後，n不再是任意的 - 它必須是k * 2（在even的情況下）或1 + k * 2（在odd的情況下）。

---

現在，讓我們看看代碼的問題在哪裏。當您在排列參數上進行模式匹配時，y和ys會變得固定 - 該模式顯示其結構，非常類似於上述情況。所以你實際上已經改寫了y和ys來表達他們不再是任意的事實。但問題在於：如果你試圖寫下y和ys的外觀，你會意識到你不能這樣做。 y可以是zs的第一個元素，也可以是y1，具體取決於zs。

lemma-ripTop (x :: xs) .z .(zs ++ y1 :: ys1) 
    (p:: .x (z :: zs) y1 ys1 x==y1 ps) = ? 

模式匹配zs不幸的是不起作用。整個（虛線）模式應該是z :: zs ++ y1 :: ys1，但這裏分爲兩種不同的模式，我想這是一個禁忌（不能說這是Agda無法做或不做的事，對不起）。

---

一種選擇是一切遷入的證明，我不知道是如何有助於您的情況，但在這裏你去。

首先，我們需要表達存在性量化。依賴對（西格瑪類型）正是這樣做;這裏是從標準庫中的定義：

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where 
    constructor _,_ 
    field 
    proj₁ : A 
    proj₂ : B proj₁ 

open Σ public 

因此，例如，語句「存在一個自然數n這樣n * n == 4」將被表示爲Σ ℕ λ n → n * n == 4，並證明是一對天生的數量和證明其廣場確實是4.在我們的情況下，這將是(2 , refl 4)。

，我們可以分裂成l將zs ++ ys通過證明表示了存在r₁和r₂，這樣l == r₁ ++ r₂，如果最終的排列是k，那麼我們需要證明k == r₁ ++ y :: r₂的事實。這是整個事情：

data Permutation {A : Set} : (xs ys : List A) → Set a where 
    nil : Permutation nil nil 
    cons : (x y : A) (xs ys zs : List A) 
    (p₁ : Σ _ λ r₁ → Σ _ λ r₂ → ys == r₁ ++ r₂) 
    (p₂ : x == y) 
    (p₃ : let (r₁ , r₂ , _) = p₁ in zs == r₁ ++ y :: r₂) → 
    Permutation xs ys → Permutation (x :: xs) zs 

這可能或可能不愉快的工作，但它保持忠實於您的原始實施。如果你願意用不同的東西：你可以使用輔助的數據類型表達的事實，x是xs地方：

data insert_into_==_ {A : Set} (x : A) : List A → List A → Set where 
    here : ∀ {xs}   → insert x into xs == (x :: xs) 
    there : ∀ {y} {xs} {xys} → insert x into xs == xys → 
          insert x into (y :: xs) == (y :: xys) 

排列則是：

data Permutation {A : Set} : (xs ys : List A) → Set where 
    nil : Permutation nil nil 
    cons : ∀ {x xs ys xys} → 
     insert x into xs == xys → 
     Permutation xs ys → 
     Permutation (x :: xs) xys