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

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

Why not use

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

Induction is more convenient with

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

Or

Inductive nelist A := cons {
  head: A ;
  tail: nelist_tail A ;
}
with nelist_tail A :=
| nil
| next (_; nelist A) ;

But this is awkward in other ways.

Figuring out the best way to encode an inductive structure for the easiest reasoning is often quite annoying.