# Why use records for non-empty lists rather than inductively defined non-empty lists?

I've come across two main ways to do non-empty lists:

Inductive nelist (A : Type) := one : A -> nelist A | cons : A -> nelist A -> nelist A.

Record nelist_b (A : Type) := build_nelist { hd : A ; tl : list A }.


The first one replaces the usual nil with a one-element node, thereby enforcing that there's always a last element. The other wraps a different structure around a plain list, thereby enforcing that there's always a head.

I'm currently trying to use a library that uses the latter approach, but the two-types nature of this approach is complicating things for me. The problem I have here that this will result in three cases (head, cons, nil), where the head and cons cases are supposed to behave the same, but I can't prove that because it's a statement across different types, resulting in me basically copy/pasting the code for the branches and visually checking identiy. (Making an induction principle-style wrapper that converts on the fly is also non-trivial, as that would result in recursion on a freshly synthesized node instead of a structurally smaller part of the input, and then I'd have to explicitly prove termination via a measure or some other approach. Ugh.)

So I've looked into converting the whole thing to the first approach, gave it a try, and finished in a few hours. Along the way, I saw that there's not much conversion back & forth between normal and non-empty lists, and so now I'm wondering why this approach was chosen in the first place.

• Is there a reason to prefer the wrapper approach to non-empty lists?
• Is there maybe some easy way of working with the two-types approach that I'm not aware of yet?
• Or are there hidden problems with the first approach that I'm not seeing yet?

Since nelist_b is based on pre-existing lists, you can presumably reuse a lot of results on lists when proving facts about nelist_bs. So I would guess the point of nelist_b is to never actually do induction on tl, but reuse some result on it. However, I have never used non-empty lists, so this is just my expectation.

You could also try to use dependently typed sequences (I'm using the Mathematical Components library here), as in:

Record nelist (A : Type) :=
new_nelist {
list : seq A;
_ : 0 < length list;
}.

Definition l := [:: 1].
Lemma lt0l : 0 < length l. Proof. by []. Qed.

Definition n := new_nelist lt0l.

Compute (list n).


Coercions can be used to make things even simpler, and allow you to reuse all the lemmas related to sequences in a straightforward way.

Why not use

Inductive nelist A := cons {
tail: option (nelist A) ;
}.


Induction is more convenient with

Inductive nelist A := cons {
hastail: bool ;
tail: Is_true hastail -> nelist A ;
}.


Or

Inductive nelist A := cons {