`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，但对于如何进行模式匹配仍然没有更明智的选择。

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

这将导致您可以访问“假”和您需要的证明元素。有关检查习语的更多信息，请参阅：

• 带有抽象的维基页面：https://agda.readthedocs.io/en/v2.6.0.1/language/with-abstraction.html
• 标准库中的 PropositionalEquality.agda 文件，它提供了成语以及如何使用它的快速说明
• 标准库中的 README/Inspect.agda 文件也提供了有关如何以及何时使用检查习语的完整示例