recursion - 在 coq 中证明两个列表队列

Question

我试图证明这里描述的队列实现的正确性：

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.

在这里提琴

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

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而不是依赖于Equation' 模式匹配构造，但是我在以这种方式证明格式良好时遇到了麻烦。有没有办法推动这个证明？

（最初是用写的，Program Fixpoint但我也无法得到这个答案）。

Answer 1

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

寓意是：不要使用match ... with end eq_refl构造，而是依赖with和inspect模式，然后方程式将避免让您陷入依赖重写地狱。

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.

Answer 2

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

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

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对象使生成的方程难以处理。（很多“重写......的依赖类型错误”就像这个问题一样）。

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

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用自由重写生成的引理进行推理。