Agda 如何确定类型是不可能的

Question

所以我试图理解为什么这段代码在 ()

周围用黄色突出显示

data sometype : List ℕ → Set where
  constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (l1 ++ (n ∷ l2))

somef : sometype [] → ⊥
somef ()

但这并不

data sometype : List ℕ → Set where
  constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (n ∷ (l1 ++ l2))

somef : sometype [] → ⊥
somef ()

两者似乎都表明 sometype [] 为空，但 Agda 无法找出第一个？为什么？这背后的代码是什么？我可以定义 somef 以使第一个定义有效吗？

Answer 1

Agda 不能假设任何像 ++ 这样的任意函数。假设我们按如下方式定义 ++：

_++_ : {A : Set} → List A → List A → List A
xs ++ ys = []

在这种情况下，sometype [] → ⊥ 无法证明，接受 () 荒谬的模式将是一个错误。

在您的第二个示例中，sometype 的索引必须采用 n ∷ (l1 ++ l2) 形式，这是一个构造函数表达式，因为 _∷_ 是一个列表构造函数。 Agda 可以安全地推断出 _∷_ 构造的列表永远不会等于 []。一般来说，不同的构造函数可以被看作是不可能统一的。

Agda 可以对函数应用程序做的是尽可能地减少它们。在某些情况下，归约会产生构造函数表达式，而在其他情况下则不会，我们需要编写额外的证明。

为了证明sometype [] → ⊥，我们应该先做一些概括。我们不能在 sometype [] 的值上进行模式匹配（因为类型索引中的 ++），但我们可以在 sometype xs 上匹配一些抽象的 xs。所以，我们的引理如下：

someF' : ∀ xs → sometype xs → xs ≡ [] → ⊥
someF' .(n  ∷ l2)           (constr [] l2 n) ()
someF' .(n' ∷ l1 ++ n ∷ l2) (constr (n' ∷ l1) l2 n) ()

换句话说，∀ xs → sometype xs → xs ≢ []。我们可以从中得出所需的证明：

someF : sometype [] → ⊥
someF p = someF' [] p refl

How Agda determines a type is impossible