在agda中包含/ 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一个记录类型.