有没有办法重写和简化`decEq x x`？

Question

在下面的代码中（试图解决“软件基础”[列表章节]中的一个练习），Idris 报告了countSingleton_rhs 的一个非常复杂的类型。该类型包含一个复杂的表达式，其核心是：case decEq x x of ...。

module CountSingleton

data NatList : Type where
  Nil : NatList
  (::) : Nat -> NatList -> NatList

-- count occurrences of a value in a list
count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count Z (Z :: ns) = S (count Z ns)
count Z (_ :: ns) = count Z ns
count j@(S _) (Z :: ns) = count j ns
count (S j) ((S k) :: ns) =
  case decEq j k of
    Yes Refl => S (count (S j) ns)
    No _ => count (S j) ns

-- to prove
countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton Z = Refl
countSingleton (S k) = ?countSingleton_rhs

为什么 Idris 不将 decEq x x 简化为 Yes Refl？ 有没有更好的方法来实现count 来避免这种行为？ 为了取得进展，我可以做些什么来简化/重写类型？

Answer 1

您的计数功能比它需要的更分裂。如果你无论如何检查decEq x y，你可以统一除count _ [] = Z之外的所有情况：

count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count x (y :: ns) = case decEq x y of
    Yes Refl => S (count x ns)
    No _ => count x ns

证明countSingleton 的直接方法是顺其自然。您的countSingleton_rhs 具有复杂类型，因为该类型是大小写切换，具体取决于decEq v v 的结果。使用with Idris 可以将分支的结果应用到结果类型。

countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton v with (decEq v v)
    | Yes prf = Refl
    | No contra = absurd $ contra Refl

---

正如您所指出的，这似乎有点多余，因为decEq x x 显然是Yes Refl。幸运的是，它已经在库中得到证明：decEqSelfIsYes : DecEq a => decEq x x = Yes Refl，我们可以使用它来重写结果类型：

countSingleton : (v : Nat) -> (count v [v]) = S Z
countSingleton v = rewrite decEqSelfIsYes {x=v} in Refl

不幸的是，由于an open issue，重写case 类型并不总是有效。但是你可以用with 重写count 来规避这个问题：

count : (v : Nat) -> (s : NatList) -> Nat
count _ [] = Z
count x (y :: ns) with (decEq x y)
    | Yes _ = S (count x ns)
    | No _ = count x ns