The equality proof has nothing to talk about. When you pattern match on a constructor, it can refine other arguments (and their types). In your case, n-n≡0 n
should refine n - n
, but there's no such expression and Agda gives you this (a bit puzzling) error message.
You can fix that by introducing the expression in a with
:
∣-refl : ∀ {n} → n ∣ n
∣-refl {n} with n - n | n-n≡0 n
... | ._ | refl = ?
We can be more explicit about the left hand side, this nicely shows how the refinement happens:
∣-refl {n} with n - n | n-n≡0 n
∣-refl {n} | .zero | refl = ?
However, when you try to fill in the rest of the definition:
∣-refl {n} with n - n | n-n≡0 n
∣-refl {n} | .zero | refl = n-d∣d 0∣d
The type checker disagrees yet again. Why is that so? n-d∣d
should have a type (n - n) ∣ n → n ∣ n
and 0∣d
has a type 0 ∣ n
. But wait! Didn't we just show that n - n
is, in fact, 0
?
The thing with pattern matching and the refining it causes is that it happens only once, the right hand side won't be affected by it, at all (this is, by the way, one of the reasons we have the inspect
machinery). How do we deal with it?
There's a function called subst
that takes something of type P a
, a proof that a ≡ b
and gives us P b
. Notice that if we substitute λ x → x ∣ n
for P
, zero
for a
and n - n
for b
, we get a function that takes zero ∣ n
and gives us n - n ∣ n
(for suitable proof, of course).
And indeed:
∣-refl {n} = n-d∣d (subst (λ x → x ∣ n) (sym (n-n≡0 n)) 0∣d)
This definition is accepted: the type of subst ... 0∣d
is n - n ∣ n
, which is suitable input for n-d∣d
. Notice that we also needed a proof that zero ≡ n - n
, but we have n - n ≡ zero
- here we use the fact that ≡
is symmetric (sym
).
For completeness' sake, here's the definition of subst
:
subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y} →
x ≡ y → P x → P y
subst _ refl p = p