Define a equivalence between SimpleQueue and EfficientQueue

Stream: lean4

[Bernardo Borges]

Following the CS 1951x Course that covers The Hitchhiker's Guide to Logical Verification book, we arrive at chapter 5, functional programming. We have already defined a SimpleQueue with these properties:

* `SimpleQueue.emp : SimpleQueue α`, an empty queue
* `SimpleQueue.enq : SimpleQueue α → α → SimpleQueue α`, a function that
  enqueues a value onto an existing queue (i.e., `SimpleQueue.enq sq x` should
  evaluate to the queue resulting from sticking `x` at the back of the queue
  represented by `sq`)
* `SimpleQueue.deq : SimpleQueue α → Option (α × SimpleQueue α)`, a function
  that dequeues from an existing queue. This should return `none` if called on
  an empty queue; otherwise, it should return `some` applied to a tuple
  containing the dequeued element in the first position and the rest of the
  queue in the second

Now we want to prove that another implementation called EfficientQueue is equivalent to the naive approach (It uses two lists), meaning I have to define
def Equiv {α : Type} : SimpleQueue α → EfficientQueue α → Prop
However, I am not sure what this should look like, as I never "returned a Prop" before. As a next step, I want to understand how am I supposed to use this to prove the base case, that two empty queues of both types are equivalent theorem emp_equiv {α : Type} : Equiv (α := α) SimpleQueue.emp EfficientQueue.emp.

This is my attempt:

def Equiv {α : Type} : SimpleQueue α → EfficientQueue α → Prop :=
  λ sq eq => match sq.deq with
   | none         => eq.deq = none
   | some (x,sq') => match eq.deq with
      | none => False
      | some (y,eq') => x = y ∧ (Equiv sq' eq')
decreasing_by sorry

Note the sorry for termination. Is this the right track? I am open to suggestions!

[James Gallicchio]

I think in this case the easiest thing to do is something like

def SimpleQueue.toList : SimpleQueue α -> List α := ...
def EfficientQueue.toList : EfficientQueue α -> List α := ...

def Equiv {α : Type} (sq : SimpleQueue α) (eq : EfficientQueue α) : Prop :=
  sq.toList = eq.toList

to avoid the recursive definition and get access to all the nice List lemmas :)

[James Gallicchio]

(and then you can prove stuff like EfficientQueue.emp.toList = [] as lemmas, from which the equivalences should be straightforward)

[Bernardo Borges]

Interesting, from this suggestion I implemented the conversion:

def toList : SimpleQueue α → List α := id

def toList : EfficientQueue α → List α
| ([],xs)    => xs
| (xs, ys) => xs.reverse ++ ys

This way the proof for equivalence for empty queues is rfl:

theorem emp_equiv {α : Type} :
  Equiv (α := α) SimpleQueue.emp EfficientQueue.emp := by rfl

Now the complex part is to prove the equivalence for enqueuing:

theorem enq_equiv {α : Type} :
  ∀ (sq : SimpleQueue α) (eq : EfficientQueue α) (x : α),
  Equiv sq eq → Equiv (sq.enq x) (eq.enq x) := sorry

Any ideas here ?

[James Gallicchio]

You should then be able to show that (sq.enq x).toList = sq.toList ++ [x] (or whichever side it's getting enqueued at) as a lemma, same for eq, and then the enq_equiv lemma is a matter of unfolding definitions and doing some rewrites