故障在圖案匹配阿格達2.5.1.2

Question

鑑於下列的數據類型，其編碼兩個自然數之間的驗證比較：

open import Agda.Builtin.Nat 

data Compare : Nat -> Nat -> Set where 
    LT : {m : Nat} {n : Nat} -> Compare m (suc (m + n)) 
    EQ : {m : Nat} -> Compare m m 
    GT : {m : Nat} {n : Nat} -> Compare (suc (m + n)) m 

下面的代碼正確地進行比較的數字和計算它們的差值：

comparehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Compare (suc m) (suc n) 
comparehelper LT = LT 
comparehelper EQ = EQ 
comparehelper GT = GT 

compare : (m : Nat) (n : Nat) -> Compare m n 
compare 0 0 = EQ 
compare (suc _) 0 = GT 
compare 0 (suc _) = LT 
compare (suc m) (suc n) = comparehelper (compare m n) 

differencehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Nat 
differencehelper (LT {n = difflt1}) = suc difflt1 
differencehelper EQ = 0 
differencehelper (GT {n = difflt1}) = suc difflt1 

difference : Nat -> Nat -> Nat 
difference m n = differencehelper (compare m n) 

但以下顯然功能相同的代碼沒有（ 模式匹配失敗類型檢查）：

compare' : (m : Nat) (n : Nat) -> Compare m n 
compare' 0 0 = EQ 
compare' (suc _) 0 = GT 
compare' 0 (suc _) = LT 
compare' (suc m) (suc n) with compare' m n 
... | LT = LT 
... | EQ = EQ 
... | GT = GT 

difference' : Nat -> Nat -> Nat 
difference' m n with compare' m n 
... | LT {n = difflt1} = suc difflt1 
... | EQ = 0 
... | GT {n = difflt1} = suc difflt1 

行爲差異的解釋是什麼？正如問題所述，我正在運行Agda 2.5.1.2。

Answer 1

這裏的問題是，類型Compare m n的值上的模式匹配優化了m和n的模式。

因此，...代表的計劃compare' (suc m) (suc n)已無效。你必須用精細的圖案重複左手邊。

compare' (suc m) (suc n) with compare' m n 
compare' (suc m) (suc .(suc m + _)) | LT = LT 
compare' (suc m) (suc .m)   | EQ = EQ 
compare' (suc .(suc m + _)) (suc m) | GT = GT 

我用

強調這裏這是在範圍，但沒有明確命名的（他們是隱含參數LT和GT分別）的變量。事實上，他們沒有被命名，但在模式中是必需的，這可能是一個很好的線索，他們應該可能是構造函數LT和GT的明確參數。

另外，如果你不關心的模式，您可以使用下劃線（這可能代表任何圖案，包括那些點），並寫：

compare' (suc _) (suc _) | LT = LT 
compare' (suc _) (suc _) | EQ = EQ 
compare' (suc _) (suc _) | GT = GT 

由於@asr提到的較新版本Agda將支持您當前的模式匹配，因爲dot patterns have been made optional。