Working with heterogeneous equality, a fully-indexed queue is almost simple as a simple typed queue. What we have to do is to prove the properties of vectors, and use the substitution rule to convert the type.

Let’s begin with the definition of Queue.

data Queue (a : Set) : {n : ℕ} → Vec a n → Set where

qu : {n : ℕ} → (fs : Vec a n) → {m : ℕ} → (rs : Vec a m) → Queue a (fs ++ reverse rs)

The index reveals the actual contents of the queue, and it does not matter how it is constructed. For example, `qu (3 ∷ 4 ∷ []) []`

equals to `qu [] (4 ∷ 3 ∷ [])`

.

As I have explained in previous post, the type of HetEq.cong is not correct, and it is the same as HetEq.subst. Therefore, we define a specific version of substitution rule for Queue.

`subst-queue : ∀ {a}{n m}{xs : Vec a n}{ys : Vec a m} → xs ≅ ys → Queue a xs → Queue a ys`

subst-queue refl xs = xs

Then, we could define the type of “pop” as following,

pop : ∀ {a n m}{xs : Vec a n} → Queue a xs → (pf : n ≅ suc m) → Queue a (init xs pf) × a

where init is the function extracting all the element but the head in the list with a proof that the vector, xs, is of length greater then 0. The index shows what the contents should be after poping. Then, …

`pop (qu [] []) ()`

pop (qu (x ∷ xs) rs) refl = (qu xs rs) , x

pop (qu [] (x ∷ xs)) refl = (subst-queue (xs++[]=xs _) (qu (init xsʳ refl) [])) , head xsʳ

where xsʳ = reverse (x ∷ xs)

First of all, the case of empty queue is impossible which is guaranteed by the proof of the length. Second, if we have a non-empty front part, we could just extract it, and the property holds directly by the definition of init. Finally, if the the front part is empty, we have to reverse the rear part and init it. However, it almost trivially holds since the type results `Queue a (xsʳ ++ [])`

, and what we need is `Queue a (xsʳ)`

.

Next, we define the type of “push”.

`push : ∀ {a n} → {xs : Vec a n} → (x : a) → Queue a xs → Queue a (xs ++ [ x ])`

The type ensures the FIFO property. Then, all we have to do is to prove that `(fs ++ reverse rs) ++ [ x ] = fs ++ reverse (x ∷ rs)`

.

`push {a} x (qu fs rs) = (subst-queue (sym (trans lem₁ lem₂)) (qu fs (x ∷ rs)))`

where

lem₁ : (fs ++ reverse rs) ++ [ x ] ≅ fs ++ (reverse rs ++ [ x ])

lem₁ = ++-assoc fs (reverse rs) [ x ]

lem₂ : fs ++ (reverse rs ++ [ x ]) ≅ fs ++ (reverse (x ∷ rs))

lem₂ = ++-cong {xs = fs} refl (sym $ reverse-concat x rs)

Here, the proof, `reverse-concat`

, is easy if you generalize the question appropriately.