在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

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

{-# 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₂)

你可以在目标中看到你有一个非依赖的sigma类型，但是你的引理有一个依赖的类型！因此，您只需将引理中的B对n₁的依赖更改为a

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

通过对lemma类型的这一小更改，您的证明就被接受了！

Answer 2

在这种情况下(通常情况下，当目标和目标表面上匹配时，Agda会给出悲哀)，问题是由于隐含变量不匹配。如果您打开show-implicit (通过C-c C-x C-h或{-# OPTIONS --show-implicit #-})，然后比较Goal和Have，您就可以发现其中的不同之处，从而理清头绪。(弄清楚为什么会有这样的差异是另一个问题。)