在 Agda 中为依赖对定义可判定相等性

Question

我正在尝试在 sigma 类型上定义可判定相等性，但尽管我的目标与我的目标相符，但还是卡住了。

module SigmaEqual where

open import Function using (id)
open import Data.Nat using (ℕ) renaming (_≟_ to _≟ℕ_)
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; cong; refl)

data B : ℕ → Set where
  bcons : (n : ℕ) → B n

Tuple = Σ ℕ B

_≟B_ : ∀ {n} → Decidable {A = B n} _≡_
bcons n ≟B bcons .n = yes refl

_≟_ : Decidable {A = Tuple} _≡_
(n₁ , b₁) ≟ (n₂ , b₂) with n₁ ≟ℕ n₂
(n₁ , b₁) ≟ (n₂ , b₂) | no ¬p = no λ q → ¬p (cong proj₁ q)
(n₁ , b₁) ≟ (.n₁ , b₂) | yes refl with b₁ ≟B b₂
(n₁ , b₁) ≟ (.n₁ , .b₁) | yes refl | yes refl = yes refl
(n₁ , b₁) ≟ (.n₁ , b₂) | yes refl | no ¬p = no λ q → ¬p (lemm {n₁} {b₁} {b₂} q)
  where
  lemm : {a : ℕ}{b₁ b₂ : B n₁} → (a , b₁) ≡ (a , b₂) → b₁ ≡ b₂
  lemm refl = refl

当我检查孔中的上下文时，我得到以下信息：

Goal: (n₁ , b₁) ≡ (n₁ , b₂)
Have: (n₁ , b₁) ≡ (n₁ , b₂)
————————————————————————————————————————————————————————————
q  : (n₁ , b₁) ≡ (n₁ , b₂)
¬p : b₁ ≡ b₂ → .Data.Empty.⊥
...

所以我想我应该能够改进它并将 q 放在它的位置，但是它不起作用，如果我放 q，我会收到以下错误。

x != n₁ of type ℕ when checking that the expression q has type (n₁ , b₁) ≡ (n₁ , b₂)

这特别令人困惑，因为我不知道所讨论的 x 来自哪里。

Answer 1

在这种情况下（当目标和目标显然匹配但 Agda 给出悲伤时通常是这种情况）问题是由于隐式变量不匹配。如果您打开 show-implicit（通过 C-c C-x C-h 或 {-# OPTIONS --show-implicit #-}），然后比较 Goal 和 Have，您可以发现差异，从而消除自己的困惑。（弄清楚为什么会有这样的差异是一个单独的问题。）

Answer 2

您可以通过在文件顶部添加以下行来了解发生了什么：

{-# OPTIONS --show-implicit #-}
open import Agda.Primitive

然后你就可以看到哪里出了问题：

Goal: _≡_ {lzero} {Σ {lzero} {lzero} ℕ (λ v → B n₁)} (n₁ , b₁)
      (n₁ , b₂)
Have: _≡_ {lzero} {Σ {lzero} {lzero} ℕ B} (n₁ , b₁) (n₁ , b₂)

您可以在目标中看到您有一个 non-dependent 西格玛类型，但您的引理有一个从属类型！因此，您只需要将引理中 B 对 n₁ 的依赖性更改为 a:

lemm : {a : ℕ}{b₁ b₂ : B a} → _≡_ {A = Tuple} (a , b₁) (a , b₂) → b₁ ≡ b₂
lemm refl = refl

通过对 lemma 类型的这个小改动，您的证明被接受了！

在 Agda 中为依赖对定义可判定相等性

Defining decidable equality for dependent pair in Agda

equality

agda

dependent-type

existential-type