Agda 中数据类型的可判定相等性

Question

我正在尝试使用 Agda stdlib 证明 Agda 中数据类型的可判定相等性。我有以下代码，但我不确定要填什么。目标看似有道理，但实际构建起来却充满挑战。

这在 Agda 中可行吗？关于如何解决这个问题有什么想法吗？

open import Data.String as String hiding (_≟_)

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Problem1 where

data Test : Set where
  test : String → Test


infix 4 _≟_ 
_≟_ : Decidable {A = Test} _≡_
test x ≟ test x₁ with x String.≟ x₁
... | yes refl = yes refl
... | no ¬a = no {!!}

洞口：

Goal: ¬ test x ≡ test x₁
————————————————————————————————————————————————————————————
¬a : ¬ x ≡ x₁
x₁ : ℕ
x  : ℕ

Answer 1

这实际上是一个单行，依赖于匿名函数内部相等性证明的大小写拆分，如下：

... | no ¬a = no λ {refl → ¬a refl}

Agda 中数据类型的可判定相等性

Decidable equality of data types in Agda

agda