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可以对功能应用程序做些什么,尽可能减少它们.在某些情况下,reduce会产生构造函数表达式,在其他情况下则不会,我们需要编写其他证明.

为了证明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