“与f x‘匹配`false`’，但不能构造`f x == false`‘

Question

这里有一段代码：

-- transitivity
trans : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl

union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
                           (ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' m n x with ismember m x | ismember n x | ismember (set-union (set-pair m n)) x
union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
                       (ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' m n x with ismember m x | ismember n x | ismember (set-union (set-pair m n)) x
...                  | false | false | false = trans {x = ismember (set-union (set-pair m n)) x} {y = false}
                                                     refl -- line #102
                                                     (union-match m n x)
-- more code available on request, although I can't see why that would matter

产生一个错误：

code.agda:102,54-58
(ismember (set-union (set-pair m n)) x) != false of type Bool
when checking that the expression refl has type
ismember (set-union (set-pair m n)) x == false

我有一个with-statement，它准确地确定了ismember (set-union (set-pair m n)) x是false这一事实。为什么它不能确定它是false

好的，我甚至可以看到一些已知的问题，https://agda.readthedocs.io/en/v2.5.2/language/with-abstraction.html#ill-typed-with-abstractions，但仍然没有更聪明的模式匹配，然后。

Answer 1

看起来您需要记住以下表达式

ismember (set-union (set-pair m n)) x

实际上等于

false

这是一个非常常见的问题，它来自于“with”结构的工作方式。默认情况下，您无法访问将模式匹配的元素与模式匹配的结果(即在您的示例中是一个类型的元素)连接的证据元素：

ismember (set-union (set-pair m n)) x == false

为了获得这种类型的元素，您需要使用标准库中与命题相等一起定义的“检查”成语。更具体地说，这意味着您必须向模式匹配中添加一个新元素，如下所示：

... | ismember (set-union (set-pair m n)) x | inspect (ismember (set-union (set-pair m n)) x

这将导致您可以访问“false”和所需的验证元素。有关检查成语的更多信息，请参见：

https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html

• The文件库中的wiki页面，它提供了标准库中的成语，以及如何在标准库中使用它的快速描述-自述文件