如何告诉 Agda 展开定义以证明等价性

Question

我有一个这样的函数：

\n

open import Data.Char\nopen import Data.Nat\nopen import Data.Bool\nopen import Relation.Binary.PropositionalEquality\nopen Relation.Binary.PropositionalEquality.\xe2\x89\xa1-Reasoning\n\nfoo : Char \xe2\x86\x92 Char \xe2\x86\x92 \xe2\x84\x95\nfoo c1 c2 with c1 == c2\n... | true = 123\n... | false = 456\n

\n

我想证明，当我用相同的参数（foo c c）调用它时，它总是会产生123：

\n

foo-eq\xe2\x87\x92123 : \xe2\x88\x80 (c : Char) \xe2\x86\x92 foo c c \xe2\x89\xa1 123\nfoo-eq\xe2\x87\x92123 c =\n  foo c c \xe2\x89\xa1\xe2\x9f\xa8 {!!} \xe2\x9f\xa9\n  123 \xe2\x88\x8e\n

\n

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

\n

foo-example : foo 'a' 'a' \xe2\x89\xa1 123\nfoo-example = refl\n

\n

所以，我认为我可以把这refl个洞放进去，因为 Agda 需要做的就是 beta-reduce foo c c。但是，用 替换孔会refl产生以下错误：

\n

.../Unfold.agda:15,14-18\n(foo c c\n | Relation.Nullary.Decidable.Core.isYes\n   (Relation.Nullary.Decidable.Core.map\xe2\x80\xb2 Data.Char.Properties.\xe2\x89\x88\xe2\x87\x92\xe2\x89\xa1\n    Data.Char.Properties.\xe2\x89\x88-reflexive\n    (Relation.Nullary.Decidable.Core.map\xe2\x80\xb2\n     (Data.Nat.Properties.\xe2\x89\xa1\xe1\xb5\x87\xe2\x87\x92\xe2\x89\xa1 (to\xe2\x84\x95 c) (to\xe2\x84\x95 c))\n     (Data.Nat.Properties.\xe2\x89\xa1\xe2\x87\x92\xe2\x89\xa1\xe1\xb5\x87 (to\xe2\x84\x95 c) (to\xe2\x84\x95 c)) (T? (to\xe2\x84\x95 c \xe2\x89\xa1\xe1\xb5\x87 to\xe2\x84\x95 c)))))\n!= 123 of type \xe2\x84\x95\nwhen checking that the expression refl has type foo c c \xe2\x89\xa1 123\n

\n

我怀疑问题是 Agda 不会自动理解这c == c适用true于所有人c：

\n

c==c : \xe2\x88\x80 (c : Char) \xe2\x86\x92 (c == c) \xe2\x89\xa1 true\nc==c c = refl\n

\n

.../Unfold.agda:23,10-14\nRelation.Nullary.Decidable.Core.isYes\n(Relation.Nullary.Decidable.Core.map\xe2\x80\xb2 Data.Char.Properties.\xe2\x89\x88\xe2\x87\x92\xe2\x89\xa1\n Data.Char.Properties.\xe2\x89\x88-reflexive\n (Relation.Nullary.Decidable.Core.map\xe2\x80\xb2\n  (Data.Nat.Properties.\xe2\x89\xa1\xe1\xb5\x87\xe2\x87\x92\xe2\x89\xa1 (to\xe2\x84\x95 c) (to\xe2\x84\x95 c))\n  (Data.Nat.Properties.\xe2\x89\xa1\xe2\x87\x92\xe2\x89\xa1\xe1\xb5\x87 (to\xe2\x84\x95 c) (to\xe2\x84\x95 c)) (T? (to\xe2\x84\x95 c \xe2\x89\xa1\xe1\xb5\x87 to\xe2\x84\x95 c))))\n!= true of type Bool\nwhen checking that the expression refl has type (c == c) \xe2\x89\xa1 true\n

\n

那么，证明我的定理的正确方法是什么foo-eq\xe2\x87\x92123？

\n

Answer 1

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

\n

_\xe2\x89\xa1\xe1\xb5\x87_ : Nat \xe2\x86\x92 Nat \xe2\x86\x92 Bool\nzero  \xe2\x89\xa1\xe1\xb5\x87 zero  = true\nsuc n \xe2\x89\xa1\xe1\xb5\x87 suc m = n \xe2\x89\xa1\xe1\xb5\x87 m\n_     \xe2\x89\xa1\xe1\xb5\x87 _     = false\n

