agda - 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