Question

Conor McBride defined the no-confusion property of Nat on page 11 of A Polynomial Testing Principle as:

1
2
3
4
5

NoConf : Nat → Nat → Set
NoConf ze ze = 1
NoConf ze (su y) = 0
NoConf (su x ) ze = 0
NoConf (su x ) (su y) = x ≡ y

Why was this defined that way, rather than the following way which works without dependencies?

1
2
3
4
5

NoConf : Nat → Nat → Set
NoConf ze ze = 1
NoConf ze (su y) = 0
NoConf (su x) ze = 0
NoConf (su x) (su y) = NoConf x y

Context

I still had this question quite near the end of my working through A Polynomial Testing Principle, and it didn’t seem to have been answered: I managed to get through most of the paper without serious problems arising from my different definition.

Answer

Conor immediately follows the definition of NoConf by defining a canonical way to construct a NoConf:

1
2
3

noConf : {x y : Nat} -> x ≡ y → NoConf x y
noConf {zero} refl = record {}
noConf {suc n} {.(suc n)} refl = refl

If you do it my way instead, you end up unable to use this canonical construction to do proofs by no-confusion. You probably find yourself proving that succ is injective manually, and then using that directly instead of via the NoConf; which defeats the entire purpose of packaging up the no-confusion property into a type.

For example:

1
2
3

+cancel : (a b : Nat) {c d : Nat} -> a ≡ b -> (a + c) ≡ (b + d) -> c ≡ d
+cancel zero .zero refl sums_equal = sums_equal
+cancel (succ a) (succ .a) refl sums_equal = +cancel a a refl {!!}

What should go here? We need something of type a + c ≡ a + d, but all we have in scope is the input succ (a + c) ≡ succ (a + d). That is, we need the no-confusion property for succ; which suggests that NoConf should somehow contain an equality type, so that we can use it!

Commentary

I think I only had this question because Nat is such a simple type. If there were more constructors and more cases in each pattern-match, it would have been obvious straight away that I had deleted the entire point of the NoConf construction.