Please upload your solutions on Moodle by Friday, 9 October 2020 at 23:59.

In this week's lab, we have a look at an implementation of amortised queues in Coq. The exercise task itself is not meant to be advanced because you will need to spend substantial time learning Coq itself.

Queues are a collection with FIFO (first-in-first-out) semantics: the least recently added elements are to be removed first. One implementation of such a queue collection, which we will work with in this exercise, is backed by two lists. This implementation of lists supports constant time enqueue operations and amortised constant time dequeue operations.

Recall that a queue allows taking elements from the front and adding elements to the end. Queues are expected to implement these operations in about constant time. Here we are going to implement and prove correct a purely functional queue, which means that it does not use mutation. The benefit is that we can prove such implementations correct much more easily and, moreover, even after adding or removing an element we can continue to access the previous version of the queue. On the flip side, it means that a simple imperative implementation (such as a doubly linked list with a tail pointer) is out of question. Instead, we use functional lists. A simplest functional approach would be to implement dequeue as list head and implement enqueue as appending a single element to the end of the list. Unfortunately, this would make enqueue linear in the size of the queue. Conversely, if we decided to implement dequeue by removing from the end of a list, then the dequeue would take linear time, instead of constant. A solution is instead to use two lists: one for removing and one for adding. When the list from which remove gets empty, we need to add elements from the other list. We do this by reversing the list, which is good on average, because we do it only once for every element we put into the queue.

To help you understand functional queues and their correctness statements, we provide this implementation in Stainless in the repository of Stainless examples called bolts. The example contains three class definitions:

1. First, we define abstract class Queue whose method bodies are only placeholders, but, crucially, contain postconditions that every implementation must obey. These postconditions are specified using toList function, which itself is abstract. Such functions used in specifications are called abstraction function: they map a (possibly complex) implementation into a simpler model (in this case list).
2. As an illustration, SimpleQueue shows a trivial implementation, where toList is an identity function. This gives us the first (inefficient) implementation. Note that, even though SimpleQueue does not contain any specifications, Stainless automatically checks that all postconditions of the superclass hold. (You can test this by trying to make implementation incorrect and examining what happens).
3. Finally, we define our amortized implementation that has a front list and rear list. The toList method gives the meaning of our queue in terms of list: it is meant to represent front ++ rear.reverse. In case of enqueue we provide a proof, using Stainless' equations library, that establishes the postcondition stated in the abstract class.

And now, we turn to Coq specification and implementation. For your convenience, the entire code skeleton can be found on this page.

Instead on relying on the lists that we have defined in the Coq tutorial, you will make use of lists as defined in the standard library. Lists in the library are defined in a similar fashion as we did. Additionally, the library already contains all the lemmas that we have proven in the tutorial.

To import the library, as well as enable a nicer notation for list:

 Require Import Coq.Lists.List.
Import ListNotations.
 

Exercise 1 : Implementation of Amortised Queues

For the first exercise, you are asked to implement the enqueue and dequeue operations on amortised queues. The type queue is defined as a pair of two lists.

 Definition queue (T : Type) : Type := list T * list T.
 

The first list is called the front list and the second list the rear list. The two lists serve different purposes:

• The front list is where elements are taken from by `dequeue` operations.
• The rear list is where elements are added to by `enqueue` operations.

When an elements is to be taken from an empty front list, the rear list is to be reversed and act as the front list.

Part 1 : Implement empty_queue

As a first part, implement a constructor of empty queues.

 Definition empty_queue (T : Type) : queue T :=
  (* TO BE IMPLEMENTED *)
 

Part 2 : Implement enqueue

You should now implement the enqueue function. That function is used to add an element to the queue. In your implementation, you should simply add the element to the front of the rear list.

 Definition enqueue { T } (x : T) (q : queue T) : queue T :=
  (* TO BE IMPLEMENTED *)
 

Part 3 : Implement dequeue

