如何解决在 coq 中证明两列表队列
我正在尝试证明 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.
我想证明的一件事涉及排空队列,所以我定义了这个函数来进行计算:
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
编写,但我也无法让 this answer 工作)。
解决方法
有根据的递归的问题在于它使用证明项进行计算。这在尝试使用 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
生成的引理进行推理,并且可以自由重写。
这是您初次尝试后的解决方案: 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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。