Is this the right way to use HeterogeneousEquality in Agda?

Question

The code below captures my question.

My intention is to create a P of Vec N (suc n) from a P of Vec N (n + 1). My experience with the subst of Propositional Equality tells me this should be the way to do it.

open import Relation.Binary.HeterogeneousEquality
postulate
  n : ℕ
  xs : Vec ℕ (n + 1)
  ys : Vec ℕ (suc n)
  eq : xs ≅ ys
data P : ∀ {n} → Vec ℕ n → Set where

lemma : P xs → P ys
lemma h = subst (λ i → P i) eq h

Obviously lemma doesn't type check because (n + 1) and (suc n) are not the same Nat.

Am I using HeterogeneousEquality correctly? If not, what is a proper way to substitute Vec N (n+1) by Vec N (suc n)?

Answer 1

Another solution, based on rewriting. Note that you'll have to make the postulate parameters.

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.HeterogeneousEquality

data P : ∀ {n} → Vec ℕ n → Set where

lemma :
  (n : ℕ)
  (xs : Vec ℕ (n + 1))
  (ys : Vec ℕ (suc n))
  (eq : xs ≅ ys)
   → P xs → P ys
lemma n xs ys eq h rewrite +-comm 1 n = subst (λ i → P i) eq h

You can also get rid of subst by dependent pattern matching:

lemma n xs ys rewrite +-comm n 1 = \ { refl h -> h }

Answer 2

Here's one solution to your problem:

open import Data.Nat using (ℕ ; zero ; suc ; _+_)
open import Data.Product using (Σ-syntax ; _,_ ; proj₁ ; proj₂)
open import Data.Vec using (Vec)
open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_ ; refl)


n+1≡Sn : ∀ n → n + 1 ≡ suc n
n+1≡Sn zero = refl
n+1≡Sn (suc n) = ≡.cong suc (n+1≡Sn n)


isubst : ∀ {la lp lq} {A : Set la} {P : A → Set lp} (Q : ∀ a → P a → Set lq)
  → ∀ {a a′}
  → a ≡ a′
  → {p : P a} {p′ : P a′}
  → p ≅ p′
  → Q a p
  → Q a′ p′
isubst Q refl refl h = h


postulate
  n : ℕ
  xs : Vec ℕ (n + 1)
  ys : Vec ℕ (suc n)
  eq : xs ≅ ys
  P : ∀ n → Vec ℕ n → Set


lemma : P (n + 1) xs → P (suc n) ys
lemma h = isubst P (n+1≡Sn n) eq h

The trick (bottled up in isubst) is that we're 'unifying' the types of xs and ys before eliminating eq.

As a general comment: I've always found heterogeneous equality more trouble than it's worth. You may want to investigate alternatives before committing to it.