agda - 如何告诉 Agda 展开一个定义来证明等价性

Question

我有这样一个函数:

open import Data.Char
open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true = 123
... | false = 456

我想证明，当我用相同的参数 (foo c c) 调用它时，它总是产生 123:

foo-eq⇒123 : ∀ (c : Char) → foo c c ≡ 123
foo-eq⇒123 c =
  foo c c ≡⟨ {!!} ⟩
  123 ∎

我可以使用 refl 来证明一个简单的例子:

foo-example : foo 'a' 'a' ≡ 123
foo-example = refl

所以，我认为我可以将 refl 放入洞中，因为所有 Agda 需要做的就是 beta-reduce foo c c。但是，用 refl 替换孔会产生以下错误:

.../Unfold.agda:15,14-18
(foo c c
 | Relation.Nullary.Decidable.Core.isYes
   (Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
    Data.Char.Properties.≈-reflexive
    (Relation.Nullary.Decidable.Core.map′
     (Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
     (Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c)))))
!= 123 of type ℕ
when checking that the expression refl has type foo c c ≡ 123

我怀疑问题在于 Agda 不会自动理解 c == c 对所有 c 都是 true:

c==c : ∀ (c : Char) → (c == c) ≡ true
c==c c = refl

.../Unfold.agda:23,10-14
Relation.Nullary.Decidable.Core.isYes
(Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
 Data.Char.Properties.≈-reflexive
 (Relation.Nullary.Decidable.Core.map′
  (Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
  (Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c))))
!= true of type Bool
when checking that the expression refl has type (c == c) ≡ true

那么，证明我的 foo-eq⇒123 定理的正确方法是什么？

Answer 1

Agda 内置的 Char 类型有点奇怪。让我们将它与一个非奇怪的内置类型 ℕ 进行对比。 ℕ 的相等性测试如下所示。

_≡ᵇ_ : Nat → Nat → Bool
zero  ≡ᵇ zero  = true
suc n ≡ᵇ suc m = n ≡ᵇ m
_     ≡ᵇ _     = false

请注意，n ≡ᵇ n 也不会归约为 true。毕竟，Agda 不知道 n 是 zero 还是 suc，即两个子句中的哪一个要申请归约。因此，这与您的 Char 示例存在相同的问题。但是对于 ℕ 来说，有一个简单的方法。

让我们再次查看您的示例，并添加一个基于 ℕ 的 foo、bar 版本。

open import Data.Char using (Char ; _==_ ; _≟_)
open import Data.Nat using (ℕ ; zero ; suc ; _≡ᵇ_)
open import Data.Bool using (true ; false)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Negation using (contradiction)

foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true  = 123
... | false = 456

bar : ℕ → ℕ → ℕ
bar n1 n2 with n1 ≡ᵇ n2
... | true  = 123
... | false = 456

那么，ℕ 的简单出路是什么？我们在 n 上进行模式匹配/案例拆分以减少 n ≡ᵇ n 刚好 来进行我们的证明。即，要么到基本情况零，要么到下一个递归步骤suc n。

bar-eq⇒123 : ∀ n → bar n n ≡ 123
bar-eq⇒123 zero    = refl
bar-eq⇒123 (suc n) = bar-eq⇒123 n

ℕ 只有两个构造函数，我们知道 ≡ᵇ 是什么样子，所以模式匹配很简单。

对于Char，事情要复杂得多。长话短说，Char 的相等性测试是根据函数 toℕ 定义的，Agda 没有给我们定义。此外，Char 数据类型是假设的，没有任何构造函数。所以像 bar-eq⇒123 这样的证明不是 Char 的选项。我们没有子句，也没有构造函数。 (我不会将 'a' 称为 Char 的构造函数。类似于 1234 不是 的构造函数ℕ.)

那么，我们可以做什么？请注意，您引用的错误消息中的 c == c 简化为涉及 isYes 的相当复杂的内容。如果我们将 c == c 减少一点点(而不是尽可能多)，我们会得到 isYes (c ≟ c)(而不是复杂的错误消息中的内容)。

_≟_ 是 Char 的可判定相等性(即“是否相等？” bool 值和证明的组合)。 isYes 去掉证明并给我们 bool 值。

我的证明想法是不对 c 进行案例拆分(就像我们对 ℕ 所做的那样)，而是对 c ≟ c。这将产生两种情况，并将 isYes 分别减少为 true 或 false。 true 的情况很明显。 false 案例可能会因与可判定等式的证明相矛盾而被驳回。

foo-eq⇒123 : ∀ c → foo c c ≡ 123
foo-eq⇒123 c with c ≟ c
... | yes p = refl
... | no ¬p = contradiction refl ¬p

请注意，反过来，此证明不容易转换为 ℕ，因为 _≡ᵇ_ 不是基于可判定的相等性并且 isYes。它是原始的。

对于 Char 和 ℕ ，而不是使用 _==_，也许更好的想法是始终坚持可判定的相等性> 或 _≡ᵇ_。 foo 将如下所示。

baz : Char → Char → ℕ
baz c1 c2 with c1 ≟ c2
... | yes p = 123
... | no ¬p = 456

foo-eq⇒123 证明将适用于它不变。