The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

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