The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Another very convenient way is to define `toList` by well-founded
recursion on the size of the list.

```
Set Implicit Arguments.

Require Import Omega.
From Coq Require Import Lists.List.
Import ListNotations.
From Equations Require Import Equations.

Inductive nonEmpty (A : Type) : Type :=
| singleton : A -> nonEmpty A
| consNE : A -> nonEmpty A -> nonEmpty A.

Section NonEmpty.

  Variable A : Type.

  Fixpoint toList (l : nonEmpty A) :=
    match l with
    | singleton x => (cons x nil)
    | consNE x xs => (cons x (toList xs))
    end.

  Equations? fromList (l : list A) : length l > 0 -> nonEmpty A by wf
(length l) lt :=
    {
      fromList nil H := _;
      fromList (cons x nil) _ := singleton x;
      fromList (cons x (cons y l)) _ := consNE x (fromList (cons y l) _)
    }.
  Proof.
    - exfalso. abstract omega.
    - abstract omega.
  Qed.

End NonEmpty.

Compute fromList [1] _.     (* = singleton 1 *)
Compute fromList [1;2] _.   (* = consNE 1 (singleton 2) *)
Compute fromList [1;2;3] _. (* = consNE 1 (consNE 2 (singleton 3)) *)
```

Here, I used the Equations plugin [1], which must be installed first.

[1]: <https://github.com/mattam82/Coq-Equations/>