agda - 用不相关的术语证明不相关的事情

Question

在 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 不接受我所拥有的。

Answer 1

您可以简单地在 a 上进行模式匹配和 b . Agda 将意识到唯一的
可能的情况是 a = T和 b = T一个，然后你就可以出院了
目标与refl .

顺便说一句，eq不需要被宣布为不相关。