在 Agda 2.6.0.1 中,我想在一个记录中使用一个不相关的证明项,然后仅根据它们的数据项来证明这些记录中的两个是相等的。
data Bools : Set where
T : Bools
F : Bools
record Thing : Set where
field
val : Bools
.pr : val == T
.eq : (a b : Thing) -> a == b
eq record { val = a ; pr = pr1 } record { val = b ; pr = pr2 } = ?
我觉得我应该能够通过诉诸于每个
Thing
的事实来证明这一点。知道它的 val
等于 T
. (如果 pr1
和 pr2
都相关,我可以匹配它们以显示 a = T = b
;但是我需要 Streicher's K 来给我 Thing.pr
项的相等性。)自
Thing.pr
是不相关的,我当然需要处于不相关的上下文中,然后才能希望使用它。我以为我已经通过放置 .
实现了这一目标前面是eq
的名字在其声明中;但是当我尝试使用 pr1
在洞中,我仍然收到通常的“变量 pr1
被声明为不相关,因此不能在这里使用”的消息。我可以在这里做我想做的吗?我可以做
eq
足够不相关,我可以使用 pr1
和 pr2
在它的定义中?答案在 Using irrelevant fields建议我可以,但对于我的生活,我不明白为什么 Agda 不接受我所拥有的。
最佳答案
您可以简单地在 a
上进行模式匹配和 b
. Agda 将意识到唯一的
可能的情况是 a = T
和 b = T
一个,然后你就可以出院了
目标与refl
.
顺便说一句,eq
不需要被宣布为不相关。
关于agda - 用不相关的术语证明不相关的事情,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59523582/