Types containing with/rewrite clauses in agda, or, how to use rewrite instead of subst?

Question

First some boring imports:

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)

Now suppose that I have a type indexed by, say, the naturals.

postulate Foo : ℕ -> Set

And that I want to prove some equalities about functions operating on this type Foo. Because agda is not very smart, these will be heterogeneous equalities. A simple example would be

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 !}

The goal in bar is

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

What are these |s doing in the goal? And how do I even begin to construct a term of this type?

In this case, I can work around the problem by manually doing the substitution with subst, but that gets really ugly and tedious for larger types and equations.

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

Those pipes indicate that reduction is suspended pending the result of the expressions in question, and it typically boils down to the fact that you had a with block whose result you need to know to proceed. This is because the rewrite construct just expands to a with of the expression in question along with any auxiliary values that might be needed to make it work, followed by a match on refl.

In this case, it just means that you need to introduce the +-comm n m in a with block and pattern match on refl (and you'll probably need to bring n + m into scope too, as it suggests, so the equality has something to talk about). The Agda evaluation model is fairly straightforward, and if you pattern match on something (except for the faux pattern matches on records), it won't reduce until you pattern match on that same thing. You might even be able to get away with rewriting by the same expression in your proof, since it just does what I outlined for you.

More precisely, if you define:

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

and then you refer to f as an expression, you will get the pipes you observed for expression a only, because it matches on someDataConstructor, so at the very least to get f to reduce you will need to introduce a and then match on someDataConstructor from it. On the other hand, b and c, although they were introduced in the same with block, do no halt evaluation, because b doesn't pattern match, and c's someRecordConstructor is known statically to be the only possible constructor because it's a record type with eta.