Next, implement the dequeue function, which is used to return the least recently inserted element from the queue. As such an element may not always exist (the queue might be empty), the result of the function should be wrapped in option. When such an oldest element exist, it should be returned along side the queue with that element removed.

Note that the oldest element will either be at the front of the front list, or, when the front list is empty, at the very end of the rear list. When the front list is empty, you should reverse the rear list and use that list as the new front list.

 Definition dequeue { T } (q : queue T) : option (T * queue T) :=
  (* TO BE IMPLEMENTED *)
 

Once you have implemented all three definitions, you may check your implementation with some examples as follows:

 Example q123 : queue nat :=
  let q1 := enqueue 1 (empty_queue nat) in
  let q2 := enqueue 2 q1 in
  let q3 := enqueue 3 q2 in
  q3.

Compute q123.

Compute (dequeue q123).
 

Exercise 2 : Proving Correctness of enqueue and dequeue

The queue can be converted to a list by concatenating the front list and the reversed rear list. This definition will be used to describe the contents of queues in the various lemmas you will have to prove in this exercise.

 Definition toList { T } (q : queue T) : list T := fst q ++ rev (snd q).
 

The elements are returned from least recently enqueued to most recently enqueued. You can see the result of toList on the q123 example queue by issuing the command:

 Compute (toList q123).
 

Part 1 : Correctness of enqueue

As a first theorem, you will have to prove the correctness of the enqueue operation with respect to toList.

 Lemma enqueue_correct:
  forall T (x : T) (q : queue T),
    toList (enqueue x q) = toList q ++ [x].
Proof.
  (* TO BE COMPLETED *)
Qed.
 

Hint: There are some lemmas on lists that are part of the library that you might find useful. In particular, consider app_assoc, which states that the ++ operation on lists is associative. You can check the type of app_assoc using the Check command.

 Check app_assoc.
 

Part 2 : Correctness of dequeue

In the last part of this lab, you will prove the correctness of the dequeue operation. To do so, you will have first have to prove the following four lemmas about dequeue:

 Lemma dequeue_some_sound:
  forall T (x : T) (q q' : queue T),
    dequeue q = Some (x, q') ->
    toList q = x :: toList q'.
Proof.
  (* TO BE COMPLETED *)
Qed.

Lemma dequeue_none_sound:
  forall T (q : queue T),
    dequeue q = None ->
    toList q = [].
Proof.
  (* TO BE COMPLETED *)
Qed.

Lemma dequeue_some_complete:
  forall T (x : T) (xs : list T) (q : queue T),
  toList q = x :: xs ->
  exists (q' : queue T),
    dequeue q = Some (x, q') /\
    toList q' = xs.
Proof.
  (* TO BE COMPLETED *)
Qed.

Lemma dequeue_none_complete:
  forall T (q : queue T),
    toList q = [] ->
    dequeue q = None.
Proof.
  (* TO BE COMPLETED *)
Qed.
 

Note that you may use some of the lemmas in the proofs of others. Indeed, some of the four lemmas are directly implied by others. Feel free to reorder the lemmas if you find it more convenient.

Hint: To prove some of the lemmas, you may find useful to destruct compound expressions. In that case, do not forget to add eqn:Eq to retain an equality on the destroyed compound expression.

Finally, you should prove the following theorems about correctness of dequeue:

 Theorem dequeue_none_correct:
  forall T (q : queue T),
    toList q = [] <->
    dequeue q = None.
Proof.
  (* TO BE COMPLETED *)
Qed.

Theorem dequeue_some_correct:
  forall T (q : queue T) (x : T) (xs : list T),
    toList q = x :: xs <->
    exists (q' : queue T),
      dequeue q = Some (x, q') /\
      toList q' = xs.
Proof.
  (* TO BE COMPLETED *)
Qed.
 

Hint: This last part should be almost immediate given the four previously proven lemmas.

Once you've proven all four lemmas and two theorems of this last part, you are officially done with this assignment! Congratulations!