`with 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 语句，它准确地确定了 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 但仍然 none 更明智地了解如何进行模式匹配。

Answer 1

看来你需要记住以下表达式

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

确实等于

false

这是一个非常常见的问题，源于 'with' 结构的工作方式。默认情况下，您无权访问连接模式匹配元素与模式匹配结果的证明元素，即在您的示例中，类型为：

的元素

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

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

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

这将使您能够访问 'false' 和您需要的证明元素。有关 inspect 习语的更多信息，请参阅：

with-abstraction 上的 wiki 页面：https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html
标准库中的文件PropositionalEquality.agda，它提供了习语以及如何使用它的快速描述
标准库中的文件 README/Inspect.agda 也提供了有关如何以及何时使用 inspect idiom 的完整示例

`with f x` 匹配 `false`，但不能构造 `f x == false`

`with f x` matches `false`, but cannot construct `f x == false`

agda