我正在尝试编写以下函数:
justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x y pf = {!!}
我不知道怎么写。对我来说,它是直观到公理化的程度,但编译器不接受 refl 作为它的证明。
我经常必须证明这类事情,例如,证明如果两个非空列表相等,则它们的头相等。
一般的方法是什么?这与 Conor McBride 的“green-goo”有关,即在构造函数的返回中包含函数吗?
最佳答案
解决方案的基础是对 pf
进行模式匹配,refl
一起,并使用点线模式表示 y
等于 x
(因为 refl
的类型!)。
justEq : ∀ {A} -> (x y : A) -> (just x ≡ just y) -> (x ≡ y)
justEq x .x refl = {!!}
此时,由于 y = .x
等式,右侧孔的类型已统一为 (x ≡ x)
模式匹配,这意味着您可以使用 refl
作为类型正确的值,给出
justEq x .x refl = refl
关于types - Agda:证明当值相等时,它们的构造函数参数也相等,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30879801/