with-pattern 结果不可见

Question

我正在尝试查看如何分支到“安全键入”的代码。例如，下面的意思是只在安全路径上调用tail - 即如果输入列表不为空。当然，有一种简单的方法可以只对列表进行模式匹配，但想法是协调函数 (null) 的结果及其在右侧的使用：

data Void : Set where

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

data Bool : Set where
  True : Bool
  False : Bool

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

null : forall {A} -> List A -> Bool
null nil         = True
null (x :: xs)   = False

non-null : forall {A} -> List A -> Set
non-null nil = Void
non-null (x :: xs) = (x :: xs) == (x :: xs)

tail : forall {A} -> (xs : List A) -> {p : non-null xs} -> List A
tail (_ :: xs) = xs
tail nil      {p = ()}

prove-non-null : forall {A} -> (xs : List A) -> (null xs == False) -> non-null xs
prove-non-null nil         ()
prove-non-null (x :: xs)   refl = refl

compileme : forall {A} -> List A -> List A
compileme xs with null xs
...             | True    = xs
...             | False   = tail xs {prove-non-null xs refl}

在最后一行，agda 抱怨不能证明refl 是null xs == False 类型。为什么它看不到 with-clause 刚刚见证了null xs 是False？

正确的做法是什么？如何从看似不依赖的结果中“提取”依赖，比如Bool类型不依赖列表xs，但在上下文中它是？

Answer 1

那是关于inspect 的成语。检查the original thread 和this stackoverflow question。标准库中inspect的The current version来自this线程（也有一些explanations）。

如果删除_==_的定义，则可以将compileme定义为

open import Relation.Binary.PropositionalEquality renaming (_≡_ to _==_)

...

compileme : forall {A} -> List A -> List A
compileme xs with null xs | inspect null xs
...             | True    | [ _ ] = xs
...             | False   | [ p ] = tail xs {prove-non-null xs p}

顺便说一句，(x :: xs) == (x :: xs) 应该是什么意思？只是

open import Data.Unit
...
non-null (x :: xs) = ⊤

顺便说一句，您可以定义类型安全的tail，就像我在this 答案中定义的类型安全pred。