\n

请注意，也n \xe2\x89\xa1\xe1\xb5\x87 n不会减少为true。毕竟，Agda 不知道niszero或suc，即应用两个子句中的哪一个来减少。所以，这和你的例子有同样的问题Char。但因为\xe2\x84\x95有一个简单的出路。

\n

让我们再次查看您的示例，并添加\xe2\x84\x95基于 - 的版本foo，bar。

\n

open import Data.Char using (Char ; _==_ ; _\xe2\x89\x9f_)\nopen import Data.Nat using (\xe2\x84\x95 ; zero ; suc ; _\xe2\x89\xa1\xe1\xb5\x87_)\nopen import Data.Bool using (true ; false)\nopen import Relation.Binary.PropositionalEquality using (_\xe2\x89\xa1_ ; refl)\nopen import Relation.Nullary using (yes ; no)\nopen import Relation.Nullary.Negation using (contradiction)\n\nfoo : Char \xe2\x86\x92 Char \xe2\x86\x92 \xe2\x84\x95\nfoo c1 c2 with c1 == c2\n... | true  = 123\n... | false = 456\n\nbar : \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 \xe2\x84\x95\nbar n1 n2 with n1 \xe2\x89\xa1\xe1\xb5\x87 n2\n... | true  = 123\n... | false = 456\n

\n

那么，有什么简单的出路呢\xe2\x84\x95？我们进行模式匹配/进行案例分割，n以减少n \xe2\x89\xa1\xe1\xb5\x87 n 足以进行证明的量。即，要么到基本情况zero，要么到下一个递归步骤suc n。

\n

bar-eq\xe2\x87\x92123 : \xe2\x88\x80 n \xe2\x86\x92 bar n n \xe2\x89\xa1 123\nbar-eq\xe2\x87\x92123 zero    = refl\nbar-eq\xe2\x87\x92123 (suc n) = bar-eq\xe2\x87\x92123 n\n

\n

\xe2\x84\x95只有两个构造函数，我们知道它\xe2\x89\xa1\xe1\xb5\x87是什么样子，所以模式匹配很简单。

\n

对于 来说Char，事情要复杂得多。长话短说，相等性测试Char是根据to\xe2\x84\x95Agda 没有给我们定义的函数来定义的。此外，Char数据类型是假定的，并且不带有任何构造函数。所以像这样的证明bar-eq\xe2\x87\x92123不是 的一个选择Char。我们没有子句，也没有构造函数。（比如说，我不会调用 的'a'构造函数Char。类似于 how1234不是 的构造函数\xe2\x84\x95类似。）

\n

那么，我们能做什么呢？请注意，c == c您引用的错误消息简化为涉及isYes. 如果我们只减少c == c一点点（而不是尽可能多），我们就会得到isYes (c \xe2\x89\x9f c)（而不是错误消息中的复杂内容）。

\n

_\xe2\x89\x9f_是可判定的相等性Char（即“是否相等？”布尔值和证明的组合）。isYes去掉证明并给我们布尔值。

\n

我的证明想法是不要在 上进行案例分割c（就像我们对 所做的那样\xe2\x84\x95），而是在 上进行案例分割c \xe2\x89\x9f c。这将产生两种情况并分别减少isYes到true或false。这个true案子就很明显了。该案false可以通过与可判定等式的证明相矛盾来解决。

\n

foo-eq\xe2\x87\x92123 : \xe2\x88\x80 c \xe2\x86\x92 foo c c \xe2\x89\xa1 123\nfoo-eq\xe2\x87\x92123 c with c \xe2\x89\x9f c\n... | yes p = refl\n... | no \xc2\xacp = contradiction refl \xc2\xacp\n

\n

请注意，反过来，这个证明也不容易转化为\xe2\x84\x95，因为_\xe2\x89\xa1\xe1\xb5\x87_它不是基于可判定的等式 和isYes。相反，它是一个原始的。

\n

也许更好的想法是始终坚持可判定的相等性， forChar以及\xe2\x84\x95而不是使用_==_or _\xe2\x89\xa1\xe1\xb5\x87_。foo然后将如下所示。

\n

baz : Char \xe2\x86\x92 Char \xe2\x86\x92 \xe2\x84\x95\nbaz c1 c2 with c1 \xe2\x89\x9f c2\n... | yes p = 123\n... | no \xc2\xacp = 456\n

\n

并且foo-eq\xe2\x87\x92123证明将不变地适用于它。

\n