How can I split a list in half in coq?

Question

It looks definitely simple task until I actually try to work on it. My method is to use twin pointers to avoid asking the length of the list ahead of time, but the difficulties come from the implication that I know for sure one list is "no emptier" than another. Specifically, in pseudo-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

But definitely it's not going to compile because the match cases are incomplete. However, the missing case by construction doesn't exist.

What's your way of implementing it?

Answer 1

May I suggest going via a more precise type? The main idea is to define a function splitting a Vector.t whose nat index has the shape m + n into a Vector.t of size m and one of size 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.

Once you have this, you've reduced your problem to defining the floor and ceil of n / 2 and proving that they sum to 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.

Indeed, you can then convert length xs into ceil (length xs / 2) + floor (length xs / 2) and use split_vector to get each part.

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.

Answer 2

I you are not afraid of dependent types, you can add a proof that rem is shorter than tail as an argument of twin_ptr. Using Program to help manage these dependent types, this could give the following.

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

The exclamation mark means that a branch is unreachable.

You can then prove lemmas about twin_ptr and deduce the properties of split from them. For example,

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.

Personally, I dislike to use dependent types in functions, as resulting objects are more difficult to manipulate. Instead, I prefer defining total functions and give them the right hypotheses in the lemmas.

Answer 3

You do not need to maintain the invariant that the second list is bigger than the third. Here is a possible solution:

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.