如何告诉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所需要做的就是减少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是true for all c

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示例有相同的问题。但对于ℕ来说，有一条简单的出路。

让我们再次查看您的示例，并添加ℕ-based版本的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，以完成我们的证明。也就是说，要么用大小写zero，要么到下一个递归步骤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的可判定等式(即“等于还是不等于？”)布尔值和证明)。isYes去掉了证明并给出了布尔值。

那么，我对证据的想法将不是在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证明对它也没有影响。