agda - 方便地使用多个 EqReasoning 实例化

Answer 1

通常，Agda 可以为您选择的唯一方法是当它由上下文唯一确定时。在 的情况下EqReasoning，通常没有足够的信息来确定Setoid，实际上更糟糕的是：您可以Setoid在同一个Carrierand上有两个不同的 s _≈_（例如，考虑trans该领域中两个定义上不相等的 itivity证明isEquivalence）。

---

但是，Agda 确实允许特殊形式的隐式参数，只要只有一个所需类型的值就可以填充。这些被称为实例参数（将实例视为 Haskell 类型的类实例）。

为了大致演示这是如何工作的：

postulate
  A : Set
  a : A

现在，实例参数用双花括号括起来{{}}：

elem : {{x : A}} → A
elem {{x}} = x

如果我们决定稍后在elem某个地方使用，Agda 将检查A范围内的任何类型值，如果只有其中一个，它会将那个填入 for {{x : A}}。如果我们添加：

postulate
  b : A

Agda 现在会抱怨：

Resolve instance argument _x_7 : A. Candidates: [a : A, b : A]

---

因为 Agda 已经允许您在类型级别上执行计算，所以故意限制实例参数的功能，即 Agda 不会执行递归搜索来填充它们。例如：

eq : ... → IsEquivalence _≈_ → IsEquivalence (Eq _≈_)

Eq你的问题中Data.Maybe.Eq提到了哪里。然后，当您要求 Agda 填写 type 的实例参数时IsEquivalence (Eq _≈_)，它不会尝试查找类型的内容IsEquivalence _≈_并应用于eq它。

---

有了这个，让我们来看看有什么可行的方法。但是，请记住，所有这些都基于统一，因此您可能需要在这里和那里将其推向正确的方向（如果您正在处理的类型变得复杂，统一可能需要您给它很多方向，以至于最后是不值得的）。

就个人而言，我发现实例参数有点脆弱，我通常会避免使用它们（从快速检查来看，标准库似乎也是如此），但您的经验可能会有所不同。

无论如何，我们开始吧。我构建了一个（完全无意义的）示例来演示如何做到这一点。首先是一些样板：

open import Data.Maybe
open import Data.Nat
open import Relation.Binary

import Relation.Binary.EqReasoning as EqR

为了让这个例子自成一体，我写了一些Setoid以自然数为载体的：

data _≡ℕ_ : ℕ → ℕ → Set where
  z≡z :                    0     ≡ℕ 0
  s≡s : ∀ {m n} → m ≡ℕ n → suc m ≡ℕ suc n

ℕ-setoid : Setoid _ _
ℕ-setoid = record
  { _≈_     = _≡ℕ_
  ; isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  }
  where
  refl : Reflexive _≡ℕ_
  refl {zero}  = z≡z
  refl {suc _} = s≡s refl

  sym : Symmetric _≡ℕ_
  sym z≡z     = z≡z
  sym (s≡s p) = s≡s (sym p)

  trans : Transitive _≡ℕ_
  trans z≡z          q  = q
  trans (s≡s p) (s≡s q) = s≡s (trans p q)

现在，EqReasoning模块在 a 上进行了参数化Setoid，所以通常你会这样做：

open EqR ℕ-setoid

但是，我们希望Setoid参数是隐式的（实例）而不是显式的，所以我们定义并打开一个虚拟模块：

open module Dummy {c ℓ} {{s : Setoid c ℓ}} = EqR s

我们可以写出这个简单的证明：

idʳ : ∀ n → n ≡ℕ (n + 0)
idʳ 0 = z≡z
idʳ (suc n) = begin
  suc n        ≈⟨ s≡s (idʳ n) ⟩
  suc (n + 0)  ∎

请注意，我们不必指定ℕ-setoid，实例参数选择了它，因为它是唯一类型正确的值。

现在，让我们稍微调味。我们将添加Data.Maybe.setoid到组合中。同样，因为实例参数不执行递归搜索，我们必须自己定义 setoid：

Maybeℕ-setoid = setoid ℕ-setoid
_≡M_ = Setoid._≈_ Maybeℕ-setoid

我将假设一些愚蠢的事情只是为了证明 Agda 确实选择了正确的 setoid：

postulate
  comm : ∀ m n → (m + n) ≡ℕ (n + m)
  eq0  : ∀ n → n ≡ℕ 0
  eq∅  : just 0 ≡M nothing

lem : ∀ n → just (n + 0) ≡M nothing
lem n = begin
  just (n + 0)  ≈⟨ just
    (begin
      n + 0  ≈⟨ comm n 0 ⟩
      n      ≈⟨ eq0 n ⟩
      0      ∎
    )⟩
  just 0        ≈⟨ eq∅ ⟩
  nothing       ∎

Answer 2