The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

That fixpoint fromList is not going to be structurally recursive as it
is defined, even if you do solve its remaining subgoals.  I would
suggest this alternative:

Fixpoint fromList (l : list A)(lgt0 : length l > 0) :nonEmpty A.

If you still really need to have a single arg version of fromList that
takes a sigma type, my suggestion is to define it in terms of the above
alternative.

On Wed, 30 Sep 2020 13:21:49 -0500
Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

> I am trying to write a function whose argument type is a sigma type.
> Here are some details.
> 
> Inductive nonEmpty (A : Type) : Type :=
> | singleton : A -> nonEmpty A
> | consNE : A -> nonEmpty A -> nonEmpty A.
> 
> Arguments singleton {A}.
> Arguments consNE {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.
> 
>   Fixpoint fromList (l : {l : list A | length l > 0}) : nonEmpty A.
>     refine (match (proj1_sig l) with
>             | nil => _
>             | (cons x nil) => singleton x
>             | (cons x xs) => consNE x (fromList (exist (fun xs =>
> length xs
> > 0) xs _))  
>             end).
> 
> Now, how do I solve these goals? For the first one, I want to show a
> contradiction, saying that (proj1_sig l) couldn't have been nil,
> given that we know that length ((proj1_sig l)) > 0. However, the
> equation (proj1_sig l) = nil is not present in the context. It is
> very similar in the case of the other hole as well.
> 
> --Agnishom