在 coq 中证明两个列表队列

Question

我正在尝试证明描述的队列实现的正确性 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

我想证明的一件事涉及清空队列，所以我定义了这个函数来进行计算：

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 _.

用 queue_dump_all 推理很有挑战性，所以我试图证明这个引理以允许更直接的计算：

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

不过，我无法使用 queue_dump_all_elim 取得进展。我怀疑问题可能出在 worker 中的 'manual' 匹配而不是依赖 Equation 的模式匹配构造，但我在证明格式良好方面遇到了麻烦。有没有办法推进这个证明？

（最初使用 Program Fixpoint 编写，但我也无法使工作）。

Answer 1

有根据的递归的问题在于它使用证明项进行计算。当尝试使用 queue_dump_all 进行计算时，这一点很明显，这需要重写并使一些引理透明，并注意漏洞的证明。（this blogpost 帮我解决了这个问题）。

然而，对证明项的依赖使得很难对展开的项进行任何推理。我的第一次尝试是具体化度量并将证明移动到签名类型中：

Equations queue_dump_all: queue_type A -> list A :=
    queue_dump_all qu := worker (exist (fun q => queue_length q = (queue_length queue)) qu eq_refl) nil
                                      
  where worker (len: nat) (q: {q: queue_type A | queue_length q = len}) (acc: list A): list A :=
        @worker 0 _ acc := acc;
        @worker (S len') queue acc with (dequeue queue.val).2 := {
            | Some elt := (worker (exist (fun q=> queue_length q = len') (dequeue (proj1_sig queue)).1 _) (elt :: acc));
            | _ := acc
        }.

这更容易证明和实际计算，因为现在可以轻松删除证明项。然而，sig 对象使得生成的方程式难以处理。（在 this question 中有很多“重写中的依赖类型错误”）。

解决方案最终转向了这样的弱规范：

Equations drain' (queue : queue_type A): option (list A) :=
  drain' queue := worker (S (queue_length queue)) queue nil
where worker (gas: nat) (q: queue_type A) (acc: list A): option (list A) :=
      @worker 0 _ _ := None;
      @worker (S gas') queue acc with (dequeue queue).2 := {
          | Some elt := worker gas' (dequeue queue).1 (elt :: acc);
          | _ := Some acc
      }.

Lemma drain_completes: forall q, drain' q <> None. ... Qed.

Definition queue_drain (queue: queue_type A): list A :=
    match drain' queue as res return (drain' queue = res -> list A) with
    | Some drained => fun pf => drained
    | None => fun pf => False_rect _ (drain_completes pf)
    end eq_refl.

将证明项从计算中移出，可以更轻松地使用 Equation 生成的引理进行推理，并可以自由重写。

Answer 2

这是您最初尝试后的解决方案： https://x80.org/collacoq/amugunalib.coq

道德是：不要使用 match ... with end eq_refl 构造，而是依赖 with 和 inspect pattern，方程将避免让你陷入依赖重写地狱。

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.

在 coq 中证明两个列表队列

Proving two-list queue in coq

recursion

queue

coq

dependent-type

fixpoint-combinators