在coq中证明两表队列

Inductive Queue : Type :=
  | Empty : Queue
  | Queue : list nat -> list nat -> Queue.

Definition enqueue (x : nat) (q : Queue) : Queue :=
  match q with
  | Empty => Queue [x] []
  | Queue inlist outlist => Queue (x :: inlist) outlist
  end.

Definition dequeue (q : Queue) : option (nat * Queue) :=
  match q with
  | Empty => None
  | Queue inlist outlist =>
      match outlist with
      | [] =>
          match rev inlist with
          | [] => None
          | x :: xs => Some (x, Queue [] xs)
          end
      | x :: xs => Some (x, Queue inlist xs)
      end
  end.

Definition queue_length (q : Queue) : nat :=
  match q with
  | Empty => 0
  | Queue inlist outlist => length inlist + length outlist
  end.

Lemma enqueue_length : forall (x : nat) (q : Queue),
  queue_length (enqueue x q) = S (queue_length q).
Proof.
  intros x q. destruct q.
  - reflexivity.
  - simpl. reflexivity.
Qed.

Lemma dequeue_length : forall (q : Queue),
  match dequeue q with
  | None => queue_length q = 0
  | Some (_, q') => queue_length q = S (queue_length q')
  end.
Proof.
  intros q. destruct q.
  - reflexivity.
  - destruct outlist.
    + destruct (rev inlist) eqn:E.
      * reflexivity.
      * simpl. reflexivity.
    + simpl. reflexivity.
Qed.