`with fx` 匹配 `false`，但不能构造 `fx == 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

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

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

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

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