[Agda] Congruence and substitutivity rules in heterogeneous equality

[Liang-Ting Chen]

Hi, all

I found something weird with heterogeneous equality as they confused me for
a while.
Let's start from the definition, the type formation rule is

data _≅_ {a : Set} (x : a) : {b : Set} → b → Set where

it shows that we may have equality between two terms x, y with different
types,
though the introduction rule

  refl : x ≅ x

shows that it holds only if x is provably convertible to y. However, the
type of
congruence and substitutivity rules in Relation.Binary.HeterogeneousEquality
are

cong : ∀ {A : Set} {B : A → Set} {x y} (f : (x : A) → B x) → x ≅ y → f x ≅ f
y

and

subst (P : A → Set) {x : A} {y : A} → x ≅ y → P x → P y, respectively.

Here, the types of element are all the same type, and this restriction
weakens
both function to those in propositional equality.

Thus, if we want to prove the following equality

lem :  ∀ {n A}(xs : Vec A n) → xs ++ [] ≅ xs
lem [] = refl
lem (x ∷ xs) = {! !}

we couldn't use cong (λ ys → x ∷ ys) (lem xs) to prove it since
their types are different - one is Vec A (n + 0) and another one is Vec A n.
Instead, we could prove it by constructing a congruence rule for Vec, 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

and the proof is just "∷-cong (lem xs)". It seems that cong and rule in
HeterogeneousEquality
don't work as I expected. Furthermore, it also breaks the heterogeneous
equational reasoning
for the same reason. Is it possible to construct these two functions
properly for all without
defining particular cong or subst for every indexed type ?

-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090713/8c198e3b/attachment.html