如何告诉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是truec:

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刚好足够来做我们的证明。即，要么到基本情况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的相等性测试是根据Agda没有给我们定义的函数toℕ来定义的。此外，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证明将不变地适用于它。