How to make sublists in Coq?

Question

I'm working in Coq and trying to figure out how to do the next thing: If I have a list of natural numbers and a given number n, I want to break my list in what goes before and after each of the n's. To make it clearer, if I have the list [1; 2; 0; 3; 4; 0; 9] and the number n = 0, then I want to have as output the three lists: [1;2], [3;4] and [9]. The main problem I have is that I don't know how to output several elements on a Fixpoint. I think I need to nest Fixpoints but I just don't see how. As a very raw idea with one too many issues I have:

Fixpoint SubLists (A : list nat)(m : nat) :=
 match A with
 |[] => []
 |n::A0 => if n =? m then (SubLists L) else n :: (SubLists L)
end.

I would very much appreciate your input on how to do this, and how to navigate having an output of several elements.

Answer 1

You can do this by combining a few fixpoints:

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

Fixpoint prefix n l :=
  match l with
  | [] => []
  | m :: l' => if beq_nat n m then []
               else m :: prefix n l'
  end.

Fixpoint suffix n l :=
  match l with
  | [] => l
  | m :: l' => if beq_nat n m then l'
               else suffix n l'
  end.

Fixpoint split_at n l :=
  match l with
  | [] => []
  | m :: l' => prefix n (m :: l') :: split_at n (suffix n (m :: l'))
  end.

Notice that Coq's termination checker accepts the recursive call to split_at, even though it is not done syntactically a subterm of l. The reason for that is that it is able to detect that suffix only outputs subterms of its argument. But in order for this to work, we must return l, and not [] on its first branch (try changing it to see what happens!).

Answer 2

In addition to Arthur's solution, you can use an accumulator, which is typical of Functional Programming style:

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

Definition add_acc m (s : list (list nat)) :=
  match s with
  | []      => [[m]]
  | s :: ss => (m :: s) :: ss
  end.

Fixpoint split_seq n l acc :=
  match l with
  | []      => map (@rev _) (rev acc)
  | m :: l' => if beq_nat n m then
                 split_seq n l' ([] :: acc)
               else
                 split_seq n l' (add_acc m acc)
  end.

Compute (split_seq 0 [1; 2; 0; 3; 4; 0; 9] []).

Note that the result is reversed so you need to use rev. A bonus exercise is to improve this.

EDIT: Provided second variant that doesn't add [] for repeated separators.

Definition reset_acc (s : list (list nat)) :=
  match s with
  | [] :: ss => [] :: ss
  | ss       => [] :: ss
  end.

Fixpoint split_seq_nodup n l acc :=
  match l with
  | []      => map (@rev _) (rev acc)
  | m :: l' => if beq_nat n m then
                 split_seq_nodup n l' (reset_acc acc)
               else
                 split_seq_nodup n l' (add_acc m acc)
  end.

Compute (split_seq_nodup 0 [1; 2; 0; 3; 4; 0; 9] []).