14

首先是一些无聊的导入：

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)

现在假设我有一个类型，例如由 naturals 索引。

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
4

1 回答 1

13

这些管道表示归约在等待相关表达式的结果之前被暂停，通常归结为您有一个with块，您需要知道其结果才能继续。这是因为该rewrite构造只是扩展为with所讨论的表达式的 a 以及使其工作可能需要的任何辅助值，然后是匹配 on refl。

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

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

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

然后您将其f称为表达式，您将获得a仅针对表达式观察到的管道，因为它匹配 on someDataConstructor，因此至少要f减少您需要引入a然后someDataConstructor从中匹配 on 。另一方面，band c，虽然它们是在 with 块中引入的，但不要停止评估，因为b不匹配模式，并且c'ssomeRecordConstructor被静态地知道是唯一可能的构造函数，因为它是带有 eta 的记录类型。

于 2012-09-19T18:46:23.057 回答