如何告诉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 c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c c 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 is true true 代码>对于所有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类型有点奇怪。让我们将其与非weird内置类型（）对比。 的平等测试如下。

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

请注意，n程n也不简化为true。毕竟，AGDA不知道n是Zero或suc> 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> char的构造函数与1234的方式相似，不是的构造函数ℕ。）

那么，我们可以做什么？请注意，在错误消息中，您引用的c == c简化为涉及isyes的相当复杂的事物。如果我们减少了c == c只有一个小一点（而不是尽可能多），我们将获得isyes（c≟C）（而不是复杂的来自错误消息的事情）。

_≟_是char的可决定性平等（即，“相等或不相等？”布尔值和证明的组合）。 isyes剥离了证明，并给了我们布尔值。

然后，我的证明想法是不要在c上进行案例（就像我们为>>），而是在c≟C上进行。 。这将产生两种情况，并将isyes分别降低到分别为 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

请注意，此证明不容易转化为，因为_ cod>_º_不是基于可决定的等式和iSyes> 。这是原始的。

也许一个更好的想法是始终坚持可决定的平等，因为char以及，而不是使用_ == _或<代码> _防_ 。 foo然后看起来如下。

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

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