精炼参数的“案例”

Question

在this answer on a question about the totality checker 中，建议使用涉及使用case 而不是with 的解决方法。

但是，在匹配结果精炼其他参数类型的情况下，这种转换并不简单。

例如，给定以下定义：

data IsEven : Nat -> Nat -> Type where
    Times2 : (n : Nat) -> IsEven (n + n) n

data IsOdd : Nat -> Nat -> Type where
    Times2Plus1 : (n : Nat) -> IsOdd (S (n + n)) n

total parity : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n))

以下定义类型检查，但不作为全部接受：

foo1 : Nat -> Nat
foo1 n with (parity n)
  foo1 n@(k + k) | Left (Evidence _ (Times2 k)) = (n * n)
  foo1 n@(S (k + k)) | Right (Evidence _ (Times2Plus1 k)) = (2 * (k * n + k))

而下面的没有类型检查：

foo2 : Nat -> Nat
foo2 n = case parity n of
  Left (Evidence k (Times2 k)) => n * n
  Right (Evidence k (Times2Plus1 k)) => (2 * (k * n + k))

由于

Type mismatch between
      IsEven (k + k) k (Type of Times2 k)
and
      IsEven n k (Expected type)

我也试过expanding the with in foo1：

foo1' : (n : Nat) -> Either (Exists (IsEven n)) (Exists (IsOdd n)) -> Nat
foo1' n@(k + k) (Left (Evidence k (Times2 k))) = (n * n)
foo1' n@(S (k + k)) (Right (Evidence k (Times2Plus1 k))) = 2 * (k * n + k)

foo1 : Nat -> Nat
foo1 n = foo1' n (parity n)

但在这里，foo1' 也不被完全接受：

 foo1' is not total as there are missing cases

Answer 1

我发现一个有效的解决方法是在每个分支中重新绑定n，即将foo2写成

foo2 : Nat -> Nat
foo2 n = case parity n of
  Left (Evidence k (Times2 k)) => let n = k + k in n * n
  Right (Evidence k (Times2Plus1 k)) => let n = S (k + k) in (2 * (k * n + k))

不幸的是，虽然这适用于我最初问题的简化问题，但当各种分支的类型不同时，它就不起作用了；例如在

total Foo : Nat -> Type
Foo n = case parity n of
    Left (Evidence k (Times2 k)) => ()
    Right (Evidence k (Times2Plus1 k)) => Bool

foo : (n : Nat) -> Foo n
foo n = case parity n of
    Left (Evidence k (Times2 k)) => ()
    Right (Evidence k (Times2Plus1 k)) => True

失败了

 Type mismatch between
         () (Type of ())
 and
         case parity (plus k k) of
           Left (Evidence k (Times2 k)) => ()
           Right (Evidence k (Times2Plus1 k)) => Bool (Expected type)