4
$\begingroup$

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?
$\endgroup$

3 Answers 3

3
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.