agda - agda 中包含 with/rewrite 子句的类型，或者，如何使用 rewrite 而不是 subst？

Question

首先是一些无聊的进口:

import Relation.Binary.PropositionalEquality as PE
import Relation.Binary.HeterogeneousEquality as HE
import Algebra
import Data.Nat
import Data.Nat.Properties
open PE
open HE using (_≅_)
open CommutativeSemiring commutativeSemiring using (+-commutativeMonoid)
open CommutativeMonoid +-commutativeMonoid using () renaming (comm to +-comm)

现在假设我有一个类型索引，比如自然数。

postulate Foo : ℕ -> Set

我想证明在这种类型上运行的函数的一些等式 Foo .因为 agda 不是很聪明，所以这些将是异构的平等。一个简单的例子是

foo : (m n : ℕ) -> Foo (m + n) -> Foo (n + m)
foo m n x rewrite +-comm n m = x

bar : (m n : ℕ) (x : Foo (m + n)) -> foo m n x ≅ x
bar m n x = {! ?0 !}

酒吧的目标是

Goal: (foo m n x | n + m | .Data.Nat.Properties.+-comm n m) ≅ x
————————————————————————————————————————————————————————————
x : Foo (m + n)
n : ℕ
m : ℕ

这些是什么 |目标是什么？我什至如何开始构建这种类型的术语？

在这种情况下，我可以通过手动替换 subst 来解决这个问题。 ，但是对于更大的类型和方程来说，这变得非常丑陋和乏味。

foo' : (m n : ℕ) -> Foo (m + n) -> Foo (n + m)
foo' m n x = PE.subst Foo (+-comm m n) x

bar' : (m n : ℕ) (x : Foo (m + n)) -> foo' m n x ≅ x
bar' m n x = HE.≡-subst-removable Foo (+-comm m n) x

Answer 1

这些管道表示在有问题的表达式的结果之前减少被暂停，这通常归结为你有一个 with 的事实。阻止您需要知道其结果才能继续。这是因为 rewrite构造只是扩展为 with有问题的表达式以及使其工作可能需要的任何辅助值，然后匹配 refl .

在这种情况下，仅意味着您需要引入 +-comm n m在 with块和模式匹配 refl (并且您可能还需要将 n + m 纳入范围，正如它所暗示的那样，因此平等有一些要讨论的内容)。 Agda 评估模型相当简单，如果您对某事物进行模式匹配(记录上的虚假模式匹配除外)，则在对同一事物进行模式匹配之前，它不会减少。你甚至可以在你的证明中用相同的表达式重写，因为它只是做了我为你概述的。

更准确地说，如果您定义:

f : ...
f with a | b | c
...  | someDataConstructor | boundButNonConstructorVariable | someRecordConstructor = ...

然后你引用 f作为表达式，您将获得您观察到的表达式 a 的管道仅，因为它匹配 someDataConstructor ，所以至少要得到 f要减少您将需要引入 a然后匹配 someDataConstructor从中。另一方面， b和 c ，虽然它们是在同一个块中引入的，但不要停止求值，因为 b不匹配模式，并且 c的 someRecordConstructor静态地知道它是唯一可能的构造函数，因为它是带有 eta 的记录类型。