Congruence Rule with Heterogeneous Equality in Agda

Congruence rule plays an important role in reasoning in Agda, and things become mystery as working under heterogeneous equality. In the standard library of Agda2, the type of Relation.Binary.HeterogeneousEquality.cong is

∀{a b} (f : a → b) {i : a} {j : a} → i ≅ j → f i ≅ f j

Since i and j are the same type, the equality between i and j becomes propositional instead of heterogeneous. The strength of this function is weaker than the expected, so we could not reley on it to prove the following properties,

Given vectors xs, ys, and zs, prove xs ++ (ys ++ zs) ≅ (xs ++ ys) ++ zs.

It’s quite easy to prove it by induction regardless of their length, and it could be proved that if terms are the same, they have the same length. However, if we try to prove it by HetEq.cong, we will find the type checker complain that

the type of (xs ++ (ys ++ zs)) is different from (xs ++ ys) ++ zs where (xs ++ (ys ++ zs)) is of length n + (m + l) and (xs ++ ys) ++ zs is of length (n + m) + l.

Without the proof of associativity, the type checker could not unify these two terms. Wait ! Do we need to prove it ? No! What we have to do is to use the benefits of heterogeneous equality – the equality between two different types.

We could construct a congruence rule for the constructor of the vector type, that is,

∷-cong : ∀ {a n m}{x : a}{xs : Vec a n}{ys : Vec a m} → xs ≅ ys → x ∷ xs ≅ x ∷ ys
∷-cong refl = refl

We may refine it a bit with different head elements, but it is enough. Then, the proof becomes as simple as the version of list.

lem₁ : ∀ {a n m l}(xs : Vec a n)(ys : Vec a m)(zs : Vec a l) → xs ++ ys ++ zs ≅ (xs ++ ys) ++ zs
lem₁ [] _ _ = refl
lem₁ (x ∷ xs) ys _ = ∷-cong (lem₁ xs ys _)

Thus, we have worked around the different types. A further interesting application is, we could prove the associativity by extracting the lengths. First, we prove that if two vectors are heterogeneously equal, then the lengths are the same as following,

len-eq : ∀ {a n m}{xs : Vec a n}{ys : Vec a m} → xs ≅ ys → n ≡ m
len-eq refl = refl

and we prove the associativity by applying lem₁.

lem₂ : ∀ {n m l a}{xs : Vec a n}{ys : Vec a m}{zs : Vec a l} → n + (m + l) ≡ (n + m) + l
lem₂ {n} {m} {l} {a} {xs} {ys} {zs} = len-eq (lem₁ xs ys zs)

What a magic !?


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s