Типы, содержащие с /rewrite предложения в agda, или, как использовать переписать вместо subst?

Сначала некоторые скучные импорта:

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

Ответ 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.