types - Agda：证明当值相等时，它们的构造函数参数相等

Question

我正在尝试编写以下函数：

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}

我不知道怎么写这个。对我来说，这是不言自明的直觉，但编译器不接受 refl 作为它的证明。

我经常不得不证明这些事情，例如，证明如果两个非空列表相等，那么它们的头是相等的。

对此的一般方法是什么？这是否与 Conor McBride 的在构造函数的返回中具有函数的“green-goo”有关？

score 3 · Accepted Answer

解决方案的基础是模式匹配与pf使用点模式相等（因为！的类型）。refl yxrefl

justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x .x refl = {!!}

(x ≡ x)此时，由于模式匹配的y = .x相等性，右侧孔的类型已统一为，这意味着您可以将refl其用作类型良好的值，给出

justEq x .x refl = refl

1 回答 1