Overcoming definitional equality issues when constructing basic Agda functions

Question

I'm trying to write a reverse vector function in agda, and am running into the following stumbling block

Goal: Vec Nat (suc n)
Have: Vec Nat (n +N 1)

If I understand correctly, these values aren't definionally equal. Here is the reverse function.

vReverse : {X : Set} {n : Nat} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = {!(vReverse x₁) +V (x ,- [])!}

How can I overcome this, if possilbe, without refactoring the code. If a refactor is necessary, how can one generally avoid these pitfalls a priori? Here is the rest of the code.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_   -- the "cons" operator associates to the right

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V xs = xs
(x ,- xs) +V [] = x ,- xs +V []
(x ,- xs) +V x₁ ,- ys = x ,- xs +V x₁ ,- ys

You define [`foldl`](https://github.com/agda/agda-stdlib/blob/041fd896be22045262fb5d53ef10fc779f827bcc/src/Data/Vec/Base.agda#L184-L189) over `Vec` and then use it for defining [`reverse`](https://github.com/agda/agda-stdlib/blob/041fd896be22045262fb5d53ef10fc779f827bcc/src/Data/Vec/Base.agda#L270-L271). See these [question and answer](https://stackoverflow.com/questions/33345899/how-to-enumerate-the-elements-of-a-list-by-fins-in-linear-time) for how to derive such a strategy. — effectfully, May 19 '20 at 17:40
Prove `suc n == n +N 1` and `rewrite` or transport using `x == y -> A x -> A y` — Sassa NF, May 21 '20 at 08:38

score 1 · Answer 1 · answered May 22 '20 at 13:24

The idea is that you can transform an element of type P x into an element of type P y provided you can prove x ≡ y. Let me guide you through this process step by step. Here is the base code you provided, which I have not refactored as you requested.

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat     -- recursive data type

{-# BUILTIN NATURAL Nat #-}

_+N_ : Nat -> Nat -> Nat
zero  +N y = y
suc x +N y = suc (x +N y)      -- there are other choices

infixl 5 _+N_

data Vec (X : Set) : Nat -> Set where  -- like lists, but length-indexed
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

infixr 4 _,-_   -- the "cons" operator associates to the right

However, your concatenation function was incorrect and it didn't terminate so here is the corrected version.

_+V_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m +N n)
[] +V vs = vs
(x ,- xs) +V vs = x ,- (xs +V vs)

The reason why we don't need to do any substitution in this function is because suc n + m is definitionally equal to suc (n + m).

Since you've defined your own naturals and your own addition, I'm assuming you want to redefine everything by yourself. According to this assumption, you'll need to define propositional equality, which is done as follows:

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

infix 1 _≡_

From this definition, we can define the substitution that was mentioned in the preamble of this answer, as well as in a comment of your question:

subst : ∀ {a b} {A : Set a} {x y : A} (P : A → Set b) → x ≡ y → P x → P y
subst _ refl p = p

In your reverse function, the problem lies in the fact that n + 1 is not definitionally equal to suc n. Which is why we need a property to establish this fact, which we can then feed to our substitution mechanism. This proof requires the congruence of the propositional equality we defined, as follows:

cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong _ refl = refl

n+1≡sn : ∀ {n} → n +N 1 ≡ suc n
n+1≡sn {zero} = refl
n+1≡sn {suc _} = cong suc n+1≡sn

We now have all the required elements to write your vReverse function:

vReverse : ∀ {X n} → Vec X n → Vec X n
vReverse [] = []
vReverse (x ,- x₁) = subst (Vec _) n+1≡sn ((vReverse x₁) +V (x ,- []))

To go Further, you can use the same process to build the usual reverse function which is more efficient (linear complexity). I took the liberty to do this for you, since it shows more examples of usage of subst.

n+sm≡sn+m : ∀ {n m} → n +N suc m ≡ suc (n +N m)
n+sm≡sn+m {zero} = refl
n+sm≡sn+m {suc _} = cong suc n+sm≡sn+m

reverse-better-aux : ∀ {X n m} → Vec X n → Vec X m → Vec X (n +N m)
reverse-better-aux [] v₂ = v₂
reverse-better-aux (x ,- v₁) v₂ = subst (Vec _) n+sm≡sn+m (reverse-better-aux v₁ (x ,- v₂))

n+0≡n : ∀ {n} → n +N 0 ≡ n
n+0≡n {zero} = refl
n+0≡n {suc _} = cong suc n+0≡n

reverse-better : ∀ {X n} → Vec X n → Vec X n
reverse-better v = subst (Vec _) n+0≡n (reverse-better-aux v [])

Overcoming definitional equality issues when constructing basic Agda functions

1 Answers1