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

Question

在我真正尝试完成之前，它看起来绝对是一项简单的任务。我的方法是使用双指针来避免提前询问列表的长度，但困难来自于我确定一个列表比另一个列表 "no emptier" 的含义。具体来说，在伪 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

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

你的实现方式是什么？

Answer 1

您不需要维护第二个列表大于第三个列表的不变量。这是一个可能的解决方案：

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Div2.
Require Import Coq.Lists.List.
Import ListNotations.

Section Split.

Variable A : Type.

Fixpoint split_aux (hs ts l : list A) {struct l} : list A * list A :=
  match l with
  | []  => (rev hs, ts)
  | [_] => (rev hs, ts)
  | _ :: _ :: l' =>
    match ts with
    | []      => (rev hs, [])
    | h :: ts => split_aux (h :: hs) ts l'
    end
  end.

Lemma split_aux_spec hs ts l n :
  n = div2 (length l) ->
  split_aux hs ts l = (rev (rev (firstn n ts) ++ hs), skipn n ts).
Proof.
revert hs ts l.
induction n as [|n IH].
- intros hs ts [|x [|y l]]; easy.
- intros hs ts [|x [|y l]]; simpl; try easy.
  intros Hn.
  destruct ts as [|h ts]; try easy.
  rewrite IH; try congruence.
  now simpl; rewrite <- app_assoc.
Qed.

Definition split l := split_aux [] l l.

Lemma split_spec l :
  split l = (firstn (div2 (length l)) l, skipn (div2 (length l)) l).
Proof.
unfold split.
rewrite (split_aux_spec [] l l (div2 (length l))); trivial.
now rewrite app_nil_r, rev_involutive.
Qed.

End Split.

Answer 2

我你不怕依赖类型，你可以添加一个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.

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

Answer 3

我可以建议使用更精确的类型吗？主要思想是定义一个函数，将 Vector.t 的 nat 索引的形状 m + n 拆分为大小为 m 的 Vector.t 和大小为 n.

Require Import Vector.

Definition split_vector : forall a m n,
  Vector.t a (m + n) -> (Vector.t a m * Vector.t a n).
Proof.
intros a m n; induction m; intro v.
- firstorder; constructor.
- destruct (IHm (tl v)) as [xs ys].
  firstorder; constructor; [exact (hd v)|assumption].
Defined.

一旦你有了这个，你就把问题简化为定义 n / 2 的 floor 和 ceil 并证明它们的总和为 n。

Fixpoint div2_floor_ceil (n : nat) : (nat * nat) := match n with
  | O        => (O , O)
  | S O      => (O , S O)
  | S (S n') => let (p , q) := div2_floor_ceil n'
                in (S p, S q)
end.

Definition div2_floor (n : nat) := fst (div2_floor_ceil n).
Definition div2_ceil  (n : nat) := snd (div2_floor_ceil n).

Lemma plus_div2_floor_ceil : forall n, div2_floor n + div2_ceil n = n.
Proof.
refine
  (fix ih n := match n with
     | O => _
     | S O => _
     | S (S n') => _
   end); try reflexivity.
unfold div2_floor, div2_ceil in *; simpl.
destruct (div2_floor_ceil n') as [p q] eqn: eq.
simpl.
replace p with (div2_floor n') by (unfold div2_floor ; rewrite eq ; auto).
replace q with (div2_ceil n') by (unfold div2_ceil ; rewrite eq ; auto).
rewrite <- plus_n_Sm; do 2 f_equal.
apply ih.
Qed.

的确，你可以将length xs转换成ceil (length xs / 2) + floor (length xs / 2)并使用split_vector得到每个部分。

Definition split_list a (xs : list a) : (list a * list a).
Proof.
refine
  (let v      := of_list xs in
  let (p , q) := split_vector a (div2_floor _) (div2_ceil _) _ in
  (to_list p, to_list q)).
rewrite plus_div2_floor_ceil; exact v.
Defined.

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

How can I split a list in half in coq?

coq