Proving two-list queue in coq

I'm trying to prove correctness of the queue implementation described here:

Inductive queue_type (A : Type) : Type := Queue : list A -> list A -> queue_type A.
Context {A : Type}.
Definition empty_queue : queue_type A := Queue nil nil.

Definition enqueue (queue : queue_type A) (elt : A) : queue_type A :=
  match queue with Queue front back => Queue front (elt :: back) end.

Definition dequeue (queue : queue_type A) : queue_type A * option A :=
  match queue with
  | Queue nil nil => (queue, None)
  | Queue (x :: xs) back => (Queue xs back, Some x)
  | Queue nil back =>
    let front := rev' back in
    match front with
    | (x :: xs) => (Queue xs nil, Some x)
    | nil => (Queue nil nil, None) (* Dead code *)
    end
  end.

Definition queue_to_list (* last elt in head *) (queue : queue_type A) : list A :=
    match queue with Queue front back => (back ++ rev front) end.

Definition queue_length (queue : queue_type A) : nat :=
    match queue with Queue front back => List.length front + List.length back end.

Fiddle here

One of the things I'd like to prove involves draining the queue, so I defined this function to do the computation:

Equations queue_dump_all (queue : queue_type A): list A :=
    queue_dump_all queue := worker queue nil
  where worker (queue': queue_type A) : list A -> list A by wf (queue_length queue') lt :=
        worker queue' acc := match (dequeue queue') as deq_res return (deq_res = (dequeue queue')) -> list A with 
                               | (queue'', Some elt) => fun pf => (worker queue'' (elt :: acc))
                               | _ => fun _=> acc
                               end _.

Reasoning with queue_dump_all is challenging, so I'm trying to prove this lemma to allow a more direct computation:

Lemma queue_dump_all_to_list: forall (queue: queue_type A), (queue_dump_all queue) = (queue_to_list queue).

I haven't been able to make progress using queue_dump_all_elim, though. I suspect the problem might be the 'manual' matching in worker instead of relying on Equation's pattern matching construct, but I had trouble with the proof of well formedness that way. Is there a way to push this proof forward?

(Originally written using Program Fixpoint but I couldn't get this answer to work either).

Here is a solution following your initial try: https://x80.org/collacoq/amugunalib.coq

The moral is: do not use match ... with end eq_refl constructs but rather rely on with and the inspect pattern, Equations will then avoid getting you into dependent rewrite hell.

From Equations Require Import Equations.
Require Import List.
Set Implicit Arguments.
Set Asymmetric Patterns.

Inductive queue_type (A : Type) : Type := Queue : list A -> list A -> queue_type A.
Context {A : Type}.
Definition empty_queue : queue_type A := Queue nil nil.

Definition enqueue (queue : queue_type A) (elt : A) : queue_type A :=
  match queue with Queue front back => Queue front (elt :: back) end.

Equations dequeue (queue : queue_type A) : queue_type A * option A :=
  | Queue nil nil => (Queue nil nil, None);
  | Queue (x :: xs) back => (Queue xs back, Some x);
  | Queue nil back with rev' back := {
    | (x :: xs) => (Queue xs nil, Some x);
    | nil => (Queue nil nil, None) (* Dead code *) }.

Definition queue_to_list (* last elt in head *) (queue : queue_type A) : list A :=
    match queue with Queue front back => (back ++ rev front) end.

Definition queue_length (queue : queue_type A) : nat :=
    match queue with Queue front back => List.length front + List.length back end.
Axiom cheat : forall {A}, A.

Lemma dequeue_queue_to_list (q : queue_type A) : 
  let (l, r) := dequeue q in queue_to_list q = 
  match r with Some x => queue_to_list l ++ (cons x nil) | None => nil end.
Proof.
  funelim (dequeue q); unfold queue_to_list; auto.
  - cbn. now rewrite app_assoc.
  - cbn. apply cheat. (* contradiction *)
  - cbn. apply cheat. (* algebra on rev, etc *)
Qed.

Definition inspect {A} (a : A) : { b : A | a = b } := (exist _ a eq_refl).

Equations queue_dump_all (queue : queue_type A): list A :=
    queue_dump_all queue := worker queue nil
  where worker (queue': queue_type A) : list A -> list A by wf (queue_length queue') lt :=
        worker queue' acc with inspect (dequeue queue') := {
                         | @exist (queue'', Some elt) eq => 
                            (worker queue'' (elt :: acc));
                         | _ => acc }.
                           
Next Obligation.
 apply cheat.
 Defined.

Lemma app_cons_nil_app {A} (l : list A) a l' : (l ++ a :: nil) ++ l' = l ++ a :: l'.
Proof.
  now rewrite <- app_assoc; cbn.
Qed.

Lemma queue_dump_all_to_list: forall (queue: queue_type A), (queue_dump_all queue) = (queue_to_list queue).
Proof.
  intros q.
  apply (queue_dump_all_elim (fun q l => l = queue_to_list q)
    (fun q queue' acc res =>
      
      res = queue_to_list queue' ++ acc)); auto.
  - intros.
    now rewrite app_nil_r in H.
  - intros. rewrite H; clear H.
    generalize (dequeue_queue_to_list queue').    
    destruct (dequeue queue').
    clear Heq. noconf e.
    intros ->. now rewrite app_cons_nil_app.
  - intros.
    generalize (dequeue_queue_to_list queue').
    destruct (dequeue queue').
    clear Heq. noconf e. cbn.
    now intros ->.
Qed.