gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-05 01:50:50 27 4
gpt4 key购买 nike

我有这样一个函数:

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 定理的正确方法是什么?

最佳答案

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

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

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

让我们再次查看您的示例,并添加一个基于 foobar 版本。

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 分别减少为 truefalsetrue 的情况很明显。 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 证明将适用于它不变。

关于agda - 如何告诉 Agda 展开一个定义来证明等价性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/72793516/

27 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com