Agda: Why am I unable to pattern match on refl?

Question

I'm trying to prove things about divisibility on integers. First I tried to prove that divisibility is reflective.

∣-refl : ∀{n} → n ∣ n

Because I defined divisibility based on subtraction...

data _∣_ : ℤ → ℤ → Set where
  0∣d : ∀{d} → zero ∣ d
  n-d∣d : ∀{n d} → (n - d) ∣ d → n ∣ d

...it seems easy if I use the fact that n-n=0:

∣-refl {n} with n-n≡0 n 
... | refl = n-d∣d 0∣d

But Agda rejects to pattern match on refl. Even if there is no possible other normal form of n-n=0 n. I've proven this with an other function. I just have to use the fact that n-n=0.

C:\Users\ebolnme\Desktop\agda\Integers.agda:118,7-11
n + neg n != zero of type ℤ
when checking that the pattern refl has type n + neg n ≡ zero

Notes:

• a - b is defined by a + (neg b)
• I've already proven n-n≡0 : (n : ℤ) → n - n ≡ zero

Answer 1

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