关于使用 rewrite 的函数的证明：一个 "vertical bars in goals" 问题
Proof about a function that uses rewrite: a "vertical bars in goals" question
我有一个函数使用 rewrite 来满足 Agda 类型检查器的要求。我认为我对如何处理此类函数的证明中的结果 "vertical bars" 有相当好的把握。然而，在我看似简单的情况下，我完全无法处理这些酒吧。
这是导入和我的函数，step。 rewrite 使 Agda 分别看到 n 等于 n + 0 和 suc (acc + n) 等于 acc + suc n。
module Repro where
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Core
open import Data.Nat.Properties
open import Agda.Builtin.Nat using () renaming (mod-helper to modₕ)
step : (acc d n : ℕ) → modₕ acc (acc + n) d n ≤ acc + n
step zero d n rewrite P.sym (+-identityʳ n) = a[modₕ]n<n n (suc d) 0
step (suc acc) d n rewrite P.sym (+-suc acc n) = a[modₕ]n<n acc (suc d) (suc n)
现在来证明，哪个模式在 acc 上匹配，就像函数一样。这是 zero 案例：
step-ok : ∀ (acc d n : ℕ) → step acc d n ≡ a[modₕ]n<n acc d n
step-ok zero d n with n | P.sym (+-identityʳ n)
step-ok zero d n | .(n + 0) | P.refl = ?
在这一点上，Agda 告诉我我不确定构造函数是否应该有一个案例P.refl，因为我在尝试解决以下统一问题时卡住了 (推断指数 ≟ 预期指数）：w ≟ w + 0 [...]
我也陷入了第二种情况，即 suc acc 的情况，尽管方式不同：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n)
step-ok (suc acc) d n | .(acc + suc n) | P.refl = ?
在这里，Agda 说 suc (acc + n) != w of type ℕ 在检查生成的 with 函数的类型 [...] 是否合式时
Sassa NF 回复后更新
我听从了 Sassa NF 的建议，用 P.subst 而不是 rewrite 重新表述了我的函数。即，我将右侧从大约 n + 0 更改为大约 n，而不是相反地将目标从大约 n 更改为大约 n + 0：
step′ : (acc d n : ℕ) → modₕ acc (acc + n) d n ≤ acc + n
step′ zero d n = P.subst (λ # → modₕ 0 # d # ≤ #) (+-identityʳ n) (a[modₕ]n<n n (suc d) 0)
step′ (suc acc) d n = P.subst (λ # → modₕ (suc acc) # d n ≤ #) (+-suc acc n) (a[modₕ]n<n acc (suc d) (suc n))
在证明过程中，函数定义中的P.subst需要去掉，可以用with构造来完成：
step-ok′ : ∀ (acc d n : ℕ) → step′ acc d n ≡ a[modₕ]n<n acc d n
step-ok′ zero d n with n + 0 | +-identityʳ n
... | .n | P.refl = P.refl
step-ok′ (suc acc) d n with acc + suc n | +-suc acc n
... | .(suc (acc + n)) | P.refl = P.refl
所以，耶！我刚刚完成了第一个涉及 with.
的 Agda 证明
在原问题上取得了一些进展
我的猜测是我的第一个问题是依赖模式匹配期间的统一问题：没有任何替换使 n 与 n + 0 相同。更一般地说，在一件事是另一件事的严格子项的情况下，我想我们可能 运行 陷入统一麻烦。所以，也许使用 with 来匹配 n 和 n + 0 是自找麻烦。
我的第二个问题似乎是 Agda 语言参考所称的类型错误的with-抽象。根据参考，这个 "happens when you abstract over a term that appears in the type of a subterm of the goal or argument types." 的罪魁祸首似乎是目标子项 a[modₕ]n<n (suc acc) d n 的类型，即 modₕ [...] ≤ (suc acc) + n，其中包含我抽象的子项 (suc acc) + n。
看起来这通常是通过对目标中具有违规类型的部分进行额外抽象来解决的。而且，实际上，以下内容会使错误消息消失：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n
... | .(acc + suc n) | P.refl | rhs = {!!}
到目前为止一切顺利。现在让我们引入 P.inspect 来捕获 rhs 替换：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n | P.inspect (a[modₕ]n<n (suc acc) d) n
... | .(acc + suc n) | P.refl | rhs | P.[ rhs-eq ] = {!!}
不幸的是，这会导致类似于原始错误的错误：w != suc (acc + n) of type ℕ when checking that the type [...] of generated with function is well -形成
一天后
当然，我会 运行 再次进入同样的错误类型 with-abstraction！毕竟P.inspect的全部意义在于保留a[modₕ]n<n (suc acc) d n，这样才能构造出a[modₕ]n<n (suc acc) d n ≡ rhs这个词。然而，preserved a[modₕ]n<n (suc acc) d n 当然仍然保留其原始类型 modₕ [...] ≤ (suc acc) + n，而 rhs 具有修改后的类型 modₕ [...] ≤ acc + suc n。这就是现在造成麻烦的原因。
我想一种解决方案是使用 P.subst 来更改我们检查的术语的类型。而且，事实上，以下作品，尽管它非常令人费解：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n | P.inspect (λ n → P.subst (λ # → modₕ (suc acc) # d n ≤ #) (P.sym (+-suc acc n)) (a[modₕ]n<n (suc acc) d n)) n
... | .(acc + suc n) | P.refl | rhs | P.[ rhs-eq ] rewrite +-suc acc n = rhs-eq
所以，再说一遍！我设法解决了原来的第二个问题——基本上是通过在证明中使用 P.subst 而不是在函数定义中使用。不过，根据 Sassa NF 的指导，在函数定义中使用 P.subst 似乎更可取，因为它会导致代码更加简洁。
统一问题对我来说还是有点神秘，但在积极的一面，我意外地了解到了无关紧要的好处。
我接受 Sassa NF 的回复，因为它让我走上了解决方案的正确轨道。
您使用 P.refl 表示对 _≡_ 的作用存在一些误解。
那种类型没有魔法。它只是一个具有单个构造函数的依赖类型。证明一些 x ≡ y 解析为 P.refl 并没有告诉 Agda 关于 x 和 y 的任何新信息：它只告诉 Agda 你设法产生了类型 _≡_。这就是它无法分辨 n 和 .(n + 0) 是同一事物，或者 suc (acc + n) 与 .(acc + suc n) 相同的原因。所以你看到的两个错误其实是一样的。
现在，rewrite 是干什么用的。
您不能为依赖类型 C _ 定义 C x ≡ C y。 C x 和 C y 是不同的类型。相等性仅针对相同类型的元素定义，因此甚至无法表达 C x 类型的元素与 C y.
类型的元素相当的想法
然而，有一个归纳公理，如果你有一个 C x 类型的元素和一个 x ≡ y 类型的元素，它允许产生 C y 类型的元素.注意类型 _≡_ 没有魔法——也就是说，你可以定义你自己的类型，并构造这样一个函数，Agda 将满足：
induction : {A : Set} {C : (x y : A) -> (x ≡ y) -> Set} (x y : A) (p : x ≡ y) ((x : A) -> C x x refl) -> C x y p
induction x .x refl f = f x
或归纳公理的简化版本：
transport : {A : Set} {C : A -> Set} (x y : A) (x ≡ y) (C x) -> C y
transport x .x refl cx = cx
这在实践中意味着，您获得了某事的证明 - 例如，A x ≡ A x，然后将此证明沿着等式 x ≡ y 传输以获得证明 A x ≡ A y.这通常需要明确指定类型，在本例中为 {C = y -> A x ≡ A y}，并提供 x、y 和 C x。因此，这是一个非常繁琐的过程，尽管学习者会从这些步骤中受益。
rewrite then 是一种句法机制，重写之前已知的术语类型，这样之后就不需要这样的 transport 了。因为它是句法的，所以它确实以一种特殊的方式解释类型 _≡_ （所以如果你定义你自己的类型，你需要告诉 Agda 你正在使用不同的类型作为相等）。重写类型不是 "telling" Agda 认为某些类型是相等的。它只是将类型签名中出现的 x 替换为 y，因此现在您只需要使用 y 和 refl.
构造内容
说了这么多，您就会明白为什么它适用于 step。 rewrite P.sym ... 字面上用 n + 0 替换了所有出现的 n，包括函数的 return 类型，所以现在是 modₕ acc (acc + (n + 0)) d (n + 0) ≤ acc + (n + 0)。然后构建该类型的值就可以了。
然后 step-ok 不起作用，因为您只对值进行模式匹配。没有什么可以说 n 和 (n + 0) 是一回事。但是 rewrite 会。或者您可以使用这样的函数 transport.
我有一个函数使用 rewrite 来满足 Agda 类型检查器的要求。我认为我对如何处理此类函数的证明中的结果 "vertical bars" 有相当好的把握。然而，在我看似简单的情况下，我完全无法处理这些酒吧。
这是导入和我的函数，step。 rewrite 使 Agda 分别看到 n 等于 n + 0 和 suc (acc + n) 等于 acc + suc n。
module Repro where
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Core
open import Data.Nat.Properties
open import Agda.Builtin.Nat using () renaming (mod-helper to modₕ)
step : (acc d n : ℕ) → modₕ acc (acc + n) d n ≤ acc + n
step zero d n rewrite P.sym (+-identityʳ n) = a[modₕ]n<n n (suc d) 0
step (suc acc) d n rewrite P.sym (+-suc acc n) = a[modₕ]n<n acc (suc d) (suc n)
现在来证明，哪个模式在 acc 上匹配，就像函数一样。这是 zero 案例：
step-ok : ∀ (acc d n : ℕ) → step acc d n ≡ a[modₕ]n<n acc d n
step-ok zero d n with n | P.sym (+-identityʳ n)
step-ok zero d n | .(n + 0) | P.refl = ?
在这一点上，Agda 告诉我我不确定构造函数是否应该有一个案例P.refl，因为我在尝试解决以下统一问题时卡住了 (推断指数 ≟ 预期指数）：w ≟ w + 0 [...]
我也陷入了第二种情况，即 suc acc 的情况，尽管方式不同：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n)
step-ok (suc acc) d n | .(acc + suc n) | P.refl = ?
在这里，Agda 说 suc (acc + n) != w of type ℕ 在检查生成的 with 函数的类型 [...] 是否合式时
Sassa NF 回复后更新
我听从了 Sassa NF 的建议，用 P.subst 而不是 rewrite 重新表述了我的函数。即，我将右侧从大约 n + 0 更改为大约 n，而不是相反地将目标从大约 n 更改为大约 n + 0：
step′ : (acc d n : ℕ) → modₕ acc (acc + n) d n ≤ acc + n
step′ zero d n = P.subst (λ # → modₕ 0 # d # ≤ #) (+-identityʳ n) (a[modₕ]n<n n (suc d) 0)
step′ (suc acc) d n = P.subst (λ # → modₕ (suc acc) # d n ≤ #) (+-suc acc n) (a[modₕ]n<n acc (suc d) (suc n))
在证明过程中，函数定义中的P.subst需要去掉，可以用with构造来完成：
step-ok′ : ∀ (acc d n : ℕ) → step′ acc d n ≡ a[modₕ]n<n acc d n
step-ok′ zero d n with n + 0 | +-identityʳ n
... | .n | P.refl = P.refl
step-ok′ (suc acc) d n with acc + suc n | +-suc acc n
... | .(suc (acc + n)) | P.refl = P.refl
所以，耶！我刚刚完成了第一个涉及 with.
在原问题上取得了一些进展
我的猜测是我的第一个问题是依赖模式匹配期间的统一问题：没有任何替换使 n 与 n + 0 相同。更一般地说，在一件事是另一件事的严格子项的情况下，我想我们可能 运行 陷入统一麻烦。所以，也许使用 with 来匹配 n 和 n + 0 是自找麻烦。
我的第二个问题似乎是 Agda 语言参考所称的类型错误的with-抽象。根据参考，这个 "happens when you abstract over a term that appears in the type of a subterm of the goal or argument types." 的罪魁祸首似乎是目标子项 a[modₕ]n<n (suc acc) d n 的类型，即 modₕ [...] ≤ (suc acc) + n，其中包含我抽象的子项 (suc acc) + n。
看起来这通常是通过对目标中具有违规类型的部分进行额外抽象来解决的。而且，实际上，以下内容会使错误消息消失：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n
... | .(acc + suc n) | P.refl | rhs = {!!}
到目前为止一切顺利。现在让我们引入 P.inspect 来捕获 rhs 替换：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n | P.inspect (a[modₕ]n<n (suc acc) d) n
... | .(acc + suc n) | P.refl | rhs | P.[ rhs-eq ] = {!!}
不幸的是，这会导致类似于原始错误的错误：w != suc (acc + n) of type ℕ when checking that the type [...] of generated with function is well -形成
一天后
当然，我会 运行 再次进入同样的错误类型 with-abstraction！毕竟P.inspect的全部意义在于保留a[modₕ]n<n (suc acc) d n，这样才能构造出a[modₕ]n<n (suc acc) d n ≡ rhs这个词。然而，preserved a[modₕ]n<n (suc acc) d n 当然仍然保留其原始类型 modₕ [...] ≤ (suc acc) + n，而 rhs 具有修改后的类型 modₕ [...] ≤ acc + suc n。这就是现在造成麻烦的原因。
我想一种解决方案是使用 P.subst 来更改我们检查的术语的类型。而且，事实上，以下作品，尽管它非常令人费解：
step-ok (suc acc) d n with suc (acc + n) | P.sym (+-suc acc n) | a[modₕ]n<n (suc acc) d n | P.inspect (λ n → P.subst (λ # → modₕ (suc acc) # d n ≤ #) (P.sym (+-suc acc n)) (a[modₕ]n<n (suc acc) d n)) n
... | .(acc + suc n) | P.refl | rhs | P.[ rhs-eq ] rewrite +-suc acc n = rhs-eq
所以，再说一遍！我设法解决了原来的第二个问题——基本上是通过在证明中使用 P.subst 而不是在函数定义中使用。不过，根据 Sassa NF 的指导，在函数定义中使用 P.subst 似乎更可取，因为它会导致代码更加简洁。
统一问题对我来说还是有点神秘，但在积极的一面，我意外地了解到了无关紧要的好处。
我接受 Sassa NF 的回复，因为它让我走上了解决方案的正确轨道。
您使用 P.refl 表示对 _≡_ 的作用存在一些误解。
那种类型没有魔法。它只是一个具有单个构造函数的依赖类型。证明一些 x ≡ y 解析为 P.refl 并没有告诉 Agda 关于 x 和 y 的任何新信息：它只告诉 Agda 你设法产生了类型 _≡_。这就是它无法分辨 n 和 .(n + 0) 是同一事物，或者 suc (acc + n) 与 .(acc + suc n) 相同的原因。所以你看到的两个错误其实是一样的。
现在，rewrite 是干什么用的。
您不能为依赖类型 C _ 定义 C x ≡ C y。 C x 和 C y 是不同的类型。相等性仅针对相同类型的元素定义，因此甚至无法表达 C x 类型的元素与 C y.
然而，有一个归纳公理，如果你有一个 C x 类型的元素和一个 x ≡ y 类型的元素，它允许产生 C y 类型的元素.注意类型 _≡_ 没有魔法——也就是说，你可以定义你自己的类型，并构造这样一个函数，Agda 将满足：
induction : {A : Set} {C : (x y : A) -> (x ≡ y) -> Set} (x y : A) (p : x ≡ y) ((x : A) -> C x x refl) -> C x y p
induction x .x refl f = f x
或归纳公理的简化版本：
transport : {A : Set} {C : A -> Set} (x y : A) (x ≡ y) (C x) -> C y
transport x .x refl cx = cx
这在实践中意味着，您获得了某事的证明 - 例如，A x ≡ A x，然后将此证明沿着等式 x ≡ y 传输以获得证明 A x ≡ A y.这通常需要明确指定类型，在本例中为 {C = y -> A x ≡ A y}，并提供 x、y 和 C x。因此，这是一个非常繁琐的过程，尽管学习者会从这些步骤中受益。
rewrite then 是一种句法机制，重写之前已知的术语类型，这样之后就不需要这样的 transport 了。因为它是句法的，所以它确实以一种特殊的方式解释类型 _≡_ （所以如果你定义你自己的类型，你需要告诉 Agda 你正在使用不同的类型作为相等）。重写类型不是 "telling" Agda 认为某些类型是相等的。它只是将类型签名中出现的 x 替换为 y，因此现在您只需要使用 y 和 refl.
说了这么多，您就会明白为什么它适用于 step。 rewrite P.sym ... 字面上用 n + 0 替换了所有出现的 n，包括函数的 return 类型，所以现在是 modₕ acc (acc + (n + 0)) d (n + 0) ≤ acc + (n + 0)。然后构建该类型的值就可以了。
然后 step-ok 不起作用，因为您只对值进行模式匹配。没有什么可以说 n 和 (n + 0) 是一回事。但是 rewrite 会。或者您可以使用这样的函数 transport.