A Fully-Indexed Queue

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.

Advertisements

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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