coq - 如何在 coq 中将列表分成两半？

在我真正尝试处理它之前，它看起来绝对是简单的任务。我的方法是使用双指针来避免提前询问列表的长度，但困难来自于我确信一个列表“不比另一个更空”的含义。具体来说，在伪 coq 中:

Definition twin_ptr (heads, tail, rem : list nat) :=
  match tail, rem with
  | _, [] => (rev heads, tail)
  | _, [_] => (rev heads, tail)
  | t :: tl, _ :: _ :: rm => twin_ptr (t :: heads) tl rm
  end.

Definition split (l : list nat) := twin_ptr [] l l

但肯定不会编译，因为匹配案例不完整。但是，不存在构造缺失的情况。

你的实现方式是什么？

最佳答案

我不怕依赖类型，您可以添加 rem 比 tail 短的证明作为 twin_ptr 的参数。使用 Program 来帮助管理这些依赖类型，这可以给出以下内容。

Require Import List. Import ListNotations.
Require Import Program.
Require Import Arith.
Require Import Omega.

Program Fixpoint twin_ptr
  (heads tail rem : list nat)
  (H:List.length rem <= List.length tail) :=
  match tail, rem with
  | a1, [] => (rev heads, tail)
  | a2, [a3] => (rev heads, tail)
  | t :: tl, _ :: _ :: rm => twin_ptr (t :: heads) tl rm _
  | [], _::_::_ => !
  end.
Next Obligation.
  simpl in H. omega.
Qed.
Next Obligation.
  simpl in H. omega.
Qed.

Definition split (l : list nat) := twin_ptr [] l l (le_n _).

感叹号表示无法访问分支。

然后，您可以证明有关 twin_ptr 的引理并从中推导出 split 的属性。例如，

Lemma twin_ptr_correct : forall head tail rem H h t,
  twin_ptr head tail rem H = (h, t) ->
  h ++ t = rev head ++ tail.
Proof.
Admitted.

Lemma split_correct : forall l h t,
  split l = (h, t) ->
  h ++ t = l.
Proof.
  intros. apply twin_ptr_correct in H. assumption.
Qed.

就我个人而言，我不喜欢在函数中使用依赖类型，因为结果对象更难操作。相反，我更喜欢定义全函数并在引理中给它们正确的假设。

关于coq - 如何在 coq 中将列表分成两半？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/46348606/