The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Here's another implementation, where instead of `destruct eqn:` I use an
auxiliary function that makes a case distinction whether a list is empty
or not.

```
(** Returns either a proof that [l = nil] or a proof that [1 <= length
l]. *)
Definition list_nil_or_not_empty (l : list A) : (l = nil) + (1 <= length l).
Proof.
  destruct l.
  - left. reflexivity.
  - right. cbn. abstract omega.
Defined.

Fixpoint fromList (l : list A) : 1 <= length l -> nonEmpty A.
Proof.
  destruct l as [ | x l'].
  - intros H. (* [H : 1 <= length nil] *)
    exfalso. cbn in H. abstract omega.
  - intros _. (* We can forget the hypothesis, since it is a tautology:
[1 <= length (x :: l')] *)
    (* Instead, we make a case analysis whether [l'] is empty or not *)
    destruct (list_nil_or_not_empty l') as [Hl'|Hl'].
    + (* [Hl' : l' = nil] *) (* We don't actually need the proof here
that [l' = nil]. *)
      exact (singleton x).
    + (* [Hl' : 1 <= length l'] *)
      refine (consNE x (fromList l' _)).
      exact (consNE x (fromList l' Hl')).
Defined.
```

On 30/09/2020 21:19, Maximilian Wuttke wrote:
> ```
>   Fixpoint fromList (l : list A) : 1 <= length l -> nonEmpty A.
>   Proof.
>     destruct l as [ | x l'].
>     - intros H. exfalso. cbn in H. abstract omega.
>     - destruct l' as [ | y l''] eqn:E.
>       + intros _. exact (singleton x).
>       + intros H. refine (consNE x (fromList l' _)).
>         abstract (subst; cbn in *; omega).
>   Defined.
> ```